Es gelten die allgemeinen Vorbemerkungen.
| (1) | Axiom 4 | ∀a: (a·0)=0 | |||||||||
| (2) | Spezialisierung (1) a ← a | (a·0)=0 | |||||||||
| (3) | Hypothese | (a·0)=S0 | |||||||||
| (4) | Symmetrie (3) | S0=(a·0) | |||||||||
| (5) | Übernahme (2) | (a·0)=0 | |||||||||
| (6) | Transitivität (4), (5) | S0=0 | |||||||||
| (7) | Konklusion (3), (6) | <(a·0)=S0 ⇒ S0=0> | |||||||||
| (8) | Kontraposition (7) | <¬S0=0 ⇒ ¬(a·0)=S0> | |||||||||
| (9) | Axiom 1 | ∀a: ¬Sa=0 | |||||||||
| (10) | Spezialisierung (9) a ← 0 | ¬S0=0 | |||||||||
| (11) | Modus ponens (8), (10) | ¬(a·0)=S0 | |||||||||
| (12) | Hypothese | ¬<a=S0∧0=S0> | |||||||||
| (13) | Übernahme (11) | ¬(a·0)=S0 | |||||||||
| (14) | Konklusion (12), (13) | <¬<a=S0∧0=S0> ⇒ ¬(a·0)=S0> | |||||||||
| (15) | Kontraposition (14) | <¬¬(a·0)=S0 ⇒ ¬¬<a=S0∧0=S0>> | |||||||||
| (16) | Hypothese | (a·0)=S0 | |||||||||
| (17) | Doppelte Negation (16) | ¬¬(a·0)=S0 | |||||||||
| (18) | Übernahme (15) | <¬¬(a·0)=S0 ⇒ ¬¬<a=S0∧0=S0>> | |||||||||
| (19) | Modus ponens (18), (17) | ¬¬<a=S0∧0=S0> | |||||||||
| (20) | Doppelte Negation (19) | <a=S0∧0=S0> | |||||||||
| (21) | Konklusion (16), (20) | <(a·0)=S0 ⇒ <a=S0∧0=S0>> | |||||||||
| (22) | Theorem 13 | ∀a: (0·a)=0 | |||||||||
| (23) | Spezialisierung (22) a ← b | (0·b)=0 | |||||||||
| (24) | Hypothese | (0·b)=S0 | |||||||||
| (25) | Symmetrie (24) | S0=(0·b) | |||||||||
| (26) | Übernahme (23) | (0·b)=0 | |||||||||
| (27) | Transitivität (25), (26) | S0=0 | |||||||||
| (28) | Konklusion (24), (27) | <(0·b)=S0 ⇒ S0=0> | |||||||||
| (29) | Kontraposition (28) | <¬S0=0 ⇒ ¬(0·b)=S0> | |||||||||
| (30) | Modus ponens (29), (10) | ¬(0·b)=S0 | |||||||||
| (31) | Hypothese | ¬<0=S0∧b=S0> | |||||||||
| (32) | Übernahme (30) | ¬(0·b)=S0 | |||||||||
| (33) | Konklusion (31), (32) | <¬<0=S0∧b=S0> ⇒ ¬(0·b)=S0> | |||||||||
| (34) | Kontraposition (33) | <¬¬(0·b)=S0 ⇒ ¬¬<0=S0∧b=S0>> | |||||||||
| (35) | Hypothese | (0·b)=S0 | |||||||||
| (36) | Doppelte Negation (35) | ¬¬(0·b)=S0 | |||||||||
| (37) | Übernahme (34) | <¬¬(0·b)=S0 ⇒ ¬¬<0=S0∧b=S0>> | |||||||||
| (38) | Modus ponens (37), (36) | ¬¬<0=S0∧b=S0> | |||||||||
| (39) | Doppelte Negation (38) | <0=S0∧b=S0> | |||||||||
| (40) | Konklusion (35), (39) | <(0·b)=S0 ⇒ <0=S0∧b=S0>> | |||||||||
| (41) | Verallgemeinerung (40) nach b | ∀b: <(0·b)=S0 ⇒ <0=S0∧b=S0>> | |||||||||
| (42) | Spezialisierung (41) b ← Sb | <(0·Sb)=S0 ⇒ <0=S0∧Sb=S0>> | |||||||||
| (43) | Axiom 5 | ∀a: ∀b: (a·Sb)=((a·b)+a) | |||||||||
| (44) | Spezialisierung (43) a ← Sa | ∀b: (Sa·Sb)=((Sa·b)+Sa) | |||||||||
| (45) | Spezialisierung (44) b ← b | (Sa·Sb)=((Sa·b)+Sa) | |||||||||
| (46) | Axiom 3 | ∀a: ∀b: (a+Sb)=S(a+b) | |||||||||
| (47) | Spezialisierung (46) a ← (Sb·c) | ∀b: ((Sb·c)+Sb)=S((Sb·c)+b) | |||||||||
| (48) | Spezialisierung (47) b ← a | ((Sa·c)+Sa)=S((Sa·c)+a) | |||||||||
| (49) | Verallgemeinerung (48) nach c | ∀c: ((Sa·c)+Sa)=S((Sa·c)+a) | |||||||||
| (50) | Spezialisierung (49) c ← b | ((Sa·b)+Sa)=S((Sa·b)+a) | |||||||||
| (51) | Transitivität (45), (50) | (Sa·Sb)=S((Sa·b)+a) | |||||||||
| (52) | Symmetrie (51) | S((Sa·b)+a)=(Sa·Sb) | |||||||||
| (53) | Theorem 4 | ∀a: ∀b: <(a+b)=0 ⇒ <a=0∧b=0>> | |||||||||
| (54) | Spezialisierung (53) a ← (Sa·c) | ∀b: <((Sa·c)+b)=0 ⇒ <(Sa·c)=0∧b=0>> | |||||||||
| (55) | Spezialisierung (54) b ← a | <((Sa·c)+a)=0 ⇒ <(Sa·c)=0∧a=0>> | |||||||||
| (56) | Verallgemeinerung (55) nach c | ∀c: <((Sa·c)+a)=0 ⇒ <(Sa·c)=0∧a=0>> | |||||||||
| (57) | Spezialisierung (56) c ← b | <((Sa·b)+a)=0 ⇒ <(Sa·b)=0∧a=0>> | |||||||||
| (58) | Theorem 29 | ∀a: ∀b: <(Sa·b)=0 ⇒ b=0> | |||||||||
| (59) | Spezialisierung (58) a ← a | ∀b: <(Sa·b)=0 ⇒ b=0> | |||||||||
| (60) | Spezialisierung (59) b ← b | <(Sa·b)=0 ⇒ b=0> | |||||||||
| (61) | Hypothese | (Sa·Sb)=S0 | |||||||||
| (62) | Übernahme (52) | S((Sa·b)+a)=(Sa·Sb) | |||||||||
| (63) | Transitivität (62), (61) | S((Sa·b)+a)=S0 | |||||||||
| (64) | S entfernen (63) | ((Sa·b)+a)=0 | |||||||||
| (65) | Übernahme (57) | <((Sa·b)+a)=0 ⇒ <(Sa·b)=0∧a=0>> | |||||||||
| (66) | Modus ponens (65), (64) | <(Sa·b)=0∧a=0> | |||||||||
| (67) | Abtrennung II (66) | a=0 | |||||||||
| (68) | Abtrennung I (66) | (Sa·b)=0 | |||||||||
| (69) | Übernahme (60) | <(Sa·b)=0 ⇒ b=0> | |||||||||
| (70) | Modus ponens (69), (68) | b=0 | |||||||||
| (71) | S hinzufügen (67) | Sa=S0 | |||||||||
| (72) | S hinzufügen (70) | Sb=S0 | |||||||||
| (73) | Konjunktion (71), (72) | <Sa=S0∧Sb=S0> | |||||||||
| (74) | Konklusion (61), (73) | <(Sa·Sb)=S0 ⇒ <Sa=S0∧Sb=S0>> | |||||||||
| (75) | Hypothese | <(a·Sb)=S0 ⇒ <a=S0∧Sb=S0>> | |||||||||
| (76) | Übernahme (74) | <(Sa·Sb)=S0 ⇒ <Sa=S0∧Sb=S0>> | |||||||||
| (77) | Konklusion (75), (76) | <<(a·Sb)=S0 ⇒ <a=S0∧Sb=S0>> ⇒ <(Sa·Sb)=S0 ⇒ <Sa=S0∧Sb=S0>>> | |||||||||
| (78) | Verallgemeinerung (77) nach a | ∀a: <<(a·Sb)=S0 ⇒ <a=S0∧Sb=S0>> ⇒ <(Sa·Sb)=S0 ⇒ <Sa=S0∧Sb=S0>>> | |||||||||
| (79) | Induktion (42), (78) | ∀a: <(a·Sb)=S0 ⇒ <a=S0∧Sb=S0>> | |||||||||
| (80) | Spezialisierung (79) a ← a | <(a·Sb)=S0 ⇒ <a=S0∧Sb=S0>> | |||||||||
| (81) | Hypothese | <(a·b)=S0 ⇒ <a=S0∧b=S0>> | |||||||||
| (82) | Übernahme (80) | <(a·Sb)=S0 ⇒ <a=S0∧Sb=S0>> | |||||||||
| (83) | Konklusion (81), (82) | <<(a·b)=S0 ⇒ <a=S0∧b=S0>> ⇒ <(a·Sb)=S0 ⇒ <a=S0∧Sb=S0>>> | |||||||||
| (84) | Verallgemeinerung (83) nach b | ∀b: <<(a·b)=S0 ⇒ <a=S0∧b=S0>> ⇒ <(a·Sb)=S0 ⇒ <a=S0∧Sb=S0>>> | |||||||||
| (85) | Induktion (21), (84) | ∀b: <(a·b)=S0 ⇒ <a=S0∧b=S0>> | |||||||||
| (86) | Verallgemeinerung (85) nach a | ∀a: ∀b: <(a·b)=S0 ⇒ <a=S0∧b=S0>> | |||||||||