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) | Spezialisierung (1) a ← b | (b+0)=b | |||||||||
| (5) | Hypothese | (a+0)=(b+0) | |||||||||
| (6) | Übernahme (3) | a=(a+0) | |||||||||
| (7) | Übernahme (4) | (b+0)=b | |||||||||
| (8) | Transitivität (6), (5) | a=(b+0) | |||||||||
| (9) | Transitivität (8), (7) | a=b | |||||||||
| (10) | Konklusion (5), (9) | <(a+0)=(b+0) ⇒ a=b> | |||||||||
| (11) | Axiom 3 | ∀a: ∀b: (a+Sb)=S(a+b) | |||||||||
| (12) | Spezialisierung (11) a ← a | ∀b: (a+Sb)=S(a+b) | |||||||||
| (13) | Spezialisierung (12) b ← c | (a+Sc)=S(a+c) | |||||||||
| (14) | Symmetrie (13) | S(a+c)=(a+Sc) | |||||||||
| (15) | Verallgemeinerung (13) nach a | ∀a: (a+Sc)=S(a+c) | |||||||||
| (16) | Spezialisierung (15) a ← b | (b+Sc)=S(b+c) | |||||||||
| (17) | Hypothese | <(a+c)=(b+c) ⇒ a=b> | |||||||||
| (18) | Hypothese | (a+Sc)=(b+Sc) | |||||||||
| (19) | Übernahme (14) | S(a+c)=(a+Sc) | |||||||||
| (20) | Übernahme (16) | (b+Sc)=S(b+c) | |||||||||
| (21) | Transitivität (19), (18) | S(a+c)=(b+Sc) | |||||||||
| (22) | Transitivität (21), (20) | S(a+c)=S(b+c) | |||||||||
| (23) | S entfernen (22) | (a+c)=(b+c) | |||||||||
| (24) | Übernahme (17) | <(a+c)=(b+c) ⇒ a=b> | |||||||||
| (25) | Modus ponens (24), (23) | a=b | |||||||||
| (26) | Konklusion (18), (25) | <(a+Sc)=(b+Sc) ⇒ a=b> | |||||||||
| (27) | Konklusion (17), (26) | <<(a+c)=(b+c) ⇒ a=b> ⇒ <(a+Sc)=(b+Sc) ⇒ a=b>> | |||||||||
| (28) | Verallgemeinerung (27) nach c | ∀c: <<(a+c)=(b+c) ⇒ a=b> ⇒ <(a+Sc)=(b+Sc) ⇒ a=b>> | |||||||||
| (29) | Induktion (10), (28) | ∀c: <(a+c)=(b+c) ⇒ a=b> | |||||||||
| (30) | Verallgemeinerung (29) nach b | ∀b: ∀c: <(a+c)=(b+c) ⇒ a=b> | |||||||||
| (31) | Verallgemeinerung (30) nach a | ∀a: ∀b: ∀c: <(a+c)=(b+c) ⇒ a=b> | |||||||||
Interpretation:
Kürzungsregel für Summanden