Es gelten die allgemeinen Vorbemerkungen.
(1) | Axiom 5 | ∀a: ∀b: (a·Sb)=((a·b)+a) | |||||||||
(2) | Spezialisierung (1) a ← Se | ∀b: (Se·Sb)=((Se·b)+Se) | |||||||||
(3) | Spezialisierung (2) b ← f | (Se·Sf)=((Se·f)+Se) | |||||||||
(4) | Axiom 3 | ∀a: ∀b: (a+Sb)=S(a+b) | |||||||||
(5) | Spezialisierung (4) a ← (Se·f) | ∀b: ((Se·f)+Sb)=S((Se·f)+b) | |||||||||
(6) | Spezialisierung (5) b ← e | ((Se·f)+Se)=S((Se·f)+e) | |||||||||
(7) | Transitivität (3), (6) | (Se·Sf)=S((Se·f)+e) | |||||||||
(8) | Symmetrie (7) | S((Se·f)+e)=(Se·Sf) | |||||||||
(9) | Theorem 1 | ∀a: a=a | |||||||||
(10) | Spezialisierung (9) a ← a | a=a | |||||||||
(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 ← S((Se·f)+e) | ∀c: ∀d: <<c=c∧S((Se·f)+e)=d> ⇒ (c·S((Se·f)+e))=(c·d)> | |||||||||
(14) | Spezialisierung (13) c ← a | ∀d: <<a=a∧S((Se·f)+e)=d> ⇒ (a·S((Se·f)+e))=(a·d)> | |||||||||
(15) | Spezialisierung (14) d ← (Se·Sf) | <<a=a∧S((Se·f)+e)=(Se·Sf)> ⇒ (a·S((Se·f)+e))=(a·(Se·Sf))> | |||||||||
(16) | Konjunktion (10), (8) | <a=a∧S((Se·f)+e)=(Se·Sf)> | |||||||||
(17) | Modus ponens (15), (16) | (a·S((Se·f)+e))=(a·(Se·Sf)) | |||||||||
(18) | Hypothese | (a·(Se·Sf))=c | |||||||||
(19) | Übernahme (17) | (a·S((Se·f)+e))=(a·(Se·Sf)) | |||||||||
(20) | Transitivität (19), (18) | (a·S((Se·f)+e))=c | |||||||||
(21) | Konklusion (18), (20) | <(a·(Se·Sf))=c ⇒ (a·S((Se·f)+e))=c> | |||||||||
(22) | Kontraposition (21) | <¬(a·S((Se·f)+e))=c ⇒ ¬(a·(Se·Sf))=c> | |||||||||
(23) | Hypothese | ∀d: ¬(a·Sd)=c | |||||||||
(24) | Spezialisierung (23) d ← ((Se·f)+e) | ¬(a·S((Se·f)+e))=c | |||||||||
(25) | Übernahme (22) | <¬(a·S((Se·f)+e))=c ⇒ ¬(a·(Se·Sf))=c> | |||||||||
(26) | Modus ponens (25), (24) | ¬(a·(Se·Sf))=c | |||||||||
(27) | Verallgemeinerung (26) nach f | ∀f: ¬(a·(Se·Sf))=c | |||||||||
(28) | Verallgemeinerung (27) nach e | ∀e: ∀f: ¬(a·(Se·Sf))=c | |||||||||
(29) | Konklusion (23), (28) | <∀d: ¬(a·Sd)=c ⇒ ∀e: ∀f: ¬(a·(Se·Sf))=c> | |||||||||
(30) | Kontraposition (29) | <¬∀e: ∀f: ¬(a·(Se·Sf))=c ⇒ ¬∀d: ¬(a·Sd)=c> |