Beweis von Theorem 4

Es gelten die allgemeinen Vorbemerkungen.

(1) Axiom 2 ∀a: (a+0)=a
(2) Spezialisierung (1) aa (a+0)=a
(3) Symmetrie (2) a=(a+0)
(4) Theorem 1 ∀a: a=a
(5) Spezialisierung (4) a0 0=0
(6) Hypothese  (a+0)=0
(7) Übernahme (3)  a=(a+0)
(8) Transitivität (7), (6)  a=0
(9) Übernahme (5)  0=0
(10) Konjunktion (8), (9)  <a=0∧0=0>
(11) Konklusion (6), (10) <(a+0)=0 ⇒ <a=0∧0=0>>
(12) Axiom 3 ∀a: ∀b: (a+Sb)=S(a+b)
(13) Spezialisierung (12) aa ∀b: (a+Sb)=S(a+b)
(14) Spezialisierung (13) bb (a+Sb)=S(a+b)
(15) Symmetrie (14) S(a+b)=(a+Sb)
(16) Axiom 1 ∀a: ¬Sa=0
(17) Spezialisierung (16) a(a+b) ¬S(a+b)=0
(18) Hypothese  (a+Sb)=0
(19) Übernahme (15)  S(a+b)=(a+Sb)
(20) Transitivität (19), (18)  S(a+b)=0
(21) Konklusion (18), (20) <(a+Sb)=0 ⇒ S(a+b)=0>
(22) Kontraposition (21) <¬S(a+b)=0 ⇒ ¬(a+Sb)=0>
(23) Modus ponens (22), (17) ¬(a+Sb)=0
(24) Hypothese  <(a+b)=0 ⇒ <a=0∧b=0>>
(25) Hypothese   ¬<a=0∧Sb=0>
(26) Übernahme (23)   ¬(a+Sb)=0
(27) Konklusion (25), (26)  <¬<a=0∧Sb=0> ⇒ ¬(a+Sb)=0>
(28) Kontraposition (27)  <¬¬(a+Sb)=0 ⇒ ¬¬<a=0∧Sb=0>>
(29) Hypothese   (a+Sb)=0
(30) Doppelte Negation (29)   ¬¬(a+Sb)=0
(31) Übernahme (28)   <¬¬(a+Sb)=0 ⇒ ¬¬<a=0∧Sb=0>>
(32) Modus ponens (31), (30)   ¬¬<a=0∧Sb=0>
(33) Doppelte Negation (32)   <a=0∧Sb=0>
(34) Konklusion (29), (33)  <(a+Sb)=0 ⇒ <a=0∧Sb=0>>
(35) Konklusion (24), (34) <<(a+b)=0 ⇒ <a=0∧b=0>> ⇒ <(a+Sb)=0 ⇒ <a=0∧Sb=0>>>
(36) Verallgemeinerung (35) nach b ∀b: <<(a+b)=0 ⇒ <a=0∧b=0>> ⇒ <(a+Sb)=0 ⇒ <a=0∧Sb=0>>>
(37) Induktion (11), (36) ∀b: <(a+b)=0 ⇒ <a=0∧b=0>>
(38) Verallgemeinerung (37) nach a ∀a: ∀b: <(a+b)=0 ⇒ <a=0∧b=0>>

Interpretation:

Eine Summe ist nur dann 0, wenn beide Summanden 0 sind

Übersicht