0 is the zero element of the natural numbers. The natural numbers can be defined in TLA+. In this introduction, we just assume they are given.