MODULE ( HEADER ( SPEC ( NAME ("proptheo1"), VERSION ("1.00.00"), VERSION ("1.00.00"), LOCATIONS ( LOCATION ("http://www.qedeq.org/0_00_53") ) ), HEADLINE ("First theorems of Propositional Calculus"), DESCRIPTION ( "This module includes first proofs of propositional calculus theorems." ), 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 ("theo1"), "First we prove a well known tautology:", PROPOSITION ( SENTENCE ( OR(NOT(PROP(1)), 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(OR(PROP(1), PROP(1)), PROP(2)), IMPL(OR(PROP(3), OR(PROP(1), PROP(1))), OR(PROP(3), PROP(2)))), REPLACEPROP ( 1, PROP(1), OR(PROP(1), PROP(1)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(1)), PROP(1)), IMPL(OR(PROP(3), OR(PROP(1), PROP(1))), OR(PROP(3), PROP(1)))), REPLACEPROP ( 2, PROP(2), PROP(1) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(1)), PROP(1)), IMPL(OR(NOT(PROP(1)), OR(PROP(1), PROP(1))), OR(NOT(PROP(1)), PROP(1)))), REPLACEPROP ( 3, PROP(3), NOT(PROP(1)) ) ), LINE ( IMPL(OR(PROP(1), PROP(1)), PROP(1)), ADDAXIOM ( LINK ("axiom1")) ), LINE ( IMPL(OR(NOT(PROP(1)), OR(PROP(1), PROP(1))), OR(NOT(PROP(1)), PROP(1))), MODUSPONENS (5, 4) ), LINE ( IMPL(IMPL(PROP(1), OR(PROP(1), PROP(1))), OR(NOT(PROP(1)), PROP(1))), REVERSEABBREVIATION (6, LINK ("impl"), 1) ), LINE ( IMPL(PROP(1), OR(PROP(1), PROP(2))), ADDAXIOM ( LINK ("axiom2")) ), LINE ( IMPL(PROP(1), OR(PROP(1), PROP(1))), REPLACEPROP ( 8, PROP(2), PROP(1) ) ), LINE ( OR(NOT(PROP(1)), PROP(1)), MODUSPONENS (9, 7) ) ) ) ), PARAGRAPH ( LABEL ("theo2"), "We just use our first sentence to get the second theorem:", PROPOSITION ( SENTENCE ( IMPL(PROP(1), PROP(1)) ), PROOF ( LINE ( OR(NOT(PROP(1)), PROP(1)), ADDSENTENCE ( LINK ("theo1")) ), LINE ( IMPL(PROP(1), PROP(1)), REVERSEABBREVIATION (1, LINK ("impl"), 1) ) ) ) ), PARAGRAPH ( LABEL ("theo3"), "And another use of the first theorem, to get the law of the excluded middle (tertium non datur):", PROPOSITION ( SENTENCE ( OR(PROP(1), NOT(PROP(1))) ), PROOF ( LINE ( OR(NOT(PROP(1)), PROP(1)), ADDSENTENCE ( LINK ("theo1")) ), LINE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), ADDAXIOM ( LINK ("axiom3")) ), LINE ( IMPL(OR(NOT(PROP(1)), PROP(2)), OR(PROP(2), NOT(PROP(1)))), REPLACEPROP ( 2, PROP(1), NOT(PROP(1)) ) ), LINE ( IMPL(OR(NOT(PROP(1)), PROP(1)), OR(PROP(1), NOT(PROP(1)))), REPLACEPROP ( 3, PROP(2), PROP(1) ) ), LINE ( OR(PROP(1), NOT(PROP(1))), MODUSPONENS (1, 4) ) ) ) ), PARAGRAPH ( LABEL ("theo4"), "Also trivial is:", PROPOSITION ( SENTENCE ( IMPL(PROP(1), NOT(NOT(PROP(1)))) ), PROOF ( LINE ( OR(PROP(1), NOT(PROP(1))), ADDSENTENCE ( LINK ("theo3")) ), LINE ( OR(NOT(PROP(1)), NOT(NOT(PROP(1)))), REPLACEPROP ( 1, PROP(1), NOT(PROP(1)) ) ), LINE ( IMPL(PROP(1), NOT(NOT(PROP(1)))), REVERSEABBREVIATION (2, LINK ("impl"), 1) ) ) ) ), PARAGRAPH ( LABEL ("theo5"), "Three negations:", PROPOSITION ( SENTENCE ( OR(PROP(1), NOT(NOT(NOT(PROP(1))))) ), PROOF ( LINE ( IMPL(PROP(1), NOT(NOT(PROP(1)))), ADDSENTENCE ( LINK ("theo4")) ), 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(1), NOT(NOT(PROP(1)))), IMPL(OR(PROP(3), PROP(1)), OR(PROP(3), NOT(NOT(PROP(1)))))), REPLACEPROP ( 2, PROP(2), NOT(NOT(PROP(1))) ) ), LINE ( IMPL(OR(PROP(3), PROP(1)), OR(PROP(3), NOT(NOT(PROP(1))))), MODUSPONENS (1, 3) ), LINE ( IMPL(OR(PROP(3), NOT(PROP(1))), OR(PROP(3), NOT(NOT(NOT(PROP(1)))))), REPLACEPROP ( 4, PROP(1), NOT(PROP(1)) ) ), LINE ( IMPL(OR(PROP(1), NOT(PROP(1))), OR(PROP(1), NOT(NOT(NOT(PROP(1)))))), REPLACEPROP ( 5, PROP(3), PROP(1) ) ), LINE ( OR(PROP(1), NOT(PROP(1))), ADDSENTENCE ( LINK ("theo3")) ), LINE ( OR(PROP(1), NOT(NOT(NOT(PROP(1))))), MODUSPONENS (7, 6) ) ) ) ), PARAGRAPH ( LABEL ("theo6"), "Now we could prove the reverse of Proposition 4:", PROPOSITION ( SENTENCE ( IMPL(NOT(NOT(PROP(1))), PROP(1)) ), PROOF ( LINE ( OR(PROP(1), NOT(NOT(NOT(PROP(1))))), ADDSENTENCE ( LINK ("theo5")) ), LINE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), ADDAXIOM ( LINK ("axiom3")) ), LINE ( IMPL(OR(PROP(1), NOT(NOT(NOT(PROP(1))))), OR(NOT(NOT(NOT(PROP(1)))), PROP(1))), REPLACEPROP ( 2, PROP(2), NOT(NOT(NOT(PROP(1)))) ) ), LINE ( OR(NOT(NOT(NOT(PROP(1)))), PROP(1)), MODUSPONENS (1, 3) ), LINE ( IMPL(NOT(NOT(PROP(1))), PROP(1)), REVERSEABBREVIATION (4, LINK ("impl"), 1) ) ) ) ) ) )