Es gelten die allgemeinen Vorbemerkungen.
| (1) | Axiom 5 | ∀a: ∀b: (a·Sb)=((a·b)+a) | |||||||||
| (2) | Spezialisierung (1) a ← Sa | ∀b: (Sa·Sb)=((Sa·b)+Sa) | |||||||||
| (3) | Spezialisierung (2) b ← b | (Sa·Sb)=((Sa·b)+Sa) | |||||||||
| (4) | Spezialisierung (1) a ← a | ∀b: (a·Sb)=((a·b)+a) | |||||||||
| (5) | Spezialisierung (4) b ← b | (a·Sb)=((a·b)+a) | |||||||||
| (6) | Theorem 12 | ∀a: ∀b: ∀c: (a+(b+c))=((a+b)+c) | |||||||||
| (7) | Spezialisierung (6) a ← (a·d) | ∀b: ∀c: ((a·d)+(b+c))=(((a·d)+b)+c) | |||||||||
| (8) | Spezialisierung (7) b ← a | ∀c: ((a·d)+(a+c))=(((a·d)+a)+c) | |||||||||
| (9) | Spezialisierung (8) c ← Sb | ((a·d)+(a+Sb))=(((a·d)+a)+Sb) | |||||||||
| (10) | Verallgemeinerung (9) nach d | ∀d: ((a·d)+(a+Sb))=(((a·d)+a)+Sb) | |||||||||
| (11) | Spezialisierung (10) d ← b | ((a·b)+(a+Sb))=(((a·b)+a)+Sb) | |||||||||
| (12) | Spezialisierung (6) a ← (a·b) | ∀b: ∀c: ((a·b)+(b+c))=(((a·b)+b)+c) | |||||||||
| (13) | Spezialisierung (12) b ← b | ∀c: ((a·b)+(b+c))=(((a·b)+b)+c) | |||||||||
| (14) | Spezialisierung (13) c ← Sa | ((a·b)+(b+Sa))=(((a·b)+b)+Sa) | |||||||||
| (15) | Symmetrie (14) | (((a·b)+b)+Sa)=((a·b)+(b+Sa)) | |||||||||
| (16) | Theorem 10 | ∀a: ∀b: ∀c: ∀d: <<a=c∧b=d> ⇒ (a+b)=(c+d)> | |||||||||
| (17) | Spezialisierung (16) a ← c | ∀b: ∀c: ∀d: <<c=c∧b=d> ⇒ (c+b)=(c+d)> | |||||||||
| (18) | Spezialisierung (17) b ← (b+Sa) | ∀c: ∀d: <<c=c∧(b+Sa)=d> ⇒ (c+(b+Sa))=(c+d)> | |||||||||
| (19) | Spezialisierung (18) c ← (a·b) | ∀d: <<(a·b)=(a·b)∧(b+Sa)=d> ⇒ ((a·b)+(b+Sa))=((a·b)+d)> | |||||||||
| (20) | Spezialisierung (19) d ← (a+Sb) | <<(a·b)=(a·b)∧(b+Sa)=(a+Sb)> ⇒ ((a·b)+(b+Sa))=((a·b)+(a+Sb))> | |||||||||
| (21) | Theorem 1 | ∀a: a=a | |||||||||
| (22) | Spezialisierung (21) a ← (a·b) | (a·b)=(a·b) | |||||||||
| (23) | Theorem 7 | ∀a: ∀b: (a+Sb)=(Sa+b) | |||||||||
| (24) | Spezialisierung (23) a ← a | ∀b: (a+Sb)=(Sa+b) | |||||||||
| (25) | Spezialisierung (24) b ← b | (a+Sb)=(Sa+b) | |||||||||
| (26) | Theorem 8 | ∀a: ∀b: (a+b)=(b+a) | |||||||||
| (27) | Spezialisierung (26) a ← Sa | ∀b: (Sa+b)=(b+Sa) | |||||||||
| (28) | Spezialisierung (27) b ← b | (Sa+b)=(b+Sa) | |||||||||
| (29) | Transitivität (25), (28) | (a+Sb)=(b+Sa) | |||||||||
| (30) | Symmetrie (29) | (b+Sa)=(a+Sb) | |||||||||
| (31) | Konjunktion (22), (30) | <(a·b)=(a·b)∧(b+Sa)=(a+Sb)> | |||||||||
| (32) | Modus ponens (20), (31) | ((a·b)+(b+Sa))=((a·b)+(a+Sb)) | |||||||||
| (33) | Transitivität (15), (32) | (((a·b)+b)+Sa)=((a·b)+(a+Sb)) | |||||||||
| (34) | Transitivität (33), (11) | (((a·b)+b)+Sa)=(((a·b)+a)+Sb) | |||||||||
| (35) | Theorem 9 | ∀a: ∀b: ∀c: <a=b ⇒ (a+c)=(b+c)> | |||||||||
| (36) | Spezialisierung (35) a ← ((a·d)+a) | ∀b: ∀c: <((a·d)+a)=b ⇒ (((a·d)+a)+c)=(b+c)> | |||||||||
| (37) | Spezialisierung (36) b ← (a·Sb) | ∀c: <((a·d)+a)=(a·Sb) ⇒ (((a·d)+a)+c)=((a·Sb)+c)> | |||||||||
| (38) | Spezialisierung (37) c ← Sb | <((a·d)+a)=(a·Sb) ⇒ (((a·d)+a)+Sb)=((a·Sb)+Sb)> | |||||||||
| (39) | Verallgemeinerung (38) nach d | ∀d: <((a·d)+a)=(a·Sb) ⇒ (((a·d)+a)+Sb)=((a·Sb)+Sb)> | |||||||||
| (40) | Spezialisierung (39) d ← b | <((a·b)+a)=(a·Sb) ⇒ (((a·b)+a)+Sb)=((a·Sb)+Sb)> | |||||||||
| (41) | Symmetrie (5) | ((a·b)+a)=(a·Sb) | |||||||||
| (42) | Modus ponens (40), (41) | (((a·b)+a)+Sb)=((a·Sb)+Sb) | |||||||||
| (43) | Transitivität (34), (42) | (((a·b)+b)+Sa)=((a·Sb)+Sb) | |||||||||
| (44) | Spezialisierung (35) a ← d | ∀b: ∀c: <d=b ⇒ (d+c)=(b+c)> | |||||||||
| (45) | Spezialisierung (44) b ← ((a·b)+b) | ∀c: <d=((a·b)+b) ⇒ (d+c)=(((a·b)+b)+c)> | |||||||||
| (46) | Spezialisierung (45) c ← Sa | <d=((a·b)+b) ⇒ (d+Sa)=(((a·b)+b)+Sa)> | |||||||||
| (47) | Verallgemeinerung (46) nach d | ∀d: <d=((a·b)+b) ⇒ (d+Sa)=(((a·b)+b)+Sa)> | |||||||||
| (48) | Spezialisierung (47) d ← (Sa·b) | <(Sa·b)=((a·b)+b) ⇒ ((Sa·b)+Sa)=(((a·b)+b)+Sa)> | |||||||||
| (49) | Hypothese | (Sa·b)=((a·b)+b) | |||||||||
| (50) | Übernahme (48) | <(Sa·b)=((a·b)+b) ⇒ ((Sa·b)+Sa)=(((a·b)+b)+Sa)> | |||||||||
| (51) | Modus ponens (50), (49) | ((Sa·b)+Sa)=(((a·b)+b)+Sa) | |||||||||
| (52) | Übernahme (3) | (Sa·Sb)=((Sa·b)+Sa) | |||||||||
| (53) | Transitivität (52), (51) | (Sa·Sb)=(((a·b)+b)+Sa) | |||||||||
| (54) | Übernahme (43) | (((a·b)+b)+Sa)=((a·Sb)+Sb) | |||||||||
| (55) | Transitivität (53), (54) | (Sa·Sb)=((a·Sb)+Sb) | |||||||||
| (56) | Konklusion (49), (55) | <(Sa·b)=((a·b)+b) ⇒ (Sa·Sb)=((a·Sb)+Sb)> | |||||||||
| (57) | Verallgemeinerung (56) nach b | ∀b: <(Sa·b)=((a·b)+b) ⇒ (Sa·Sb)=((a·Sb)+Sb)> | |||||||||
| (58) | Axiom 4 | ∀a: (a·0)=0 | |||||||||
| (59) | Spezialisierung (58) a ← a | (a·0)=0 | |||||||||
| (60) | Spezialisierung (58) a ← Sa | (Sa·0)=0 | |||||||||
| (61) | Spezialisierung (35) a ← (a·0) | ∀b: ∀c: <(a·0)=b ⇒ ((a·0)+c)=(b+c)> | |||||||||
| (62) | Spezialisierung (61) b ← 0 | ∀c: <(a·0)=0 ⇒ ((a·0)+c)=(0+c)> | |||||||||
| (63) | Spezialisierung (62) c ← 0 | <(a·0)=0 ⇒ ((a·0)+0)=(0+0)> | |||||||||
| (64) | Modus ponens (63), (59) | ((a·0)+0)=(0+0) | |||||||||
| (65) | Axiom 2 | ∀a: (a+0)=a | |||||||||
| (66) | Spezialisierung (65) a ← 0 | (0+0)=0 | |||||||||
| (67) | Transitivität (64), (66) | ((a·0)+0)=0 | |||||||||
| (68) | Symmetrie (67) | 0=((a·0)+0) | |||||||||
| (69) | Transitivität (60), (68) | (Sa·0)=((a·0)+0) | |||||||||
| (70) | Induktion (69), (57) | ∀b: (Sa·b)=((a·b)+b) | |||||||||
| (71) | Verallgemeinerung (70) nach a | ∀a: ∀b: (Sa·b)=((a·b)+b) | |||||||||