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) | Theorem 1 | ∀a: a=a | |||||||||
| (5) | Spezialisierung (4) a ← 0 | 0=0 | |||||||||
| (6) | Hypothese | (a+0)=0 | |||||||||
| (7) | Übernahme (3) | a=(a+0) | |||||||||
| (8) | Transitivität (7), (6) | a=0 | |||||||||
| (9) | Übernahme (5) | 0=0 | |||||||||
| (10) | Konjunktion (8), (9) | <a=0∧0=0> | |||||||||
| (11) | Konklusion (6), (10) | <(a+0)=0 ⇒ <a=0∧0=0>> | |||||||||
| (12) | Axiom 3 | ∀a: ∀b: (a+Sb)=S(a+b) | |||||||||
| (13) | Spezialisierung (12) a ← a | ∀b: (a+Sb)=S(a+b) | |||||||||
| (14) | Spezialisierung (13) b ← b | (a+Sb)=S(a+b) | |||||||||
| (15) | Symmetrie (14) | S(a+b)=(a+Sb) | |||||||||
| (16) | Axiom 1 | ∀a: ¬Sa=0 | |||||||||
| (17) | Spezialisierung (16) a ← (a+b) | ¬S(a+b)=0 | |||||||||
| (18) | Hypothese | (a+Sb)=0 | |||||||||
| (19) | Übernahme (15) | S(a+b)=(a+Sb) | |||||||||
| (20) | Transitivität (19), (18) | S(a+b)=0 | |||||||||
| (21) | Konklusion (18), (20) | <(a+Sb)=0 ⇒ S(a+b)=0> | |||||||||
| (22) | Kontraposition (21) | <¬S(a+b)=0 ⇒ ¬(a+Sb)=0> | |||||||||
| (23) | Modus ponens (22), (17) | ¬(a+Sb)=0 | |||||||||
| (24) | Hypothese | <(a+b)=0 ⇒ <a=0∧b=0>> | |||||||||
| (25) | Hypothese | ¬<a=0∧Sb=0> | |||||||||
| (26) | Übernahme (23) | ¬(a+Sb)=0 | |||||||||
| (27) | Konklusion (25), (26) | <¬<a=0∧Sb=0> ⇒ ¬(a+Sb)=0> | |||||||||
| (28) | Kontraposition (27) | <¬¬(a+Sb)=0 ⇒ ¬¬<a=0∧Sb=0>> | |||||||||
| (29) | Hypothese | (a+Sb)=0 | |||||||||
| (30) | Doppelte Negation (29) | ¬¬(a+Sb)=0 | |||||||||
| (31) | Übernahme (28) | <¬¬(a+Sb)=0 ⇒ ¬¬<a=0∧Sb=0>> | |||||||||
| (32) | Modus ponens (31), (30) | ¬¬<a=0∧Sb=0> | |||||||||
| (33) | Doppelte Negation (32) | <a=0∧Sb=0> | |||||||||
| (34) | Konklusion (29), (33) | <(a+Sb)=0 ⇒ <a=0∧Sb=0>> | |||||||||
| (35) | Konklusion (24), (34) | <<(a+b)=0 ⇒ <a=0∧b=0>> ⇒ <(a+Sb)=0 ⇒ <a=0∧Sb=0>>> | |||||||||
| (36) | Verallgemeinerung (35) nach b | ∀b: <<(a+b)=0 ⇒ <a=0∧b=0>> ⇒ <(a+Sb)=0 ⇒ <a=0∧Sb=0>>> | |||||||||
| (37) | Induktion (11), (36) | ∀b: <(a+b)=0 ⇒ <a=0∧b=0>> | |||||||||
| (38) | Verallgemeinerung (37) nach a | ∀a: ∀b: <(a+b)=0 ⇒ <a=0∧b=0>> | |||||||||
Interpretation:
Eine Summe ist nur dann 0, wenn beide Summanden 0 sind