Es gelten die allgemeinen Vorbemerkungen.
| (1) | Theorem 5 | ∀a: (0+a)=a | |||||||||
| (2) | Axiom 2 | ∀a: (a+0)=a | |||||||||
| (3) | Spezialisierung (1) a ← a | (0+a)=a | |||||||||
| (4) | Spezialisierung (2) a ← a | (a+0)=a | |||||||||
| (5) | Symmetrie (3) | a=(0+a) | |||||||||
| (6) | Transitivität (4), (5) | (a+0)=(0+a) | |||||||||
| (7) | Theorem 6 | ∀a: ∀b: (Sa+b)=S(a+b) | |||||||||
| (8) | Spezialisierung (7) a ← c | ∀b: (Sc+b)=S(c+b) | |||||||||
| (9) | Spezialisierung (8) b ← a | (Sc+a)=S(c+a) | |||||||||
| (10) | Verallgemeinerung (9) nach c | ∀c: (Sc+a)=S(c+a) | |||||||||
| (11) | Spezialisierung (10) c ← b | (Sb+a)=S(b+a) | |||||||||
| (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) | Hypothese | (a+b)=(b+a) | |||||||||
| (16) | Übernahme (14) | (a+Sb)=S(a+b) | |||||||||
| (17) | Übernahme (11) | (Sb+a)=S(b+a) | |||||||||
| (18) | Symmetrie (17) | S(b+a)=(Sb+a) | |||||||||
| (19) | S hinzufügen (15) | S(a+b)=S(b+a) | |||||||||
| (20) | Transitivität (16), (19) | (a+Sb)=S(b+a) | |||||||||
| (21) | Transitivität (20), (18) | (a+Sb)=(Sb+a) | |||||||||
| (22) | Konklusion (15), (21) | <(a+b)=(b+a) ⇒ (a+Sb)=(Sb+a)> | |||||||||
| (23) | Verallgemeinerung (22) nach b | ∀b: <(a+b)=(b+a) ⇒ (a+Sb)=(Sb+a)> | |||||||||
| (24) | Induktion (6), (23) | ∀b: (a+b)=(b+a) | |||||||||
| (25) | Verallgemeinerung (24) nach a | ∀a: ∀b: (a+b)=(b+a) | |||||||||
Interpretation:
Addition ist kommutativ