Es gelten die allgemeinen Vorbemerkungen.
| (1) | Axiom 1 | ∀a: ¬Sa=0 | |||||||||
| (2) | Axiom 3 | ∀a: ∀b: (a+Sb)=S(a+b) | |||||||||
| (3) | Spezialisierung (2) a ← a | ∀b: (a+Sb)=S(a+b) | |||||||||
| (4) | Spezialisierung (3) b ← c | (a+Sc)=S(a+c) | |||||||||
| (5) | Spezialisierung (3) b ← Sd | (a+SSd)=S(a+Sd) | |||||||||
| (6) | Verallgemeinerung (5) nach a | ∀a: (a+SSd)=S(a+Sd) | |||||||||
| (7) | Spezialisierung (6) a ← b | (b+SSd)=S(b+Sd) | |||||||||
| (8) | Spezialisierung (1) a ← d | ¬Sd=0 | |||||||||
| (9) | Theorem 6 | ∀a: ∀b: (Sa+b)=S(a+b) | |||||||||
| (10) | Spezialisierung (9) a ← a | ∀b: (Sa+b)=S(a+b) | |||||||||
| (11) | Spezialisierung (10) b ← c | (Sa+c)=S(a+c) | |||||||||
| (12) | Verallgemeinerung (11) nach a | ∀a: (Sa+c)=S(a+c) | |||||||||
| (13) | Spezialisierung (12) a ← b | (Sb+c)=S(b+c) | |||||||||
| (14) | Verallgemeinerung (13) nach c | ∀c: (Sb+c)=S(b+c) | |||||||||
| (15) | Spezialisierung (14) c ← Sd | (Sb+Sd)=S(b+Sd) | |||||||||
| (16) | Theorem 5 | ∀a: (0+a)=a | |||||||||
| (17) | Spezialisierung (16) a ← b | (0+b)=b | |||||||||
| (18) | Spezialisierung (16) a ← a | (0+a)=a | |||||||||
| (19) | Theorem 8 | ∀a: ∀b: (a+b)=(b+a) | |||||||||
| (20) | Spezialisierung (19) a ← a | ∀b: (a+b)=(b+a) | |||||||||
| (21) | Spezialisierung (20) b ← c | (a+c)=(c+a) | |||||||||
| (22) | Theorem 22 | ∀a: ∀b: ∀c: <(a+c)=(b+c) ⇒ a=b> | |||||||||
| (23) | Spezialisierung (22) a ← a | ∀b: ∀c: <(a+c)=(b+c) ⇒ a=b> | |||||||||
| (24) | Spezialisierung (23) b ← 0 | ∀c: <(a+c)=(0+c) ⇒ a=0> | |||||||||
| (25) | Spezialisierung (24) c ← b | <(a+b)=(0+b) ⇒ a=0> | |||||||||
| (26) | Hypothese | (a+b)=b | |||||||||
| (27) | Übernahme (17) | (0+b)=b | |||||||||
| (28) | Symmetrie (27) | b=(0+b) | |||||||||
| (29) | Transitivität (26), (28) | (a+b)=(0+b) | |||||||||
| (30) | Übernahme (25) | <(a+b)=(0+b) ⇒ a=0> | |||||||||
| (31) | Modus ponens (30), (29) | a=0 | |||||||||
| (32) | Konklusion (26), (31) | <(a+b)=b ⇒ a=0> | |||||||||
| (33) | Verallgemeinerung (32) nach b | ∀b: <(a+b)=b ⇒ a=0> | |||||||||
| (34) | Spezialisierung (33) b ← Sb | <(a+Sb)=Sb ⇒ a=0> | |||||||||
| (35) | Verallgemeinerung (34) nach a | ∀a: <(a+Sb)=Sb ⇒ a=0> | |||||||||
| (36) | Spezialisierung (35) a ← Sd | <(Sd+Sb)=Sb ⇒ Sd=0> | |||||||||
| (37) | Spezialisierung (20) b ← Sd | (a+Sd)=(Sd+a) | |||||||||
| (38) | Verallgemeinerung (37) nach a | ∀a: (a+Sd)=(Sd+a) | |||||||||
| (39) | Spezialisierung (38) a ← Sb | (Sb+Sd)=(Sd+Sb) | |||||||||
| (40) | Hypothese | (Sb+Sd)=Sb | |||||||||
| (41) | Übernahme (39) | (Sb+Sd)=(Sd+Sb) | |||||||||
| (42) | Symmetrie (41) | (Sd+Sb)=(Sb+Sd) | |||||||||
| (43) | Transitivität (42), (40) | (Sd+Sb)=Sb | |||||||||
| (44) | Übernahme (36) | <(Sd+Sb)=Sb ⇒ Sd=0> | |||||||||
| (45) | Modus ponens (44), (43) | Sd=0 | |||||||||
| (46) | Konklusion (40), (45) | <(Sb+Sd)=Sb ⇒ Sd=0> | |||||||||
| (47) | Theorem 9 | ∀a: ∀b: ∀c: <a=b ⇒ (a+c)=(b+c)> | |||||||||
| (48) | Spezialisierung (47) a ← a | ∀b: ∀c: <a=b ⇒ (a+c)=(b+c)> | |||||||||
| (49) | Spezialisierung (48) b ← b | ∀c: <a=b ⇒ (a+c)=(b+c)> | |||||||||
| (50) | Spezialisierung (49) c ← d | <a=b ⇒ (a+d)=(b+d)> | |||||||||
| (51) | Verallgemeinerung (50) nach a | ∀a: <a=b ⇒ (a+d)=(b+d)> | |||||||||
| (52) | Spezialisierung (51) a ← c | <c=b ⇒ (c+d)=(b+d)> | |||||||||
| (53) | Verallgemeinerung (52) nach b | ∀b: <c=b ⇒ (c+d)=(b+d)> | |||||||||
| (54) | Spezialisierung (53) b ← 0 | <c=0 ⇒ (c+d)=(0+d)> | |||||||||
| (55) | Verallgemeinerung (54) nach d | ∀d: <c=0 ⇒ (c+d)=(0+d)> | |||||||||
| (56) | Spezialisierung (55) d ← a | <c=0 ⇒ (c+a)=(0+a)> | |||||||||
| (57) | Hypothese | c=0 | |||||||||
| (58) | Übernahme (56) | <c=0 ⇒ (c+a)=(0+a)> | |||||||||
| (59) | Modus ponens (58), (57) | (c+a)=(0+a) | |||||||||
| (60) | Übernahme (21) | (a+c)=(c+a) | |||||||||
| (61) | Übernahme (18) | (0+a)=a | |||||||||
| (62) | Transitivität (60), (59) | (a+c)=(0+a) | |||||||||
| (63) | Transitivität (62), (61) | (a+c)=a | |||||||||
| (64) | Konklusion (57), (63) | <c=0 ⇒ (a+c)=a> | |||||||||
| (65) | Spezialisierung (53) b ← Se | <c=Se ⇒ (c+d)=(Se+d)> | |||||||||
| (66) | Verallgemeinerung (65) nach d | ∀d: <c=Se ⇒ (c+d)=(Se+d)> | |||||||||
| (67) | Spezialisierung (66) d ← a | <c=Se ⇒ (c+a)=(Se+a)> | |||||||||
| (68) | Spezialisierung (20) b ← Se | (a+Se)=(Se+a) | |||||||||
| (69) | Symmetrie (68) | (Se+a)=(a+Se) | |||||||||
| (70) | Hypothese | Se=c | |||||||||
| (71) | Symmetrie (70) | c=Se | |||||||||
| (72) | Übernahme (67) | <c=Se ⇒ (c+a)=(Se+a)> | |||||||||
| (73) | Modus ponens (72), (71) | (c+a)=(Se+a) | |||||||||
| (74) | Übernahme (21) | (a+c)=(c+a) | |||||||||
| (75) | Übernahme (69) | (Se+a)=(a+Se) | |||||||||
| (76) | Transitivität (74), (73) | (a+c)=(Se+a) | |||||||||
| (77) | Transitivität (76), (75) | (a+c)=(a+Se) | |||||||||
| (78) | Symmetrie (77) | (a+Se)=(a+c) | |||||||||
| (79) | Konklusion (70), (78) | <Se=c ⇒ (a+Se)=(a+c)> | |||||||||
| (80) | Theorem 3 | ∀a: <∀b: ¬Sb=a ⇒ a=0> | |||||||||
| (81) | Spezialisierung (80) a ← c | <∀b: ¬Sb=c ⇒ c=0> | |||||||||
| (82) | Hypothese | ∀e: ¬Se=c | |||||||||
| (83) | Spezialisierung (82) e ← b | ¬Sb=c | |||||||||
| (84) | Verallgemeinerung (83) nach b | ∀b: ¬Sb=c | |||||||||
| (85) | Übernahme (81) | <∀b: ¬Sb=c ⇒ c=0> | |||||||||
| (86) | Modus ponens (85), (84) | c=0 | |||||||||
| (87) | Konklusion (82), (86) | <∀e: ¬Se=c ⇒ c=0> | |||||||||
| (88) | Hypothese | ∀d: ¬(b+Sd)=Sa | |||||||||
| (89) | Spezialisierung (88) d ← Sd | ¬(b+SSd)=Sa | |||||||||
| (90) | Hypothese | (Sb+Sd)=Sa | |||||||||
| (91) | Übernahme (15) | (Sb+Sd)=S(b+Sd) | |||||||||
| (92) | Symmetrie (91) | S(b+Sd)=(Sb+Sd) | |||||||||
| (93) | Übernahme (7) | (b+SSd)=S(b+Sd) | |||||||||
| (94) | Transitivität (93), (92) | (b+SSd)=(Sb+Sd) | |||||||||
| (95) | Transitivität (94), (90) | (b+SSd)=Sa | |||||||||
| (96) | Konklusion (90), (95) | <(Sb+Sd)=Sa ⇒ (b+SSd)=Sa> | |||||||||
| (97) | Kontraposition (96) | <¬(b+SSd)=Sa ⇒ ¬(Sb+Sd)=Sa> | |||||||||
| (98) | Modus ponens (97), (89) | ¬(Sb+Sd)=Sa | |||||||||
| (99) | Verallgemeinerung (98) nach d | ∀d: ¬(Sb+Sd)=Sa | |||||||||
| (100) | Konklusion (88), (99) | <∀d: ¬(b+Sd)=Sa ⇒ ∀d: ¬(Sb+Sd)=Sa> | |||||||||
| (101) | Hypothese | a=b | |||||||||
| (102) | Hypothese | (Sb+Sd)=Sa | |||||||||
| (103) | Übernahme (101) | a=b | |||||||||
| (104) | S hinzufügen (103) | Sa=Sb | |||||||||
| (105) | Transitivität (102), (104) | (Sb+Sd)=Sb | |||||||||
| (106) | Übernahme (46) | <(Sb+Sd)=Sb ⇒ Sd=0> | |||||||||
| (107) | Modus ponens (106), (105) | Sd=0 | |||||||||
| (108) | Konklusion (102), (107) | <(Sb+Sd)=Sa ⇒ Sd=0> | |||||||||
| (109) | Kontraposition (108) | <¬Sd=0 ⇒ ¬(Sb+Sd)=Sa> | |||||||||
| (110) | Übernahme (8) | ¬Sd=0 | |||||||||
| (111) | Modus ponens (109), (110) | ¬(Sb+Sd)=Sa | |||||||||
| (112) | Verallgemeinerung (111) nach d | ∀d: ¬(Sb+Sd)=Sa | |||||||||
| (113) | Konklusion (101), (112) | <a=b ⇒ ∀d: ¬(Sb+Sd)=Sa> | |||||||||
| (114) | Hypothese | ¬a=b | |||||||||
| (115) | Hypothese | ∀c: ¬(a+Sc)=b | |||||||||
| (116) | Spezialisierung (115) c ← e | ¬(a+Se)=b | |||||||||
| (117) | Hypothese | (a+Sc)=Sb | |||||||||
| (118) | Übernahme (4) | (a+Sc)=S(a+c) | |||||||||
| (119) | Symmetrie (118) | S(a+c)=(a+Sc) | |||||||||
| (120) | Transitivität (119), (117) | S(a+c)=Sb | |||||||||
| (121) | S entfernen (120) | (a+c)=b | |||||||||
| (122) | Hypothese | Se=c | |||||||||
| (123) | Übernahme (79) | <Se=c ⇒ (a+Se)=(a+c)> | |||||||||
| (124) | Modus ponens (123), (122) | (a+Se)=(a+c) | |||||||||
| (125) | Übernahme (121) | (a+c)=b | |||||||||
| (126) | Transitivität (124), (125) | (a+Se)=b | |||||||||
| (127) | Konklusion (122), (126) | <Se=c ⇒ (a+Se)=b> | |||||||||
| (128) | Kontraposition (127) | <¬(a+Se)=b ⇒ ¬Se=c> | |||||||||
| (129) | Übernahme (116) | ¬(a+Se)=b | |||||||||
| (130) | Modus ponens (128), (129) | ¬Se=c | |||||||||
| (131) | Verallgemeinerung (130) nach e | ∀e: ¬Se=c | |||||||||
| (132) | Übernahme (87) | <∀e: ¬Se=c ⇒ c=0> | |||||||||
| (133) | Modus ponens (132), (131) | c=0 | |||||||||
| (134) | Übernahme (64) | <c=0 ⇒ (a+c)=a> | |||||||||
| (135) | Modus ponens (134), (133) | (a+c)=a | |||||||||
| (136) | S hinzufügen (135) | S(a+c)=Sa | |||||||||
| (137) | Transitivität (118), (136) | (a+Sc)=Sa | |||||||||
| (138) | Symmetrie (137) | Sa=(a+Sc) | |||||||||
| (139) | Transitivität (138), (117) | Sa=Sb | |||||||||
| (140) | S entfernen (139) | a=b | |||||||||
| (141) | Konklusion (117), (140) | <(a+Sc)=Sb ⇒ a=b> | |||||||||
| (142) | Kontraposition (141) | <¬a=b ⇒ ¬(a+Sc)=Sb> | |||||||||
| (143) | Übernahme (114) | ¬a=b | |||||||||
| (144) | Modus ponens (142), (143) | ¬(a+Sc)=Sb | |||||||||
| (145) | Verallgemeinerung (144) nach c | ∀c: ¬(a+Sc)=Sb | |||||||||
| (146) | Konklusion (115), (145) | <∀c: ¬(a+Sc)=b ⇒ ∀c: ¬(a+Sc)=Sb> | |||||||||
| (147) | Konklusion (114), (146) | <¬a=b ⇒ <∀c: ¬(a+Sc)=b ⇒ ∀c: ¬(a+Sc)=Sb>> | |||||||||
| (148) | Hypothese | <¬∀c: ¬(a+Sc)=Sb∧¬∀d: ¬(Sb+Sd)=Sa> | |||||||||
| (149) | Abtrennung I (148) | ¬∀c: ¬(a+Sc)=Sb | |||||||||
| (150) | Abtrennung II (148) | ¬∀d: ¬(Sb+Sd)=Sa | |||||||||
| (151) | Übernahme (100) | <∀d: ¬(b+Sd)=Sa ⇒ ∀d: ¬(Sb+Sd)=Sa> | |||||||||
| (152) | Kontraposition (151) | <¬∀d: ¬(Sb+Sd)=Sa ⇒ ¬∀d: ¬(b+Sd)=Sa> | |||||||||
| (153) | Modus ponens (152), (150) | ¬∀d: ¬(b+Sd)=Sa | |||||||||
| (154) | Übernahme (113) | <a=b ⇒ ∀d: ¬(Sb+Sd)=Sa> | |||||||||
| (155) | Kontraposition (154) | <¬∀d: ¬(Sb+Sd)=Sa ⇒ ¬a=b> | |||||||||
| (156) | Modus ponens (155), (150) | ¬a=b | |||||||||
| (157) | Übernahme (147) | <¬a=b ⇒ <∀c: ¬(a+Sc)=b ⇒ ∀c: ¬(a+Sc)=Sb>> | |||||||||
| (158) | Modus ponens (157), (156) | <∀c: ¬(a+Sc)=b ⇒ ∀c: ¬(a+Sc)=Sb> | |||||||||
| (159) | Kontraposition (158) | <¬∀c: ¬(a+Sc)=Sb ⇒ ¬∀c: ¬(a+Sc)=b> | |||||||||
| (160) | Modus ponens (159), (149) | ¬∀c: ¬(a+Sc)=b | |||||||||
| (161) | Konjunktion (160), (153) | <¬∀c: ¬(a+Sc)=b∧¬∀d: ¬(b+Sd)=Sa> | |||||||||
| (162) | Konklusion (148), (161) | <<¬∀c: ¬(a+Sc)=Sb∧¬∀d: ¬(Sb+Sd)=Sa> ⇒ <¬∀c: ¬(a+Sc)=b∧¬∀d: ¬(b+Sd)=Sa>> | |||||||||
| (163) | Kontraposition (162) | <¬<¬∀c: ¬(a+Sc)=b∧¬∀d: ¬(b+Sd)=Sa> ⇒ ¬<¬∀c: ¬(a+Sc)=Sb∧¬∀d: ¬(Sb+Sd)=Sa>> | |||||||||
| (164) | Verallgemeinerung (163) nach b | ∀b: <¬<¬∀c: ¬(a+Sc)=b∧¬∀d: ¬(b+Sd)=Sa> ⇒ ¬<¬∀c: ¬(a+Sc)=Sb∧¬∀d: ¬(Sb+Sd)=Sa>> | |||||||||
| (165) | Hypothese | (a+Sc)=0 | |||||||||
| (166) | Übernahme (4) | (a+Sc)=S(a+c) | |||||||||
| (167) | Symmetrie (166) | S(a+c)=(a+Sc) | |||||||||
| (168) | Transitivität (167), (165) | S(a+c)=0 | |||||||||
| (169) | Konklusion (165), (168) | <(a+Sc)=0 ⇒ S(a+c)=0> | |||||||||
| (170) | Kontraposition (169) | <¬S(a+c)=0 ⇒ ¬(a+Sc)=0> | |||||||||
| (171) | Spezialisierung (1) a ← (a+c) | ¬S(a+c)=0 | |||||||||
| (172) | Modus ponens (170), (171) | ¬(a+Sc)=0 | |||||||||
| (173) | Verallgemeinerung (172) nach c | ∀c: ¬(a+Sc)=0 | |||||||||
| (174) | Doppelte Negation (173) | ¬¬∀c: ¬(a+Sc)=0 | |||||||||
| (175) | Hypothese | <¬∀c: ¬(a+Sc)=0∧¬∀d: ¬(0+Sd)=Sa> | |||||||||
| (176) | Abtrennung I (175) | ¬∀c: ¬(a+Sc)=0 | |||||||||
| (177) | Konklusion (175), (176) | <<¬∀c: ¬(a+Sc)=0∧¬∀d: ¬(0+Sd)=Sa> ⇒ ¬∀c: ¬(a+Sc)=0> | |||||||||
| (178) | Kontraposition (177) | <¬¬∀c: ¬(a+Sc)=0 ⇒ ¬<¬∀c: ¬(a+Sc)=0∧¬∀d: ¬(0+Sd)=Sa>> | |||||||||
| (179) | Modus ponens (178), (174) | ¬<¬∀c: ¬(a+Sc)=0∧¬∀d: ¬(0+Sd)=Sa> | |||||||||
| (180) | Induktion (179), (164) | ∀b: ¬<¬∀c: ¬(a+Sc)=b∧¬∀d: ¬(b+Sd)=Sa> | |||||||||
| (181) | Verallgemeinerung (180) nach a | ∀a: ∀b: ¬<¬∀c: ¬(a+Sc)=b∧¬∀d: ¬(b+Sd)=Sa> | |||||||||
| (182) | Spezialisierung (181) a ← SSSS0 | ∀b: ¬<¬∀c: ¬(SSSS0+Sc)=b∧¬∀d: ¬(b+Sd)=SSSSS0> | |||||||||
Interpretation:
Es gibt keine Zahl zwischen 4 und 5