Next: Induction, Up: Sequence Logic [Contents]
Sequence Logic, often abbreviated ’seqlog’, uses the following six axioms:
The first axiom states that no sucessor is the zero object, or, to put it differently, that the zero object is the first object. The second axiom states that no two different objects have the same sucessor. Using these two axioms, a ’Universal Sequence’ can be defined, in a way similar to how the Peano Axioms define the natural numbers. The third axiom is the definition of a sequence, stating that the value under a given sequence ’S’ of every object ’x’ can be determined by a function. The rule ’sq’ introduces such a sequence (see sq). The fourth axiom defines the nil object. This is a lot like ‘NULL’ in C, or ‘nil’ in lisp.
The natural numbers are defined as a sequence. For example, Vx(x = nat → VyVz(v(nat,y) = v(nat,z) → y = z) ^ Vy(~v(nat,y) = \0)). This will define an infinite sequence (2nd part), that is one-to-one (1st part). Then, to define zero, one simply states Vx(v(nat,z(x)) = 0). This means that the zero’th element of the ‘nat’ sequence is the object ‘0’.