Es gelten die allgemeinen Vorbemerkungen.
| (1) | Theorem 28 | ∀a: ∀b: ∀c: <(Sc·a)=(Sc·b) ⇒ a=b> | |||||||||
| (2) | Spezialisierung (1) a ← 0 | ∀b: ∀c: <(Sc·0)=(Sc·b) ⇒ 0=b> | |||||||||
| (3) | Spezialisierung (2) b ← b | ∀c: <(Sc·0)=(Sc·b) ⇒ 0=b> | |||||||||
| (4) | Spezialisierung (3) c ← a | <(Sa·0)=(Sa·b) ⇒ 0=b> | |||||||||
| (5) | Axiom 4 | ∀a: (a·0)=0 | |||||||||
| (6) | Spezialisierung (5) a ← Sa | (Sa·0)=0 | |||||||||
| (7) | Symmetrie (6) | 0=(Sa·0) | |||||||||
| (8) | Hypothese | (Sa·0)=Sa | |||||||||
| (9) | Übernahme (7) | 0=(Sa·0) | |||||||||
| (10) | Transitivität (9), (8) | 0=Sa | |||||||||
| (11) | Symmetrie (10) | Sa=0 | |||||||||
| (12) | Konklusion (8), (11) | <(Sa·0)=Sa ⇒ Sa=0> | |||||||||
| (13) | Kontraposition (12) | <¬Sa=0 ⇒ ¬(Sa·0)=Sa> | |||||||||
| (14) | Axiom 1 | ∀a: ¬Sa=0 | |||||||||
| (15) | Spezialisierung (14) a ← a | ¬Sa=0 | |||||||||
| (16) | Modus ponens (13), (15) | ¬(Sa·0)=Sa | |||||||||
| (17) | Hypothese | ¬0=S0 | |||||||||
| (18) | Übernahme (16) | ¬(Sa·0)=Sa | |||||||||
| (19) | Konklusion (17), (18) | <¬0=S0 ⇒ ¬(Sa·0)=Sa> | |||||||||
| (20) | Kontraposition (19) | <¬¬(Sa·0)=Sa ⇒ ¬¬0=S0> | |||||||||
| (21) | Hypothese | (Sa·0)=Sa | |||||||||
| (22) | Doppelte Negation (21) | ¬¬(Sa·0)=Sa | |||||||||
| (23) | Übernahme (20) | <¬¬(Sa·0)=Sa ⇒ ¬¬0=S0> | |||||||||
| (24) | Modus ponens (23), (22) | ¬¬0=S0 | |||||||||
| (25) | Doppelte Negation (24) | 0=S0 | |||||||||
| (26) | Konklusion (21), (25) | <(Sa·0)=Sa ⇒ 0=S0> | |||||||||
| (27) | Axiom 5 | ∀a: ∀b: (a·Sb)=((a·b)+a) | |||||||||
| (28) | Spezialisierung (27) a ← Sa | ∀b: (Sa·Sb)=((Sa·b)+Sa) | |||||||||
| (29) | Spezialisierung (28) b ← b | (Sa·Sb)=((Sa·b)+Sa) | |||||||||
| (30) | Theorem 8 | ∀a: ∀b: (a+b)=(b+a) | |||||||||
| (31) | Spezialisierung (30) a ← Sa | ∀b: (Sa+b)=(b+Sa) | |||||||||
| (32) | Spezialisierung (31) b ← (Sa·b) | (Sa+(Sa·b))=((Sa·b)+Sa) | |||||||||
| (33) | Symmetrie (32) | ((Sa·b)+Sa)=(Sa+(Sa·b)) | |||||||||
| (34) | Transitivität (29), (33) | (Sa·Sb)=(Sa+(Sa·b)) | |||||||||
| (35) | Symmetrie (34) | (Sa+(Sa·b))=(Sa·Sb) | |||||||||
| (36) | Theorem 27 | ∀a: ∀b: <(a+b)=a ⇒ b=0> | |||||||||
| (37) | Spezialisierung (36) a ← Sa | ∀b: <(Sa+b)=Sa ⇒ b=0> | |||||||||
| (38) | Spezialisierung (37) b ← (Sa·b) | <(Sa+(Sa·b))=Sa ⇒ (Sa·b)=0> | |||||||||
| (39) | Hypothese | (Sa·Sb)=Sa | |||||||||
| (40) | Übernahme (35) | (Sa+(Sa·b))=(Sa·Sb) | |||||||||
| (41) | Transitivität (40), (39) | (Sa+(Sa·b))=Sa | |||||||||
| (42) | Übernahme (38) | <(Sa+(Sa·b))=Sa ⇒ (Sa·b)=0> | |||||||||
| (43) | Modus ponens (42), (41) | (Sa·b)=0 | |||||||||
| (44) | Übernahme (7) | 0=(Sa·0) | |||||||||
| (45) | Transitivität (43), (44) | (Sa·b)=(Sa·0) | |||||||||
| (46) | Symmetrie (45) | (Sa·0)=(Sa·b) | |||||||||
| (47) | Übernahme (4) | <(Sa·0)=(Sa·b) ⇒ 0=b> | |||||||||
| (48) | Modus ponens (47), (46) | 0=b | |||||||||
| (49) | Symmetrie (48) | b=0 | |||||||||
| (50) | S hinzufügen (49) | Sb=S0 | |||||||||
| (51) | Konklusion (39), (50) | <(Sa·Sb)=Sa ⇒ Sb=S0> | |||||||||
| (52) | Hypothese | <(Sa·b)=Sa ⇒ b=S0> | |||||||||
| (53) | Übernahme (51) | <(Sa·Sb)=Sa ⇒ Sb=S0> | |||||||||
| (54) | Konklusion (52), (53) | <<(Sa·b)=Sa ⇒ b=S0> ⇒ <(Sa·Sb)=Sa ⇒ Sb=S0>> | |||||||||
| (55) | Verallgemeinerung (54) nach b | ∀b: <<(Sa·b)=Sa ⇒ b=S0> ⇒ <(Sa·Sb)=Sa ⇒ Sb=S0>> | |||||||||
| (56) | Induktion (26), (55) | ∀b: <(Sa·b)=Sa ⇒ b=S0> | |||||||||
| (57) | Verallgemeinerung (56) nach a | ∀a: ∀b: <(Sa·b)=Sa ⇒ b=S0> | |||||||||