MODULE ( HEADER ( SPEC ( NAME ("predtheo1"), VERSION ("1.00.00"), VERSION("1.00.00"), LOCATIONS ( LOCATION (".") ) ), HEADLINE ("First theorems of Predicate Calculus"), DESCRIPTION ( "This module includes first proofs of predicate calculus theorems." ), EMAIL ("principa@meyling.com"), AUTHORS ( AUTHOR ("Michael Meyling",EMAIL ("michael@meyling.com")) ) ), IMPORTS ( IMPORT ( SPEC ( NAME ("propaxiom"), VERSION ("1.00.00"), VERSION ("1.00.00"), LOCATIONS ( LOCATION (".") ) ) ), IMPORT ( SPEC ( NAME ("predaxiom"), VERSION ("1.00.00"), VERSION ("1.00.00"), LOCATIONS ( LOCATION (".") ) ) ) ), PARAGRAPHS ( PARAGRAPH ( LABEL ("theo1"), "First we prove a simple implication:", PROPOSITION ( SENTENCE ( IMPL(EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))), NOT(FORALL(VAR(1), NOT(PREDVAR(1, L(VAR(1))))))) ), PROOF ( LINE ( IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), PREDVAR(1, L(VAR(2)))), ADDAXIOM ( LINK ("axiom5")) ), LINE ( IMPL(FORALL(VAR(1), NOT(PREDVAR(1, L(VAR(1))))), NOT(PREDVAR(1, L(VAR(2))))), REPLACEPREDICATE ( 1, PREDVAR(1, L(SPATTERN(1))), NOT(PREDVAR(1, L(SPATTERN(1)))) ) ), LINE ( OR(NOT(FORALL(VAR(1), NOT(PREDVAR(1, L(VAR(1)))))), NOT(PREDVAR(1, L(VAR(2))))), USEABBREVIATION (2, LINK ("impl"), 1) ), LINE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), ADDAXIOM ( LINK ("axiom3")) ), LINE ( IMPL(OR(NOT(FORALL(VAR(1), NOT(PREDVAR(1, L(VAR(1)))))), PROP(2)), OR(PROP(2), NOT(FORALL(VAR(1), NOT(PREDVAR(1, L(VAR(1)))))))), REPLACEPROP ( 4, PROP(1), NOT(FORALL(VAR(1), NOT(PREDVAR(1, L(VAR(1)))))) ) ), LINE ( IMPL(OR(NOT(FORALL(VAR(1), NOT(PREDVAR(1, L(VAR(1)))))), NOT(PREDVAR(1, L(VAR(2))))), OR(NOT(PREDVAR(1, L(VAR(2)))), NOT(FORALL(VAR(1), NOT(PREDVAR(1, L(VAR(1)))))))), REPLACEPROP ( 5, PROP(2), NOT(PREDVAR(1, L(VAR(2)))) ) ), LINE ( OR(NOT(PREDVAR(1, L(VAR(2)))), NOT(FORALL(VAR(1), NOT(PREDVAR(1, L(VAR(1))))))), MODUSPONENS (3, 6) ), LINE ( IMPL(PREDVAR(1, L(VAR(2))), NOT(FORALL(VAR(1), NOT(PREDVAR(1, L(VAR(1))))))), REVERSEABBREVIATION (7, LINK ("impl"), 1) ), LINE ( IMPL(EXISTS(VAR(2), PREDVAR(1, L(VAR(2)))), NOT(FORALL(VAR(1), NOT(PREDVAR(1, L(VAR(1))))))), PARTICULARIZATION (8, VAR(2)) ), LINE ( IMPL(EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))), NOT(FORALL(VAR(1), NOT(PREDVAR(1, L(VAR(1))))))), RENAMEBOUNDVARIABLE (9, VAR(2), VAR(1), 1) ) ) ) ) ) )