Beweis von Theorem 44

Es gelten die allgemeinen Vorbemerkungen.

(1) Axiom 5 ∀a: ∀b: (a·Sb)=((a·b)+a)
(2) Spezialisierung (1) aSe ∀b: (Se·Sb)=((Se·b)+Se)
(3) Spezialisierung (2) bf (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) be ((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) aa a=a
(11) Theorem 18 ∀a: ∀b: ∀c: ∀d: <<a=c∧b=d> ⇒ (a·b)=(c·d)>
(12) Spezialisierung (11) ac ∀b: ∀c: ∀d: <<c=c∧b=d> ⇒ (c·b)=(c·d)>
(13) Spezialisierung (12) bS((Se·f)+e) ∀c: ∀d: <<c=c∧S((Se·f)+e)=d> ⇒ (c·S((Se·f)+e))=(c·d)>
(14) Spezialisierung (13) ca ∀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>

Übersicht