Es gelten die allgemeinen Vorbemerkungen.
| (1) | Axiom 2 | ∀a: (a+0)=a | |||||||||
| (2) | Spezialisierung (1) a ← a | (a+0)=a | |||||||||
| (3) | Spezialisierung (1) a ← b | (b+0)=b | |||||||||
| (4) | Symmetrie (3) | b=(b+0) | |||||||||
| (5) | Axiom 3 | ∀a: ∀b: (a+Sb)=S(a+b) | |||||||||
| (6) | Spezialisierung (5) a ← a | ∀b: (a+Sb)=S(a+b) | |||||||||
| (7) | Spezialisierung (6) b ← c | (a+Sc)=S(a+c) | |||||||||
| (8) | Verallgemeinerung (7) nach a | ∀a: (a+Sc)=S(a+c) | |||||||||
| (9) | Spezialisierung (8) a ← b | (b+Sc)=S(b+c) | |||||||||
| (10) | Hypothese | a=b | |||||||||
| (11) | Übernahme (2) | (a+0)=a | |||||||||
| (12) | Transitivität (11), (10) | (a+0)=b | |||||||||
| (13) | Übernahme (4) | b=(b+0) | |||||||||
| (14) | Transitivität (12), (13) | (a+0)=(b+0) | |||||||||
| (15) | Konklusion (10), (14) | <a=b ⇒ (a+0)=(b+0)> | |||||||||
| (16) | Hypothese | <a=b ⇒ (a+c)=(b+c)> | |||||||||
| (17) | Hypothese | a=b | |||||||||
| (18) | Übernahme (7) | (a+Sc)=S(a+c) | |||||||||
| (19) | Übernahme (9) | (b+Sc)=S(b+c) | |||||||||
| (20) | Übernahme (16) | <a=b ⇒ (a+c)=(b+c)> | |||||||||
| (21) | Modus ponens (20), (17) | (a+c)=(b+c) | |||||||||
| (22) | S hinzufügen (21) | S(a+c)=S(b+c) | |||||||||
| (23) | Transitivität (18), (22) | (a+Sc)=S(b+c) | |||||||||
| (24) | Symmetrie (19) | S(b+c)=(b+Sc) | |||||||||
| (25) | Transitivität (23), (24) | (a+Sc)=(b+Sc) | |||||||||
| (26) | Konklusion (17), (25) | <a=b ⇒ (a+Sc)=(b+Sc)> | |||||||||
| (27) | Konklusion (16), (26) | <<a=b ⇒ (a+c)=(b+c)> ⇒ <a=b ⇒ (a+Sc)=(b+Sc)>> | |||||||||
| (28) | Verallgemeinerung (27) nach c | ∀c: <<a=b ⇒ (a+c)=(b+c)> ⇒ <a=b ⇒ (a+Sc)=(b+Sc)>> | |||||||||
| (29) | Induktion (15), (28) | ∀c: <a=b ⇒ (a+c)=(b+c)> | |||||||||
| (30) | Verallgemeinerung (29) nach b | ∀b: ∀c: <a=b ⇒ (a+c)=(b+c)> | |||||||||
| (31) | Verallgemeinerung (30) nach a | ∀a: ∀b: ∀c: <a=b ⇒ (a+c)=(b+c)> | |||||||||
Interpretation:
Addition ist eine Funktion im ersten Summanden