Es gelten die allgemeinen Vorbemerkungen.
| (1) | Axiom 1 | ∀a: ¬Sa=0 | |||||||||
| (2) | Axiom 2 | ∀a: (a+0)=a | |||||||||
| (3) | Axiom 3 | ∀a: ∀b: (a+Sb)=S(a+b) | |||||||||
| (4) | Spezialisierung (3) a ← a | ∀b: (a+Sb)=S(a+b) | |||||||||
| (5) | Spezialisierung (4) b ← b | (a+Sb)=S(a+b) | |||||||||
| (6) | Spezialisierung (2) a ← a | (a+0)=a | |||||||||
| (7) | Spezialisierung (2) a ← b | (b+0)=b | |||||||||
| (8) | Symmetrie (6) | a=(a+0) | |||||||||
| (9) | Transitivität (8), (6) | a=a | |||||||||
| (10) | Verallgemeinerung (9) nach a | ∀a: a=a | |||||||||
| (11) | Spezialisierung (10) a ← 0 | 0=0 | |||||||||
| (12) | Spezialisierung (10) a ← Sc | Sc=Sc | |||||||||
| (13) | Spezialisierung (4) b ← c | (a+Sc)=S(a+c) | |||||||||
| (14) | Verallgemeinerung (13) nach a | ∀a: (a+Sc)=S(a+c) | |||||||||
| (15) | Spezialisierung (14) a ← b | (b+Sc)=S(b+c) | |||||||||
| (16) | Spezialisierung (3) a ← Sa | ∀b: (Sa+Sb)=S(Sa+b) | |||||||||
| (17) | Spezialisierung (16) b ← b | (Sa+Sb)=S(Sa+b) | |||||||||
| (18) | Spezialisierung (3) a ← 0 | ∀b: (0+Sb)=S(0+b) | |||||||||
| (19) | Spezialisierung (18) b ← a | (0+Sa)=S(0+a) | |||||||||
| (20) | Spezialisierung (4) b ← Sd | (a+SSd)=S(a+Sd) | |||||||||
| (21) | Verallgemeinerung (20) nach a | ∀a: (a+SSd)=S(a+Sd) | |||||||||
| (22) | Spezialisierung (21) a ← b | (b+SSd)=S(b+Sd) | |||||||||
| (23) | Spezialisierung (1) a ← d | ¬Sd=0 | |||||||||
| (24) | Spezialisierung (2) a ← Sa | (Sa+0)=Sa | |||||||||
| (25) | S hinzufügen (8) | Sa=S(a+0) | |||||||||
| (26) | Transitivität (24), (25) | (Sa+0)=S(a+0) | |||||||||
| (27) | Hypothese | (Sa+b)=S(a+b) | |||||||||
| (28) | Übernahme (17) | (Sa+Sb)=S(Sa+b) | |||||||||
| (29) | S hinzufügen (27) | S(Sa+b)=SS(a+b) | |||||||||
| (30) | Transitivität (28), (29) | (Sa+Sb)=SS(a+b) | |||||||||
| (31) | Übernahme (5) | (a+Sb)=S(a+b) | |||||||||
| (32) | S hinzufügen (31) | S(a+Sb)=SS(a+b) | |||||||||
| (33) | Symmetrie (32) | SS(a+b)=S(a+Sb) | |||||||||
| (34) | Transitivität (30), (33) | (Sa+Sb)=S(a+Sb) | |||||||||
| (35) | Konklusion (27), (34) | <(Sa+b)=S(a+b) ⇒ (Sa+Sb)=S(a+Sb)> | |||||||||
| (36) | Verallgemeinerung (35) nach b | ∀b: <(Sa+b)=S(a+b) ⇒ (Sa+Sb)=S(a+Sb)> | |||||||||
| (37) | Induktion (26), (36) | ∀b: (Sa+b)=S(a+b) | |||||||||
| (38) | Spezialisierung (37) b ← c | (Sa+c)=S(a+c) | |||||||||
| (39) | Verallgemeinerung (38) nach a | ∀a: (Sa+c)=S(a+c) | |||||||||
| (40) | Spezialisierung (39) a ← b | (Sb+c)=S(b+c) | |||||||||
| (41) | Verallgemeinerung (40) nach c | ∀c: (Sb+c)=S(b+c) | |||||||||
| (42) | Spezialisierung (41) c ← a | (Sb+a)=S(b+a) | |||||||||
| (43) | Spezialisierung (41) c ← Sd | (Sb+Sd)=S(b+Sd) | |||||||||
| (44) | Spezialisierung (2) a ← 0 | (0+0)=0 | |||||||||
| (45) | Hypothese | (0+a)=a | |||||||||
| (46) | Übernahme (19) | (0+Sa)=S(0+a) | |||||||||
| (47) | S hinzufügen (45) | S(0+a)=Sa | |||||||||
| (48) | Transitivität (46), (47) | (0+Sa)=Sa | |||||||||
| (49) | Konklusion (45), (48) | <(0+a)=a ⇒ (0+Sa)=Sa> | |||||||||
| (50) | Verallgemeinerung (49) nach a | ∀a: <(0+a)=a ⇒ (0+Sa)=Sa> | |||||||||
| (51) | Induktion (44), (50) | ∀a: (0+a)=a | |||||||||
| (52) | Spezialisierung (51) a ← b | (0+b)=b | |||||||||
| (53) | Spezialisierung (51) a ← a | (0+a)=a | |||||||||
| (54) | Symmetrie (53) | a=(0+a) | |||||||||
| (55) | Transitivität (6), (54) | (a+0)=(0+a) | |||||||||
| (56) | Hypothese | (a+b)=(b+a) | |||||||||
| (57) | Übernahme (5) | (a+Sb)=S(a+b) | |||||||||
| (58) | Übernahme (42) | (Sb+a)=S(b+a) | |||||||||
| (59) | Symmetrie (58) | S(b+a)=(Sb+a) | |||||||||
| (60) | S hinzufügen (56) | S(a+b)=S(b+a) | |||||||||
| (61) | Transitivität (57), (60) | (a+Sb)=S(b+a) | |||||||||
| (62) | Transitivität (61), (59) | (a+Sb)=(Sb+a) | |||||||||
| (63) | Konklusion (56), (62) | <(a+b)=(b+a) ⇒ (a+Sb)=(Sb+a)> | |||||||||
| (64) | Verallgemeinerung (63) nach b | ∀b: <(a+b)=(b+a) ⇒ (a+Sb)=(Sb+a)> | |||||||||
| (65) | Induktion (55), (64) | ∀b: (a+b)=(b+a) | |||||||||
| (66) | Spezialisierung (65) b ← c | (a+c)=(c+a) | |||||||||
| (67) | Hypothese | (a+0)=(b+0) | |||||||||
| (68) | Übernahme (7) | (b+0)=b | |||||||||
| (69) | Übernahme (8) | a=(a+0) | |||||||||
| (70) | Transitivität (69), (67) | a=(b+0) | |||||||||
| (71) | Transitivität (70), (68) | a=b | |||||||||
| (72) | Konklusion (67), (71) | <(a+0)=(b+0) ⇒ a=b> | |||||||||
| (73) | Hypothese | <(a+c)=(b+c) ⇒ a=b> | |||||||||
| (74) | Hypothese | (a+Sc)=(b+Sc) | |||||||||
| (75) | Übernahme (13) | (a+Sc)=S(a+c) | |||||||||
| (76) | Übernahme (15) | (b+Sc)=S(b+c) | |||||||||
| (77) | Transitivität (74), (76) | (a+Sc)=S(b+c) | |||||||||
| (78) | Symmetrie (75) | S(a+c)=(a+Sc) | |||||||||
| (79) | Transitivität (78), (77) | S(a+c)=S(b+c) | |||||||||
| (80) | S entfernen (79) | (a+c)=(b+c) | |||||||||
| (81) | Übernahme (73) | <(a+c)=(b+c) ⇒ a=b> | |||||||||
| (82) | Modus ponens (81), (80) | a=b | |||||||||
| (83) | Konklusion (74), (82) | <(a+Sc)=(b+Sc) ⇒ a=b> | |||||||||
| (84) | Konklusion (73), (83) | <<(a+c)=(b+c) ⇒ a=b> ⇒ <(a+Sc)=(b+Sc) ⇒ a=b>> | |||||||||
| (85) | Verallgemeinerung (84) nach c | ∀c: <<(a+c)=(b+c) ⇒ a=b> ⇒ <(a+Sc)=(b+Sc) ⇒ a=b>> | |||||||||
| (86) | Induktion (72), (85) | ∀c: <(a+c)=(b+c) ⇒ a=b> | |||||||||
| (87) | Verallgemeinerung (86) nach b | ∀b: ∀c: <(a+c)=(b+c) ⇒ a=b> | |||||||||
| (88) | Spezialisierung (87) b ← 0 | ∀c: <(a+c)=(0+c) ⇒ a=0> | |||||||||
| (89) | Spezialisierung (88) c ← b | <(a+b)=(0+b) ⇒ a=0> | |||||||||
| (90) | Hypothese | (a+b)=b | |||||||||
| (91) | Übernahme (52) | (0+b)=b | |||||||||
| (92) | Symmetrie (91) | b=(0+b) | |||||||||
| (93) | Transitivität (90), (92) | (a+b)=(0+b) | |||||||||
| (94) | Übernahme (89) | <(a+b)=(0+b) ⇒ a=0> | |||||||||
| (95) | Modus ponens (94), (93) | a=0 | |||||||||
| (96) | Konklusion (90), (95) | <(a+b)=b ⇒ a=0> | |||||||||
| (97) | Verallgemeinerung (96) nach b | ∀b: <(a+b)=b ⇒ a=0> | |||||||||
| (98) | Spezialisierung (97) b ← Sb | <(a+Sb)=Sb ⇒ a=0> | |||||||||
| (99) | Verallgemeinerung (98) nach a | ∀a: <(a+Sb)=Sb ⇒ a=0> | |||||||||
| (100) | Spezialisierung (99) a ← Sd | <(Sd+Sb)=Sb ⇒ Sd=0> | |||||||||
| (101) | Spezialisierung (65) b ← Sd | (a+Sd)=(Sd+a) | |||||||||
| (102) | Verallgemeinerung (101) nach a | ∀a: (a+Sd)=(Sd+a) | |||||||||
| (103) | Spezialisierung (102) a ← Sb | (Sb+Sd)=(Sd+Sb) | |||||||||
| (104) | Hypothese | (Sb+Sd)=Sb | |||||||||
| (105) | Übernahme (103) | (Sb+Sd)=(Sd+Sb) | |||||||||
| (106) | Symmetrie (105) | (Sd+Sb)=(Sb+Sd) | |||||||||
| (107) | Transitivität (106), (104) | (Sd+Sb)=Sb | |||||||||
| (108) | Übernahme (100) | <(Sd+Sb)=Sb ⇒ Sd=0> | |||||||||
| (109) | Modus ponens (108), (107) | Sd=0 | |||||||||
| (110) | Konklusion (104), (109) | <(Sb+Sd)=Sb ⇒ Sd=0> | |||||||||
| (111) | Hypothese | a=b | |||||||||
| (112) | Übernahme (6) | (a+0)=a | |||||||||
| (113) | Übernahme (7) | (b+0)=b | |||||||||
| (114) | Symmetrie (113) | b=(b+0) | |||||||||
| (115) | Transitivität (112), (111) | (a+0)=b | |||||||||
| (116) | Transitivität (115), (114) | (a+0)=(b+0) | |||||||||
| (117) | Konklusion (111), (116) | <a=b ⇒ (a+0)=(b+0)> | |||||||||
| (118) | Hypothese | <a=b ⇒ (a+c)=(b+c)> | |||||||||
| (119) | Hypothese | a=b | |||||||||
| (120) | Übernahme (118) | <a=b ⇒ (a+c)=(b+c)> | |||||||||
| (121) | Modus ponens (120), (119) | (a+c)=(b+c) | |||||||||
| (122) | S hinzufügen (121) | S(a+c)=S(b+c) | |||||||||
| (123) | Übernahme (13) | (a+Sc)=S(a+c) | |||||||||
| (124) | Übernahme (15) | (b+Sc)=S(b+c) | |||||||||
| (125) | Symmetrie (124) | S(b+c)=(b+Sc) | |||||||||
| (126) | Transitivität (123), (122) | (a+Sc)=S(b+c) | |||||||||
| (127) | Transitivität (126), (125) | (a+Sc)=(b+Sc) | |||||||||
| (128) | Konklusion (119), (127) | <a=b ⇒ (a+Sc)=(b+Sc)> | |||||||||
| (129) | Konklusion (118), (128) | <<a=b ⇒ (a+c)=(b+c)> ⇒ <a=b ⇒ (a+Sc)=(b+Sc)>> | |||||||||
| (130) | Verallgemeinerung (129) nach c | ∀c: <<a=b ⇒ (a+c)=(b+c)> ⇒ <a=b ⇒ (a+Sc)=(b+Sc)>> | |||||||||
| (131) | Induktion (117), (130) | ∀c: <a=b ⇒ (a+c)=(b+c)> | |||||||||
| (132) | Spezialisierung (131) c ← d | <a=b ⇒ (a+d)=(b+d)> | |||||||||
| (133) | Verallgemeinerung (132) nach a | ∀a: <a=b ⇒ (a+d)=(b+d)> | |||||||||
| (134) | Spezialisierung (133) a ← c | <c=b ⇒ (c+d)=(b+d)> | |||||||||
| (135) | Verallgemeinerung (134) nach b | ∀b: <c=b ⇒ (c+d)=(b+d)> | |||||||||
| (136) | Spezialisierung (135) b ← 0 | <c=0 ⇒ (c+d)=(0+d)> | |||||||||
| (137) | Verallgemeinerung (136) nach d | ∀d: <c=0 ⇒ (c+d)=(0+d)> | |||||||||
| (138) | Spezialisierung (137) d ← a | <c=0 ⇒ (c+a)=(0+a)> | |||||||||
| (139) | Hypothese | c=0 | |||||||||
| (140) | Übernahme (138) | <c=0 ⇒ (c+a)=(0+a)> | |||||||||
| (141) | Modus ponens (140), (139) | (c+a)=(0+a) | |||||||||
| (142) | Übernahme (66) | (a+c)=(c+a) | |||||||||
| (143) | Übernahme (53) | (0+a)=a | |||||||||
| (144) | Transitivität (142), (141) | (a+c)=(0+a) | |||||||||
| (145) | Transitivität (144), (143) | (a+c)=a | |||||||||
| (146) | Konklusion (139), (145) | <c=0 ⇒ (a+c)=a> | |||||||||
| (147) | Spezialisierung (135) b ← Se | <c=Se ⇒ (c+d)=(Se+d)> | |||||||||
| (148) | Verallgemeinerung (147) nach d | ∀d: <c=Se ⇒ (c+d)=(Se+d)> | |||||||||
| (149) | Spezialisierung (148) d ← a | <c=Se ⇒ (c+a)=(Se+a)> | |||||||||
| (150) | Spezialisierung (65) b ← Se | (a+Se)=(Se+a) | |||||||||
| (151) | Symmetrie (150) | (Se+a)=(a+Se) | |||||||||
| (152) | Hypothese | Se=c | |||||||||
| (153) | Symmetrie (152) | c=Se | |||||||||
| (154) | Übernahme (149) | <c=Se ⇒ (c+a)=(Se+a)> | |||||||||
| (155) | Modus ponens (154), (153) | (c+a)=(Se+a) | |||||||||
| (156) | Übernahme (66) | (a+c)=(c+a) | |||||||||
| (157) | Übernahme (151) | (Se+a)=(a+Se) | |||||||||
| (158) | Transitivität (156), (155) | (a+c)=(Se+a) | |||||||||
| (159) | Transitivität (158), (157) | (a+c)=(a+Se) | |||||||||
| (160) | Symmetrie (159) | (a+Se)=(a+c) | |||||||||
| (161) | Konklusion (152), (160) | <Se=c ⇒ (a+Se)=(a+c)> | |||||||||
| (162) | Hypothese | ∀e: ¬Se=0 | |||||||||
| (163) | Übernahme (11) | 0=0 | |||||||||
| (164) | Konklusion (162), (163) | <∀e: ¬Se=0 ⇒ 0=0> | |||||||||
| (165) | Hypothese | <∀e: ¬Se=c ⇒ c=0> | |||||||||
| (166) | Hypothese | ∀e: ¬Se=Sc | |||||||||
| (167) | Spezialisierung (166) e ← c | ¬Sc=Sc | |||||||||
| (168) | Hypothese | ¬Sc=0 | |||||||||
| (169) | Übernahme (12) | Sc=Sc | |||||||||
| (170) | Konklusion (168), (169) | <¬Sc=0 ⇒ Sc=Sc> | |||||||||
| (171) | Kontraposition (170) | <¬Sc=Sc ⇒ ¬¬Sc=0> | |||||||||
| (172) | Modus ponens (171), (167) | ¬¬Sc=0 | |||||||||
| (173) | Doppelte Negation (172) | Sc=0 | |||||||||
| (174) | Konklusion (166), (173) | <∀e: ¬Se=Sc ⇒ Sc=0> | |||||||||
| (175) | Konklusion (165), (174) | <<∀e: ¬Se=c ⇒ c=0> ⇒ <∀e: ¬Se=Sc ⇒ Sc=0>> | |||||||||
| (176) | Verallgemeinerung (175) nach c | ∀c: <<∀e: ¬Se=c ⇒ c=0> ⇒ <∀e: ¬Se=Sc ⇒ Sc=0>> | |||||||||
| (177) | Induktion (164), (176) | ∀c: <∀e: ¬Se=c ⇒ c=0> | |||||||||
| (178) | Spezialisierung (177) c ← c | <∀e: ¬Se=c ⇒ c=0> | |||||||||
| (179) | Hypothese | ∀d: ¬(b+Sd)=Sa | |||||||||
| (180) | Spezialisierung (179) d ← Sd | ¬(b+SSd)=Sa | |||||||||
| (181) | Hypothese | (Sb+Sd)=Sa | |||||||||
| (182) | Übernahme (43) | (Sb+Sd)=S(b+Sd) | |||||||||
| (183) | Symmetrie (182) | S(b+Sd)=(Sb+Sd) | |||||||||
| (184) | Übernahme (22) | (b+SSd)=S(b+Sd) | |||||||||
| (185) | Transitivität (184), (183) | (b+SSd)=(Sb+Sd) | |||||||||
| (186) | Transitivität (185), (181) | (b+SSd)=Sa | |||||||||
| (187) | Konklusion (181), (186) | <(Sb+Sd)=Sa ⇒ (b+SSd)=Sa> | |||||||||
| (188) | Kontraposition (187) | <¬(b+SSd)=Sa ⇒ ¬(Sb+Sd)=Sa> | |||||||||
| (189) | Modus ponens (188), (180) | ¬(Sb+Sd)=Sa | |||||||||
| (190) | Verallgemeinerung (189) nach d | ∀d: ¬(Sb+Sd)=Sa | |||||||||
| (191) | Konklusion (179), (190) | <∀d: ¬(b+Sd)=Sa ⇒ ∀d: ¬(Sb+Sd)=Sa> | |||||||||
| (192) | Hypothese | a=b | |||||||||
| (193) | Hypothese | (Sb+Sd)=Sa | |||||||||
| (194) | Übernahme (192) | a=b | |||||||||
| (195) | S hinzufügen (194) | Sa=Sb | |||||||||
| (196) | Transitivität (193), (195) | (Sb+Sd)=Sb | |||||||||
| (197) | Übernahme (110) | <(Sb+Sd)=Sb ⇒ Sd=0> | |||||||||
| (198) | Modus ponens (197), (196) | Sd=0 | |||||||||
| (199) | Konklusion (193), (198) | <(Sb+Sd)=Sa ⇒ Sd=0> | |||||||||
| (200) | Kontraposition (199) | <¬Sd=0 ⇒ ¬(Sb+Sd)=Sa> | |||||||||
| (201) | Übernahme (23) | ¬Sd=0 | |||||||||
| (202) | Modus ponens (200), (201) | ¬(Sb+Sd)=Sa | |||||||||
| (203) | Verallgemeinerung (202) nach d | ∀d: ¬(Sb+Sd)=Sa | |||||||||
| (204) | Konklusion (192), (203) | <a=b ⇒ ∀d: ¬(Sb+Sd)=Sa> | |||||||||
| (205) | Hypothese | ¬a=b | |||||||||
| (206) | Hypothese | ∀c: ¬(a+Sc)=b | |||||||||
| (207) | Spezialisierung (206) c ← e | ¬(a+Se)=b | |||||||||
| (208) | Hypothese | (a+Sc)=Sb | |||||||||
| (209) | Übernahme (13) | (a+Sc)=S(a+c) | |||||||||
| (210) | Symmetrie (209) | S(a+c)=(a+Sc) | |||||||||
| (211) | Transitivität (210), (208) | S(a+c)=Sb | |||||||||
| (212) | S entfernen (211) | (a+c)=b | |||||||||
| (213) | Hypothese | Se=c | |||||||||
| (214) | Übernahme (161) | <Se=c ⇒ (a+Se)=(a+c)> | |||||||||
| (215) | Modus ponens (214), (213) | (a+Se)=(a+c) | |||||||||
| (216) | Übernahme (212) | (a+c)=b | |||||||||
| (217) | Transitivität (215), (216) | (a+Se)=b | |||||||||
| (218) | Konklusion (213), (217) | <Se=c ⇒ (a+Se)=b> | |||||||||
| (219) | Kontraposition (218) | <¬(a+Se)=b ⇒ ¬Se=c> | |||||||||
| (220) | Übernahme (207) | ¬(a+Se)=b | |||||||||
| (221) | Modus ponens (219), (220) | ¬Se=c | |||||||||
| (222) | Verallgemeinerung (221) nach e | ∀e: ¬Se=c | |||||||||
| (223) | Übernahme (178) | <∀e: ¬Se=c ⇒ c=0> | |||||||||
| (224) | Modus ponens (223), (222) | c=0 | |||||||||
| (225) | Übernahme (146) | <c=0 ⇒ (a+c)=a> | |||||||||
| (226) | Modus ponens (225), (224) | (a+c)=a | |||||||||
| (227) | S hinzufügen (226) | S(a+c)=Sa | |||||||||
| (228) | Transitivität (209), (227) | (a+Sc)=Sa | |||||||||
| (229) | Symmetrie (228) | Sa=(a+Sc) | |||||||||
| (230) | Transitivität (229), (208) | Sa=Sb | |||||||||
| (231) | S entfernen (230) | a=b | |||||||||
| (232) | Konklusion (208), (231) | <(a+Sc)=Sb ⇒ a=b> | |||||||||
| (233) | Kontraposition (232) | <¬a=b ⇒ ¬(a+Sc)=Sb> | |||||||||
| (234) | Übernahme (205) | ¬a=b | |||||||||
| (235) | Modus ponens (233), (234) | ¬(a+Sc)=Sb | |||||||||
| (236) | Verallgemeinerung (235) nach c | ∀c: ¬(a+Sc)=Sb | |||||||||
| (237) | Konklusion (206), (236) | <∀c: ¬(a+Sc)=b ⇒ ∀c: ¬(a+Sc)=Sb> | |||||||||
| (238) | Konklusion (205), (237) | <¬a=b ⇒ <∀c: ¬(a+Sc)=b ⇒ ∀c: ¬(a+Sc)=Sb>> | |||||||||
| (239) | Hypothese | <¬∀c: ¬(a+Sc)=Sb∧¬∀d: ¬(Sb+Sd)=Sa> | |||||||||
| (240) | Abtrennung I (239) | ¬∀c: ¬(a+Sc)=Sb | |||||||||
| (241) | Abtrennung II (239) | ¬∀d: ¬(Sb+Sd)=Sa | |||||||||
| (242) | Übernahme (191) | <∀d: ¬(b+Sd)=Sa ⇒ ∀d: ¬(Sb+Sd)=Sa> | |||||||||
| (243) | Kontraposition (242) | <¬∀d: ¬(Sb+Sd)=Sa ⇒ ¬∀d: ¬(b+Sd)=Sa> | |||||||||
| (244) | Modus ponens (243), (241) | ¬∀d: ¬(b+Sd)=Sa | |||||||||
| (245) | Übernahme (204) | <a=b ⇒ ∀d: ¬(Sb+Sd)=Sa> | |||||||||
| (246) | Kontraposition (245) | <¬∀d: ¬(Sb+Sd)=Sa ⇒ ¬a=b> | |||||||||
| (247) | Modus ponens (246), (241) | ¬a=b | |||||||||
| (248) | Übernahme (238) | <¬a=b ⇒ <∀c: ¬(a+Sc)=b ⇒ ∀c: ¬(a+Sc)=Sb>> | |||||||||
| (249) | Modus ponens (248), (247) | <∀c: ¬(a+Sc)=b ⇒ ∀c: ¬(a+Sc)=Sb> | |||||||||
| (250) | Kontraposition (249) | <¬∀c: ¬(a+Sc)=Sb ⇒ ¬∀c: ¬(a+Sc)=b> | |||||||||
| (251) | Modus ponens (250), (240) | ¬∀c: ¬(a+Sc)=b | |||||||||
| (252) | Konjunktion (251), (244) | <¬∀c: ¬(a+Sc)=b∧¬∀d: ¬(b+Sd)=Sa> | |||||||||
| (253) | Konklusion (239), (252) | <<¬∀c: ¬(a+Sc)=Sb∧¬∀d: ¬(Sb+Sd)=Sa> ⇒ <¬∀c: ¬(a+Sc)=b∧¬∀d: ¬(b+Sd)=Sa>> | |||||||||
| (254) | Kontraposition (253) | <¬<¬∀c: ¬(a+Sc)=b∧¬∀d: ¬(b+Sd)=Sa> ⇒ ¬<¬∀c: ¬(a+Sc)=Sb∧¬∀d: ¬(Sb+Sd)=Sa>> | |||||||||
| (255) | Verallgemeinerung (254) nach b | ∀b: <¬<¬∀c: ¬(a+Sc)=b∧¬∀d: ¬(b+Sd)=Sa> ⇒ ¬<¬∀c: ¬(a+Sc)=Sb∧¬∀d: ¬(Sb+Sd)=Sa>> | |||||||||
| (256) | Hypothese | (a+Sc)=0 | |||||||||
| (257) | Übernahme (13) | (a+Sc)=S(a+c) | |||||||||
| (258) | Symmetrie (257) | S(a+c)=(a+Sc) | |||||||||
| (259) | Transitivität (258), (256) | S(a+c)=0 | |||||||||
| (260) | Konklusion (256), (259) | <(a+Sc)=0 ⇒ S(a+c)=0> | |||||||||
| (261) | Kontraposition (260) | <¬S(a+c)=0 ⇒ ¬(a+Sc)=0> | |||||||||
| (262) | Spezialisierung (1) a ← (a+c) | ¬S(a+c)=0 | |||||||||
| (263) | Modus ponens (261), (262) | ¬(a+Sc)=0 | |||||||||
| (264) | Verallgemeinerung (263) nach c | ∀c: ¬(a+Sc)=0 | |||||||||
| (265) | Doppelte Negation (264) | ¬¬∀c: ¬(a+Sc)=0 | |||||||||
| (266) | Hypothese | <¬∀c: ¬(a+Sc)=0∧¬∀d: ¬(0+Sd)=Sa> | |||||||||
| (267) | Abtrennung I (266) | ¬∀c: ¬(a+Sc)=0 | |||||||||
| (268) | Konklusion (266), (267) | <<¬∀c: ¬(a+Sc)=0∧¬∀d: ¬(0+Sd)=Sa> ⇒ ¬∀c: ¬(a+Sc)=0> | |||||||||
| (269) | Kontraposition (268) | <¬¬∀c: ¬(a+Sc)=0 ⇒ ¬<¬∀c: ¬(a+Sc)=0∧¬∀d: ¬(0+Sd)=Sa>> | |||||||||
| (270) | Modus ponens (269), (265) | ¬<¬∀c: ¬(a+Sc)=0∧¬∀d: ¬(0+Sd)=Sa> | |||||||||
| (271) | Induktion (270), (255) | ∀b: ¬<¬∀c: ¬(a+Sc)=b∧¬∀d: ¬(b+Sd)=Sa> | |||||||||
| (272) | Verallgemeinerung (271) nach a | ∀a: ∀b: ¬<¬∀c: ¬(a+Sc)=b∧¬∀d: ¬(b+Sd)=Sa> | |||||||||
| (273) | Spezialisierung (272) a ← SSSS0 | ∀b: ¬<¬∀c: ¬(SSSS0+Sc)=b∧¬∀d: ¬(b+Sd)=SSSSS0> | |||||||||
Interpretation:
Es gibt keine Zahl zwischen 4 und 5 (direkt aus den Axiomen gezeigt)