Es gelten die allgemeinen Vorbemerkungen.
| c<=a => c|b | |||||||||||
| (1) | Theorem 47 | ∀a: ∀b: <<¬∀d: ¬(a+d)=Sb∧¬a=Sb> ⇒ ¬∀d: ¬(a+d)=b> | |||||||||
| (2) | Spezialisierung (1) a ← c | ∀b: <<¬∀d: ¬(c+d)=Sb∧¬c=Sb> ⇒ ¬∀d: ¬(c+d)=b> | |||||||||
| (3) | Spezialisierung (2) b ← a | <<¬∀d: ¬(c+d)=Sa∧¬c=Sa> ⇒ ¬∀d: ¬(c+d)=a> | |||||||||
| (4) | Axiom 5 | ∀a: ∀b: (a·Sb)=((a·b)+a) | |||||||||
| (5) | Spezialisierung (4) a ← Sd | ∀b: (Sd·Sb)=((Sd·b)+Sd) | |||||||||
| (6) | Spezialisierung (5) b ← a | (Sd·Sa)=((Sd·a)+Sd) | |||||||||
| (7) | Axiom 3 | ∀a: ∀b: (a+Sb)=S(a+b) | |||||||||
| (8) | Spezialisierung (7) a ← (Sd·a) | ∀b: ((Sd·a)+Sb)=S((Sd·a)+b) | |||||||||
| (9) | Spezialisierung (8) b ← d | ((Sd·a)+Sd)=S((Sd·a)+d) | |||||||||
| (10) | Transitivität (6), (9) | (Sd·Sa)=S((Sd·a)+d) | |||||||||
| (11) | Theorem 18 | ∀a: ∀b: ∀c: ∀d: <<a=c∧b=d> ⇒ (a·b)=(c·d)> | |||||||||
| (12) | Spezialisierung (11) a ← c | ∀b: ∀c: ∀d: <<c=c∧b=d> ⇒ (c·b)=(c·d)> | |||||||||
| (13) | Spezialisierung (12) b ← (Sb·Sa) | ∀c: ∀d: <<c=c∧(Sb·Sa)=d> ⇒ (c·(Sb·Sa))=(c·d)> | |||||||||
| (14) | Spezialisierung (13) c ← c | ∀d: <<c=c∧(Sb·Sa)=d> ⇒ (c·(Sb·Sa))=(c·d)> | |||||||||
| (15) | Spezialisierung (14) d ← S((Sb·a)+b) | <<c=c∧(Sb·Sa)=S((Sb·a)+b)> ⇒ (c·(Sb·Sa))=(c·S((Sb·a)+b))> | |||||||||
| (16) | Verallgemeinerung (15) nach b | ∀b: <<c=c∧(Sb·Sa)=S((Sb·a)+b)> ⇒ (c·(Sb·Sa))=(c·S((Sb·a)+b))> | |||||||||
| (17) | Spezialisierung (16) b ← d | <<c=c∧(Sd·Sa)=S((Sd·a)+d)> ⇒ (c·(Sd·Sa))=(c·S((Sd·a)+d))> | |||||||||
| (18) | Theorem 1 | ∀a: a=a | |||||||||
| (19) | Spezialisierung (18) a ← c | c=c | |||||||||
| (20) | Konjunktion (19), (10) | <c=c∧(Sd·Sa)=S((Sd·a)+d)> | |||||||||
| (21) | Modus ponens (17), (20) | (c·(Sd·Sa))=(c·S((Sd·a)+d)) | |||||||||
| (22) | Symmetrie (21) | (c·S((Sd·a)+d))=(c·(Sd·Sa)) | |||||||||
| (23) | Hypothese | ∀c: <¬∀d: ¬(c+d)=a ⇒ ¬∀d: ¬(c·Sd)=b> | |||||||||
| (24) | Spezialisierung (23) c ← c | <¬∀d: ¬(c+d)=a ⇒ ¬∀d: ¬(c·Sd)=b> | |||||||||
| (25) | Hypothese | ¬∀d: ¬(c+d)=Sa | |||||||||
| (26) | Hypothese | ¬c=Sa | |||||||||
| (27) | Übernahme (25) | ¬∀d: ¬(c+d)=Sa | |||||||||
| (28) | Konjunktion (27), (26) | <¬∀d: ¬(c+d)=Sa∧¬c=Sa> | |||||||||
| (29) | Übernahme (3) | <<¬∀d: ¬(c+d)=Sa∧¬c=Sa> ⇒ ¬∀d: ¬(c+d)=a> | |||||||||
| (30) | Modus ponens (29), (28) | ¬∀d: ¬(c+d)=a | |||||||||
| (31) | Übernahme (24) | <¬∀d: ¬(c+d)=a ⇒ ¬∀d: ¬(c·Sd)=b> | |||||||||
| (32) | Modus ponens (31), (30) | ¬∀d: ¬(c·Sd)=b | |||||||||
| (33) | Hypothese | ∀d: ¬(c·Sd)=(b·Sa) | |||||||||
| (34) | Spezialisierung (33) d ← ((Sd·a)+d) | ¬(c·S((Sd·a)+d))=(b·Sa) | |||||||||
| (35) | Hypothese | (c·(Sd·Sa))=(b·Sa) | |||||||||
| (36) | Übernahme (22) | (c·S((Sd·a)+d))=(c·(Sd·Sa)) | |||||||||
| (37) | Transitivität (36), (35) | (c·S((Sd·a)+d))=(b·Sa) | |||||||||
| (38) | Konklusion (35), (37) | <(c·(Sd·Sa))=(b·Sa) ⇒ (c·S((Sd·a)+d))=(b·Sa)> | |||||||||
| (39) | Kontraposition (38) | <¬(c·S((Sd·a)+d))=(b·Sa) ⇒ ¬(c·(Sd·Sa))=(b·Sa)> | |||||||||
| (40) | Modus ponens (39), (34) | ¬(c·(Sd·Sa))=(b·Sa) | |||||||||
| (41) | Hypothese | (c·Sd)=b | |||||||||
| (42) | - unbewiesen - | <<(c·Sd)=b∧Sa=Sa> ⇒ ((c·Sd)·Sa)==(b·Sa)> | |||||||||
Fehlerhafter Beweis!