Es gelten die allgemeinen Vorbemerkungen.
| (1) | Axiom 2 | ∀a: (a+0)=a | |||||||||
| (2) | Spezialisierung (1) a ← a | (a+0)=a | |||||||||
| (3) | Symmetrie (2) | a=(a+0) | |||||||||
| (4) | Axiom 3 | ∀a: ∀b: (a+Sb)=S(a+b) | |||||||||
| (5) | Spezialisierung (4) a ← a | ∀b: (a+Sb)=S(a+b) | |||||||||
| (6) | Spezialisierung (5) b ← d | (a+Sd)=S(a+d) | |||||||||
| (7) | Hypothese | (a+0)=Sb | |||||||||
| (8) | Übernahme (3) | a=(a+0) | |||||||||
| (9) | Transitivität (8), (7) | a=Sb | |||||||||
| (10) | Konklusion (7), (9) | <(a+0)=Sb ⇒ a=Sb> | |||||||||
| (11) | Kontraposition (10) | <¬a=Sb ⇒ ¬(a+0)=Sb> | |||||||||
| (12) | Hypothese | <¬a=Sb∧∀d: ¬(a+d)=b> | |||||||||
| (13) | Abtrennung I (12) | ¬a=Sb | |||||||||
| (14) | Abtrennung II (12) | ∀d: ¬(a+d)=b | |||||||||
| (15) | Übernahme (11) | <¬a=Sb ⇒ ¬(a+0)=Sb> | |||||||||
| (16) | Modus ponens (15), (13) | ¬(a+0)=Sb | |||||||||
| (17) | Hypothese | (a+Sd)=Sb | |||||||||
| (18) | Übernahme (6) | (a+Sd)=S(a+d) | |||||||||
| (19) | Symmetrie (18) | S(a+d)=(a+Sd) | |||||||||
| (20) | Transitivität (19), (17) | S(a+d)=Sb | |||||||||
| (21) | S entfernen (20) | (a+d)=b | |||||||||
| (22) | Konklusion (17), (21) | <(a+Sd)=Sb ⇒ (a+d)=b> | |||||||||
| (23) | Kontraposition (22) | <¬(a+d)=b ⇒ ¬(a+Sd)=Sb> | |||||||||
| (24) | Spezialisierung (14) d ← d | ¬(a+d)=b | |||||||||
| (25) | Modus ponens (23), (24) | ¬(a+Sd)=Sb | |||||||||
| (26) | Hypothese | ¬(a+d)=Sb | |||||||||
| (27) | Übernahme (25) | ¬(a+Sd)=Sb | |||||||||
| (28) | Konklusion (26), (27) | <¬(a+d)=Sb ⇒ ¬(a+Sd)=Sb> | |||||||||
| (29) | Verallgemeinerung (28) nach d | ∀d: <¬(a+d)=Sb ⇒ ¬(a+Sd)=Sb> | |||||||||
| (30) | Induktion (16), (29) | ∀d: ¬(a+d)=Sb | |||||||||
| (31) | Konklusion (12), (30) | <<¬a=Sb∧∀d: ¬(a+d)=b> ⇒ ∀d: ¬(a+d)=Sb> | |||||||||
| (32) | Kontraposition (31) | <¬∀d: ¬(a+d)=Sb ⇒ ¬<¬a=Sb∧∀d: ¬(a+d)=b>> | |||||||||
| (33) | Hypothese | <¬∀d: ¬(a+d)=Sb∧¬a=Sb> | |||||||||
| (34) | Abtrennung I (33) | ¬∀d: ¬(a+d)=Sb | |||||||||
| (35) | Abtrennung II (33) | ¬a=Sb | |||||||||
| (36) | Übernahme (32) | <¬∀d: ¬(a+d)=Sb ⇒ ¬<¬a=Sb∧∀d: ¬(a+d)=b>> | |||||||||
| (37) | Modus ponens (36), (34) | ¬<¬a=Sb∧∀d: ¬(a+d)=b> | |||||||||
| (38) | Hypothese | ∀d: ¬(a+d)=b | |||||||||
| (39) | Übernahme (35) | ¬a=Sb | |||||||||
| (40) | Konjunktion (39), (38) | <¬a=Sb∧∀d: ¬(a+d)=b> | |||||||||
| (41) | Konklusion (38), (40) | <∀d: ¬(a+d)=b ⇒ <¬a=Sb∧∀d: ¬(a+d)=b>> | |||||||||
| (42) | Kontraposition (41) | <¬<¬a=Sb∧∀d: ¬(a+d)=b> ⇒ ¬∀d: ¬(a+d)=b> | |||||||||
| (43) | Modus ponens (42), (37) | ¬∀d: ¬(a+d)=b | |||||||||
| (44) | Konklusion (33), (43) | <<¬∀d: ¬(a+d)=Sb∧¬a=Sb> ⇒ ¬∀d: ¬(a+d)=b> | |||||||||
| (45) | Verallgemeinerung (44) nach b | ∀b: <<¬∀d: ¬(a+d)=Sb∧¬a=Sb> ⇒ ¬∀d: ¬(a+d)=b> | |||||||||
| (46) | Verallgemeinerung (45) nach a | ∀a: ∀b: <<¬∀d: ¬(a+d)=Sb∧¬a=Sb> ⇒ ¬∀d: ¬(a+d)=b> | |||||||||
Interpretation:
Ist a<=Sb so a=Sb oder a<=b