Es gelten die allgemeinen Vorbemerkungen.
| (1) | Theorem 9 | ∀a: ∀b: ∀c: <a=b ⇒ (a+c)=(b+c)> | |||||||||
| (2) | Spezialisierung (1) a ← a | ∀b: ∀c: <a=b ⇒ (a+c)=(b+c)> | |||||||||
| (3) | Spezialisierung (2) b ← (0+a) | ∀c: <a=(0+a) ⇒ (a+c)=((0+a)+c)> | |||||||||
| (4) | Verallgemeinerung (3) nach a | ∀a: ∀c: <a=(0+a) ⇒ (a+c)=((0+a)+c)> | |||||||||
| (5) | Spezialisierung (4) a ← b | ∀c: <b=(0+b) ⇒ (b+c)=((0+b)+c)> | |||||||||
| (6) | Spezialisierung (5) c ← c | <b=(0+b) ⇒ (b+c)=((0+b)+c)> | |||||||||
| (7) | Spezialisierung (1) a ← (Sa+d) | ∀b: ∀c: <(Sa+d)=b ⇒ ((Sa+d)+c)=(b+c)> | |||||||||
| (8) | Spezialisierung (7) b ← S(a+d) | ∀c: <(Sa+d)=S(a+d) ⇒ ((Sa+d)+c)=(S(a+d)+c)> | |||||||||
| (9) | Spezialisierung (8) c ← c | <(Sa+d)=S(a+d) ⇒ ((Sa+d)+c)=(S(a+d)+c)> | |||||||||
| (10) | Verallgemeinerung (9) nach d | ∀d: <(Sa+d)=S(a+d) ⇒ ((Sa+d)+c)=(S(a+d)+c)> | |||||||||
| (11) | Spezialisierung (10) d ← b | <(Sa+b)=S(a+b) ⇒ ((Sa+b)+c)=(S(a+b)+c)> | |||||||||
| (12) | Theorem 5 | ∀a: (0+a)=a | |||||||||
| (13) | Spezialisierung (12) a ← b | (0+b)=b | |||||||||
| (14) | Symmetrie (13) | b=(0+b) | |||||||||
| (15) | Modus ponens (6), (14) | (b+c)=((0+b)+c) | |||||||||
| (16) | Spezialisierung (12) a ← (b+c) | (0+(b+c))=(b+c) | |||||||||
| (17) | Transitivität (16), (15) | (0+(b+c))=((0+b)+c) | |||||||||
| (18) | Theorem 6 | ∀a: ∀b: (Sa+b)=S(a+b) | |||||||||
| (19) | Spezialisierung (18) a ← a | ∀b: (Sa+b)=S(a+b) | |||||||||
| (20) | Spezialisierung (19) b ← (b+c) | (Sa+(b+c))=S(a+(b+c)) | |||||||||
| (21) | Spezialisierung (19) b ← b | (Sa+b)=S(a+b) | |||||||||
| (22) | Spezialisierung (19) b ← c | (Sa+c)=S(a+c) | |||||||||
| (23) | Verallgemeinerung (22) nach a | ∀a: (Sa+c)=S(a+c) | |||||||||
| (24) | Spezialisierung (23) a ← (a+b) | (S(a+b)+c)=S((a+b)+c) | |||||||||
| (25) | Hypothese | (a+(b+c))=((a+b)+c) | |||||||||
| (26) | Übernahme (20) | (Sa+(b+c))=S(a+(b+c)) | |||||||||
| (27) | Übernahme (21) | (Sa+b)=S(a+b) | |||||||||
| (28) | Übernahme (11) | <(Sa+b)=S(a+b) ⇒ ((Sa+b)+c)=(S(a+b)+c)> | |||||||||
| (29) | Modus ponens (28), (27) | ((Sa+b)+c)=(S(a+b)+c) | |||||||||
| (30) | Übernahme (24) | (S(a+b)+c)=S((a+b)+c) | |||||||||
| (31) | Transitivität (29), (30) | ((Sa+b)+c)=S((a+b)+c) | |||||||||
| (32) | Symmetrie (31) | S((a+b)+c)=((Sa+b)+c) | |||||||||
| (33) | S hinzufügen (25) | S(a+(b+c))=S((a+b)+c) | |||||||||
| (34) | Transitivität (26), (33) | (Sa+(b+c))=S((a+b)+c) | |||||||||
| (35) | Transitivität (34), (32) | (Sa+(b+c))=((Sa+b)+c) | |||||||||
| (36) | Konklusion (25), (35) | <(a+(b+c))=((a+b)+c) ⇒ (Sa+(b+c))=((Sa+b)+c)> | |||||||||
| (37) | Verallgemeinerung (36) nach a | ∀a: <(a+(b+c))=((a+b)+c) ⇒ (Sa+(b+c))=((Sa+b)+c)> | |||||||||
| (38) | Induktion (17), (37) | ∀a: (a+(b+c))=((a+b)+c) | |||||||||
| (39) | Spezialisierung (38) a ← a | (a+(b+c))=((a+b)+c) | |||||||||
| (40) | Verallgemeinerung (39) nach c | ∀c: (a+(b+c))=((a+b)+c) | |||||||||
| (41) | Verallgemeinerung (40) nach b | ∀b: ∀c: (a+(b+c))=((a+b)+c) | |||||||||
| (42) | Verallgemeinerung (41) nach a | ∀a: ∀b: ∀c: (a+(b+c))=((a+b)+c) | |||||||||
Interpretation:
Addition ist assoziativ