Es gelten die allgemeinen Vorbemerkungen.
(1) | Theorem 10 | ∀a: ∀b: ∀c: ∀d: <<a=c∧b=d> ⇒ (a+b)=(c+d)> | |||||||||
(2) | Spezialisierung (1) a ← c | ∀b: ∀c: ∀d: <<c=c∧b=d> ⇒ (c+b)=(c+d)> | |||||||||
(3) | Spezialisierung (2) b ← b | ∀c: ∀d: <<c=c∧b=d> ⇒ (c+b)=(c+d)> | |||||||||
(4) | Spezialisierung (3) c ← a | ∀d: <<a=a∧b=d> ⇒ (a+b)=(a+d)> | |||||||||
(5) | Spezialisierung (4) d ← 0 | <<a=a∧b=0> ⇒ (a+b)=(a+0)> | |||||||||
(6) | Theorem 1 | ∀a: a=a | |||||||||
(7) | Spezialisierung (6) a ← a | a=a | |||||||||
(8) | Axiom 2 | ∀a: (a+0)=a | |||||||||
(9) | Spezialisierung (8) a ← a | (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