MODULE ( HEADER ( SPEC ( NAME ("proptheo2"), VERSION ("1.00.00"), VERSION ("1.00.00"), LOCATIONS ( LOCATION ("http://www.qedeq.org/0_00_53") ) ), HEADLINE ("The Axioms of the Whitehead Russell Calculus"), DESCRIPTION ( "This module notates the original axioms of the Whitehead-Russell calculus, the so called `primitive propositions'. These five primitive propositions could be deduced by our four axioms." ), EMAIL ("module@qedeq.org"), AUTHORS ( AUTHOR ("Michael Meyling",EMAIL ("mime@qedeq.org")) ) ), IMPORTS ( IMPORT ( SPEC ( NAME ("propaxiom"), VERSION ("1.00.00"), VERSION ("1.00.00"), LOCATIONS ( LOCATION ("."), LOCATION ("http://www.qedeq.org/0_00_53") ) ) ) ), PARAGRAPHS ( PARAGRAPH ( LABEL ("lem1"), "At first we show a little proposition to demonstrate the basic proof methods of propositional calculus:", PROPOSITION ( SENTENCE ( IMPL(PROP(1), OR(PROP(2), PROP(1))) ), PROOF ( LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(OR(PROP(3), PROP(1)), OR(PROP(3), PROP(2)))), ADDAXIOM ( LINK ("axiom4")) ), LINE ( IMPL(IMPL(PROP(4), PROP(2)), IMPL(OR(PROP(3), PROP(4)), OR(PROP(3), PROP(2)))), REPLACEPROP ( 1, PROP(1), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(4), OR(PROP(2), PROP(1))), IMPL(OR(PROP(3), PROP(4)), OR(PROP(3), OR(PROP(2), PROP(1))))), REPLACEPROP ( 2, PROP(2), OR(PROP(2), PROP(1)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), IMPL(OR(PROP(3), OR(PROP(1), PROP(2))), OR(PROP(3), OR(PROP(2), PROP(1))))), REPLACEPROP ( 3, PROP(4), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), IMPL(OR(NOT(PROP(1)), OR(PROP(1), PROP(2))), OR(NOT(PROP(1)), OR(PROP(2), PROP(1))))), REPLACEPROP ( 4, PROP(3), NOT(PROP(1)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), IMPL(IMPL(PROP(1), OR(PROP(1), PROP(2))), OR(NOT(PROP(1)), OR(PROP(2), PROP(1))))), REVERSEABBREVIATION (5, LINK ("impl"), 1) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), IMPL(IMPL(PROP(1), OR(PROP(1), PROP(2))), IMPL(PROP(1), OR(PROP(2), PROP(1))))), REVERSEABBREVIATION (6, LINK ("impl"), 1) ), LINE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), ADDAXIOM ( LINK ("axiom3")) ), LINE ( IMPL(IMPL(PROP(1), OR(PROP(1), PROP(2))), IMPL(PROP(1), OR(PROP(2), PROP(1)))), MODUSPONENS (8, 7) ), LINE ( IMPL(PROP(1), OR(PROP(1), PROP(2))), ADDAXIOM ( LINK ("axiom2")) ), LINE ( IMPL(PROP(1), OR(PROP(2), PROP(1))), MODUSPONENS (10, 9) ) ) ) ), PARAGRAPH ( LABEL ("prin1"), "This is the first primitive proposition, its equal to our first axiom:", PROPOSITION ( SENTENCE ( IMPL(OR(PROP(1), PROP(1)), PROP(1)) ), PROOF ( LINE ( IMPL(OR(PROP(1), PROP(1)), PROP(1)), ADDAXIOM ( LINK ("axiom1")) ) ) ) ), PARAGRAPH ( LABEL ("prin2"), "Now comes the second primitive proposition. It looks simular to our second axiom, but we have to use our first proposition to prove it:", PROPOSITION ( SENTENCE ( IMPL(PROP(2), OR(PROP(1), PROP(2))) ), PROOF ( LINE ( IMPL(PROP(1), OR(PROP(2), PROP(1))), ADDSENTENCE ( LINK ("lem1")) ), LINE ( IMPL(PROP(1), OR(PROP(3), PROP(1))), REPLACEPROP ( 1, PROP(2), PROP(3) ) ), LINE ( IMPL(PROP(2), OR(PROP(3), PROP(2))), REPLACEPROP ( 2, PROP(1), PROP(2) ) ), LINE ( IMPL(PROP(2), OR(PROP(1), PROP(2))), REPLACEPROP ( 3, PROP(3), PROP(1) ) ) ) ) ), PARAGRAPH ( LABEL ("prin3"), "The third primitive proposition:", PROPOSITION ( SENTENCE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))) ), PROOF ( LINE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), ADDAXIOM ( LINK ("axiom3")) ) ) ) ), PARAGRAPH ( LABEL ("prin4"), "The fourth primitive proposition was proved with the other primitve propositions by P. Bernays. Here comes the sledgehammer:", PROPOSITION ( SENTENCE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))) ), PROOF ( LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(OR(PROP(3), PROP(1)), OR(PROP(3), PROP(2)))), ADDAXIOM ( LINK ("axiom4")) ), LINE ( IMPL(IMPL(PROP(7), PROP(2)), IMPL(OR(PROP(3), PROP(7)), OR(PROP(3), PROP(2)))), REPLACEPROP ( 1, PROP(1), PROP(7) ) ), LINE ( IMPL(IMPL(PROP(7), PROP(8)), IMPL(OR(PROP(3), PROP(7)), OR(PROP(3), PROP(8)))), REPLACEPROP ( 2, PROP(2), PROP(8) ) ), LINE ( IMPL(IMPL(PROP(7), PROP(8)), IMPL(OR(PROP(9), PROP(7)), OR(PROP(9), PROP(8)))), REPLACEPROP ( 3, PROP(3), PROP(9) ) ), LINE ( IMPL(PROP(1), OR(PROP(2), PROP(1))), ADDSENTENCE ( LINK ("lem1")) ), LINE ( IMPL(IMPL(PROP(1), OR(PROP(2), PROP(1))), IMPL(OR(PROP(3), PROP(1)), OR(PROP(3), OR(PROP(2), PROP(1))))), REPLACEPROP ( 1, PROP(2), OR(PROP(2), PROP(1)) ) ), LINE ( IMPL(OR(PROP(3), PROP(1)), OR(PROP(3), OR(PROP(2), PROP(1)))), MODUSPONENS (5, 6) ), LINE ( IMPL(IMPL(OR(PROP(3), PROP(1)), PROP(8)), IMPL(OR(PROP(9), OR(PROP(3), PROP(1))), OR(PROP(9), PROP(8)))), REPLACEPROP ( 4, PROP(7), OR(PROP(3), PROP(1)) ) ), LINE ( IMPL(IMPL(OR(PROP(3), PROP(1)), OR(PROP(3), OR(PROP(2), PROP(1)))), IMPL(OR(PROP(9), OR(PROP(3), PROP(1))), OR(PROP(9), OR(PROP(3), OR(PROP(2), PROP(1)))))), REPLACEPROP ( 8, PROP(8), OR(PROP(3), OR(PROP(2), PROP(1))) ) ), LINE ( IMPL(OR(PROP(9), OR(PROP(3), PROP(1))), OR(PROP(9), OR(PROP(3), OR(PROP(2), PROP(1))))), MODUSPONENS (7, 9) ), LINE ( IMPL(OR(PROP(2), OR(PROP(3), PROP(1))), OR(PROP(2), OR(PROP(3), OR(PROP(2), PROP(1))))), REPLACEPROP ( 10, PROP(9), PROP(2) ) ), LINE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), ADDAXIOM ( LINK ("axiom3")) ), LINE ( IMPL(OR(PROP(6), PROP(2)), OR(PROP(2), PROP(6))), REPLACEPROP ( 12, PROP(1), PROP(6) ) ), LINE ( IMPL(OR(PROP(6), OR(PROP(3), OR(PROP(2), PROP(1)))), OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(6))), REPLACEPROP ( 13, PROP(2), OR(PROP(3), OR(PROP(2), PROP(1))) ) ), LINE ( IMPL(OR(PROP(2), OR(PROP(3), OR(PROP(2), PROP(1)))), OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2))), REPLACEPROP ( 14, PROP(6), PROP(2) ) ), LINE ( IMPL(IMPL(OR(PROP(2), OR(PROP(3), OR(PROP(2), PROP(1)))), PROP(8)), IMPL(OR(PROP(9), OR(PROP(2), OR(PROP(3), OR(PROP(2), PROP(1))))), OR(PROP(9), PROP(8)))), REPLACEPROP ( 4, PROP(7), OR(PROP(2), OR(PROP(3), OR(PROP(2), PROP(1)))) ) ), LINE ( IMPL(IMPL(OR(PROP(2), OR(PROP(3), OR(PROP(2), PROP(1)))), OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2))), IMPL(OR(PROP(9), OR(PROP(2), OR(PROP(3), OR(PROP(2), PROP(1))))), OR(PROP(9), OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2))))), REPLACEPROP ( 16, PROP(8), OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2)) ) ), LINE ( IMPL(OR(PROP(9), OR(PROP(2), OR(PROP(3), OR(PROP(2), PROP(1))))), OR(PROP(9), OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2)))), MODUSPONENS (15, 17) ), LINE ( IMPL(OR(NOT(OR(PROP(2), OR(PROP(3), PROP(1)))), OR(PROP(2), OR(PROP(3), OR(PROP(2), PROP(1))))), OR(NOT(OR(PROP(2), OR(PROP(3), PROP(1)))), OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2)))), REPLACEPROP ( 18, PROP(9), NOT(OR(PROP(2), OR(PROP(3), PROP(1)))) ) ), LINE ( IMPL(IMPL(OR(PROP(2), OR(PROP(3), PROP(1))), OR(PROP(2), OR(PROP(3), OR(PROP(2), PROP(1))))), OR(NOT(OR(PROP(2), OR(PROP(3), PROP(1)))), OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2)))), REVERSEABBREVIATION (19, LINK ("impl"), 1) ), LINE ( IMPL(IMPL(OR(PROP(2), OR(PROP(3), PROP(1))), OR(PROP(2), OR(PROP(3), OR(PROP(2), PROP(1))))), IMPL(OR(PROP(2), OR(PROP(3), PROP(1))), OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2)))), REVERSEABBREVIATION (20, LINK ("impl"), 1) ), LINE ( IMPL(OR(PROP(2), OR(PROP(3), PROP(1))), OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2))), MODUSPONENS (11, 21) ), LINE ( IMPL(PROP(1), OR(PROP(1), PROP(2))), ADDAXIOM ( LINK ("axiom2")) ), LINE ( IMPL(PROP(3), OR(PROP(3), PROP(2))), REPLACEPROP ( 23, PROP(1), PROP(3) ) ), LINE ( IMPL(PROP(3), OR(PROP(3), PROP(1))), REPLACEPROP ( 24, PROP(2), PROP(1) ) ), LINE ( IMPL(PROP(2), OR(PROP(2), PROP(1))), REPLACEPROP ( 25, PROP(3), PROP(2) ) ), LINE ( IMPL(PROP(1), OR(PROP(3), PROP(1))), REPLACEPROP ( 5, PROP(2), PROP(3) ) ), LINE ( IMPL(OR(PROP(2), PROP(1)), OR(PROP(3), OR(PROP(2), PROP(1)))), REPLACEPROP ( 27, PROP(1), OR(PROP(2), PROP(1)) ) ), LINE ( IMPL(IMPL(OR(PROP(2), PROP(1)), PROP(8)), IMPL(OR(PROP(9), OR(PROP(2), PROP(1))), OR(PROP(9), PROP(8)))), REPLACEPROP ( 4, PROP(7), OR(PROP(2), PROP(1)) ) ), LINE ( IMPL(IMPL(OR(PROP(2), PROP(1)), OR(PROP(3), OR(PROP(2), PROP(1)))), IMPL(OR(PROP(9), OR(PROP(2), PROP(1))), OR(PROP(9), OR(PROP(3), OR(PROP(2), PROP(1)))))), REPLACEPROP ( 29, PROP(8), OR(PROP(3), OR(PROP(2), PROP(1))) ) ), LINE ( IMPL(OR(PROP(9), OR(PROP(2), PROP(1))), OR(PROP(9), OR(PROP(3), OR(PROP(2), PROP(1))))), MODUSPONENS (28, 30) ), LINE ( IMPL(OR(NOT(PROP(2)), OR(PROP(2), PROP(1))), OR(NOT(PROP(2)), OR(PROP(3), OR(PROP(2), PROP(1))))), REPLACEPROP ( 31, PROP(9), NOT(PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(2), OR(PROP(2), PROP(1))), OR(NOT(PROP(2)), OR(PROP(3), OR(PROP(2), PROP(1))))), REVERSEABBREVIATION (32, LINK ("impl"), 1) ), LINE ( IMPL(IMPL(PROP(2), OR(PROP(2), PROP(1))), IMPL(PROP(2), OR(PROP(3), OR(PROP(2), PROP(1))))), REVERSEABBREVIATION (33, LINK ("impl"), 1) ), LINE ( IMPL(PROP(2), OR(PROP(3), OR(PROP(2), PROP(1)))), MODUSPONENS (26, 34) ), LINE ( IMPL(IMPL(PROP(2), PROP(8)), IMPL(OR(PROP(9), PROP(2)), OR(PROP(9), PROP(8)))), REPLACEPROP ( 4, PROP(7), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(2), OR(PROP(3), OR(PROP(2), PROP(1)))), IMPL(OR(PROP(9), PROP(2)), OR(PROP(9), OR(PROP(3), OR(PROP(2), PROP(1)))))), REPLACEPROP ( 36, PROP(8), OR(PROP(3), OR(PROP(2), PROP(1))) ) ), LINE ( IMPL(OR(PROP(9), PROP(2)), OR(PROP(9), OR(PROP(3), OR(PROP(2), PROP(1))))), MODUSPONENS (35, 37) ), LINE ( IMPL(OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2)), OR(OR(PROP(3), OR(PROP(2), PROP(1))), OR(PROP(3), OR(PROP(2), PROP(1))))), REPLACEPROP ( 38, PROP(9), OR(PROP(3), OR(PROP(2), PROP(1))) ) ), LINE ( IMPL(OR(PROP(1), PROP(1)), PROP(1)), ADDAXIOM ( LINK ("axiom1")) ), LINE ( IMPL(OR(OR(PROP(3), OR(PROP(2), PROP(1))), OR(PROP(3), OR(PROP(2), PROP(1)))), OR(PROP(3), OR(PROP(2), PROP(1)))), REPLACEPROP ( 40, PROP(1), OR(PROP(3), OR(PROP(2), PROP(1))) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(3), OR(PROP(2), PROP(1))), OR(PROP(3), OR(PROP(2), PROP(1)))), PROP(8)), IMPL(OR(PROP(9), OR(OR(PROP(3), OR(PROP(2), PROP(1))), OR(PROP(3), OR(PROP(2), PROP(1))))), OR(PROP(9), PROP(8)))), REPLACEPROP ( 4, PROP(7), OR(OR(PROP(3), OR(PROP(2), PROP(1))), OR(PROP(3), OR(PROP(2), PROP(1)))) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(3), OR(PROP(2), PROP(1))), OR(PROP(3), OR(PROP(2), PROP(1)))), OR(PROP(3), OR(PROP(2), PROP(1)))), IMPL(OR(PROP(9), OR(OR(PROP(3), OR(PROP(2), PROP(1))), OR(PROP(3), OR(PROP(2), PROP(1))))), OR(PROP(9), OR(PROP(3), OR(PROP(2), PROP(1)))))), REPLACEPROP ( 42, PROP(8), OR(PROP(3), OR(PROP(2), PROP(1))) ) ), LINE ( IMPL(OR(PROP(9), OR(OR(PROP(3), OR(PROP(2), PROP(1))), OR(PROP(3), OR(PROP(2), PROP(1))))), OR(PROP(9), OR(PROP(3), OR(PROP(2), PROP(1))))), MODUSPONENS (41, 43) ), LINE ( IMPL(OR(NOT(OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2))), OR(OR(PROP(3), OR(PROP(2), PROP(1))), OR(PROP(3), OR(PROP(2), PROP(1))))), OR(NOT(OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2))), OR(PROP(3), OR(PROP(2), PROP(1))))), REPLACEPROP ( 44, PROP(9), NOT(OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2))) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2)), OR(OR(PROP(3), OR(PROP(2), PROP(1))), OR(PROP(3), OR(PROP(2), PROP(1))))), OR(NOT(OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2))), OR(PROP(3), OR(PROP(2), PROP(1))))), REVERSEABBREVIATION (45, LINK ("impl"), 1) ), LINE ( IMPL(IMPL(OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2)), OR(OR(PROP(3), OR(PROP(2), PROP(1))), OR(PROP(3), OR(PROP(2), PROP(1))))), IMPL(OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2)), OR(PROP(3), OR(PROP(2), PROP(1))))), REVERSEABBREVIATION (46, LINK ("impl"), 1) ), LINE ( IMPL(OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2)), OR(PROP(3), OR(PROP(2), PROP(1)))), MODUSPONENS (39, 47) ), LINE ( IMPL(IMPL(OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2)), PROP(8)), IMPL(OR(PROP(9), OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2))), OR(PROP(9), PROP(8)))), REPLACEPROP ( 4, PROP(7), OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2)) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2)), OR(PROP(3), OR(PROP(2), PROP(1)))), IMPL(OR(PROP(9), OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2))), OR(PROP(9), OR(PROP(3), OR(PROP(2), PROP(1)))))), REPLACEPROP ( 49, PROP(8), OR(PROP(3), OR(PROP(2), PROP(1))) ) ), LINE ( IMPL(OR(PROP(9), OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2))), OR(PROP(9), OR(PROP(3), OR(PROP(2), PROP(1))))), MODUSPONENS (48, 50) ), LINE ( IMPL(OR(NOT(OR(PROP(2), OR(PROP(3), PROP(1)))), OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2))), OR(NOT(OR(PROP(2), OR(PROP(3), PROP(1)))), OR(PROP(3), OR(PROP(2), PROP(1))))), REPLACEPROP ( 51, PROP(9), NOT(OR(PROP(2), OR(PROP(3), PROP(1)))) ) ), LINE ( IMPL(IMPL(OR(PROP(2), OR(PROP(3), PROP(1))), OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2))), OR(NOT(OR(PROP(2), OR(PROP(3), PROP(1)))), OR(PROP(3), OR(PROP(2), PROP(1))))), REVERSEABBREVIATION (52, LINK ("impl"), 1) ), LINE ( IMPL(IMPL(OR(PROP(2), OR(PROP(3), PROP(1))), OR(OR(PROP(3), OR(PROP(2), PROP(1))), PROP(2))), IMPL(OR(PROP(2), OR(PROP(3), PROP(1))), OR(PROP(3), OR(PROP(2), PROP(1))))), REVERSEABBREVIATION (53, LINK ("impl"), 1) ), LINE ( IMPL(OR(PROP(2), OR(PROP(3), PROP(1))), OR(PROP(3), OR(PROP(2), PROP(1)))), MODUSPONENS (22, 54) ), LINE ( IMPL(OR(PROP(7), OR(PROP(3), PROP(1))), OR(PROP(3), OR(PROP(7), PROP(1)))), REPLACEPROP ( 55, PROP(2), PROP(7) ) ), LINE ( IMPL(OR(PROP(7), OR(PROP(2), PROP(1))), OR(PROP(2), OR(PROP(7), PROP(1)))), REPLACEPROP ( 56, PROP(3), PROP(2) ) ), LINE ( IMPL(OR(PROP(7), OR(PROP(2), PROP(3))), OR(PROP(2), OR(PROP(7), PROP(3)))), REPLACEPROP ( 57, PROP(1), PROP(3) ) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))), REPLACEPROP ( 58, PROP(7), PROP(1) ) ) ) ) ), PARAGRAPH ( LABEL ("prin5"), "The fifth primitive proposition is our fourth axiom:", PROPOSITION ( SENTENCE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(OR(PROP(3), PROP(1)), OR(PROP(3), PROP(2)))) ), PROOF ( LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(OR(PROP(3), PROP(1)), OR(PROP(3), PROP(2)))), ADDAXIOM ( LINK ("axiom4")) ) ) ) ) ) )