Beweis von Theorem 11

Es gelten die allgemeinen Vorbemerkungen.

(1) Theorem 10 ∀a: ∀b: ∀c: ∀d: <<a=c∧b=d> ⇒ (a+b)=(c+d)>
(2) Spezialisierung (1) ac ∀b: ∀c: ∀d: <<c=c∧b=d> ⇒ (c+b)=(c+d)>
(3) Spezialisierung (2) bb ∀c: ∀d: <<c=c∧b=d> ⇒ (c+b)=(c+d)>
(4) Spezialisierung (3) ca ∀d: <<a=a∧b=d> ⇒ (a+b)=(a+d)>
(5) Spezialisierung (4) d0 <<a=a∧b=0> ⇒ (a+b)=(a+0)>
(6) Theorem 1 ∀a: a=a
(7) Spezialisierung (6) aa a=a
(8) Axiom 2 ∀a: (a+0)=a
(9) Spezialisierung (8) aa (a+0)=a
(10) Hypothese  b=0
(11) Übernahme (7)  a=a
(12) Konjunktion (11), (10)  <a=a∧b=0>
(13) Übernahme (5)  <<a=a∧b=0> ⇒ (a+b)=(a+0)>
(14) Modus ponens (13), (12)  (a+b)=(a+0)
(15) Übernahme (9)  (a+0)=a
(16) Transitivität (14), (15)  (a+b)=a
(17) Konklusion (10), (16) <b=0 ⇒ (a+b)=a>
(18) Verallgemeinerung (17) nach b ∀b: <b=0 ⇒ (a+b)=a>
(19) Verallgemeinerung (18) nach a ∀a: ∀b: <b=0 ⇒ (a+b)=a>

Interpretation:

Axiom 2 in Funktionsinterpretation

Übersicht