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