Lemma·L15
Basic properties of the order
Irreflexive, transitive, successor-compatible: the order behaves.
For all
, with
and
from D029:(i)
;(ii)
;(iii)
;(iv)
;(v)
;(vi)
;(vii)
.
In words
No number is less than itself; less-than chains compose; being less than a successor means being at most the predecessor; zero is least; if m is strictly below n then the successor of m is still at most n; every number is below its successor; and every non-zero number is a successor.
Never needed: F05 · F08 · F10 · F12 · F13 · A02 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).
Proof
- 1
- 2(ii) and : since is a transitive set by L07, , so .
- 3
- 4(iv) Induction on (T05, Separation): holds as . If , then in either case ( or ) we get , so , hence .
- 5(v) Induction on with quantified inside: let . Base: means , impossible (D002), so vacuously. Step: let and ; by (iii) . If : . If : the hypothesis gives ; if then by (vi) below at (that is, with substitutivity); if then . Either way , so : . T05 gives .
- 6
- 7(vii) Induction on : for the implication holds vacuously, since by reflexivity makes the antecedent false (F04, ex falso). For : take ; then , since and ω is transitive, and .
∎
Remarks
Seven small facts, stated once so that later proofs can cite them by number. (i) and (ii) make
a strict order; (iii) is the bridge between order and successor; (iv) and (vii) anchor arguments at zero; (v) is the discreteness of the naturals (nothing lives strictly between
and
); (vi) feeds every induction that climbs one step.
Used by
Propose an edit2 published revisions