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