Es gelten die allgemeinen Vorbemerkungen.
| (1) | Theorem 1 | ∀a: a=a | |||||||||
| (2) | Spezialisierung (1) a ← 0 | 0=0 | |||||||||
| (3) | Spezialisierung (1) a ← Sa | Sa=Sa | |||||||||
| (4) | Hypothese | ∀b: ¬Sb=0 | |||||||||
| (5) | Übernahme (2) | 0=0 | |||||||||
| (6) | Konklusion (4), (5) | <∀b: ¬Sb=0 ⇒ 0=0> | |||||||||
| (7) | Hypothese | <∀b: ¬Sb=a ⇒ a=0> | |||||||||
| (8) | Hypothese | ∀b: ¬Sb=Sa | |||||||||
| (9) | Spezialisierung (8) b ← a | ¬Sa=Sa | |||||||||
| (10) | Hypothese | ¬Sa=0 | |||||||||
| (11) | Übernahme (3) | Sa=Sa | |||||||||
| (12) | Konklusion (10), (11) | <¬Sa=0 ⇒ Sa=Sa> | |||||||||
| (13) | Kontraposition (12) | <¬Sa=Sa ⇒ ¬¬Sa=0> | |||||||||
| (14) | Modus ponens (13), (9) | ¬¬Sa=0 | |||||||||
| (15) | Doppelte Negation (14) | Sa=0 | |||||||||
| (16) | Konklusion (8), (15) | <∀b: ¬Sb=Sa ⇒ Sa=0> | |||||||||
| (17) | Konklusion (7), (16) | <<∀b: ¬Sb=a ⇒ a=0> ⇒ <∀b: ¬Sb=Sa ⇒ Sa=0>> | |||||||||
| (18) | Verallgemeinerung (17) nach a | ∀a: <<∀b: ¬Sb=a ⇒ a=0> ⇒ <∀b: ¬Sb=Sa ⇒ Sa=0>> | |||||||||
| (19) | Induktion (6), (18) | ∀a: <∀b: ¬Sb=a ⇒ a=0> | |||||||||
Interpretation:
Nur 0 hat keinen Vorgänger