MODULE ( HEADER ( SPEC ( NAME ("predtheo2"), VERSION ("1.00.00"), VERSION ("1.00.00"), LOCATIONS ( LOCATION (".") ) ), HEADLINE ("Some more 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 ("predaxiom"), VERSION ("1.00.00"), VERSION ("1.00.00"), LOCATIONS ( LOCATION (".") ) ) ), IMPORT ( SPEC ( NAME ("prophilbert3"), VERSION ("1.00.00"), VERSION ("1.00.00"), LOCATIONS ( LOCATION (".") ) ) ) ), PARAGRAPHS ( PARAGRAPH ( LABEL ("predtheo1"), "A simple implication:", PROPOSITION ( SENTENCE ( IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), EXISTS(VAR(1), 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(PREDVAR(1, L(VAR(2))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), ADDAXIOM ( LINK ("axiom6")) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(3), PROP(1)), IMPL(PROP(3), PROP(2)))), ADDSENTENCE ( LINK ("hilb1")) ), LINE ( IMPL(IMPL(PROP(4), PROP(2)), IMPL(IMPL(PROP(3), PROP(4)), IMPL(PROP(3), PROP(2)))), REPLACEPROP ( 3, PROP(1), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(4), PROP(5)), IMPL(IMPL(PROP(3), PROP(4)), IMPL(PROP(3), PROP(5)))), REPLACEPROP ( 4, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(4), PROP(5)), IMPL(IMPL(PROP(6), PROP(4)), IMPL(PROP(6), PROP(5)))), REPLACEPROP ( 5, PROP(3), PROP(6) ) ), LINE ( IMPL(IMPL(PREDVAR(1, L(VAR(2))), PROP(5)), IMPL(IMPL(PROP(6), PREDVAR(1, L(VAR(2)))), IMPL(PROP(6), PROP(5)))), REPLACEPROP ( 6, PROP(4), PREDVAR(1, L(VAR(2))) ) ), LINE ( IMPL(IMPL(PREDVAR(1, L(VAR(2))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), IMPL(IMPL(PROP(6), PREDVAR(1, L(VAR(2)))), IMPL(PROP(6), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), REPLACEPROP ( 7, PROP(5), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))) ) ), LINE ( IMPL(IMPL(PREDVAR(1, L(VAR(2))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), IMPL(IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), PREDVAR(1, L(VAR(2)))), IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), REPLACEPROP ( 8, PROP(6), FORALL(VAR(1), PREDVAR(1, L(VAR(1)))) ) ), LINE ( IMPL(IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), PREDVAR(1, L(VAR(2)))), IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))), MODUSPONENS (2, 9) ), LINE ( IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), MODUSPONENS (1, 10) ) ) ) ), PARAGRAPH ( LABEL ("predtheo2"), "A well known 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) ) ) ) ), PARAGRAPH ( LABEL ("predtheo3"), "The reverse is also true:", PROPOSITION ( SENTENCE ( IMPL(NOT(FORALL(VAR(1), NOT(PREDVAR(1, L(VAR(1)))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))) ), PROOF ( LINE ( IMPL(PREDVAR(1, L(VAR(2))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), ADDAXIOM ( LINK ("axiom6")) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(NOT(PROP(2)), NOT(PROP(1)))), ADDSENTENCE ( LINK ("hilb7")) ), LINE ( IMPL(IMPL(PROP(3), PROP(2)), IMPL(NOT(PROP(2)), NOT(PROP(3)))), REPLACEPROP ( 2, PROP(1), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(3), PROP(4)), IMPL(NOT(PROP(4)), NOT(PROP(3)))), REPLACEPROP ( 3, PROP(2), PROP(4) ) ), LINE ( IMPL(IMPL(PREDVAR(1, L(VAR(2))), PROP(4)), IMPL(NOT(PROP(4)), NOT(PREDVAR(1, L(VAR(2)))))), REPLACEPROP ( 4, PROP(3), PREDVAR(1, L(VAR(2))) ) ), LINE ( IMPL(IMPL(PREDVAR(1, L(VAR(2))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), IMPL(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), NOT(PREDVAR(1, L(VAR(2)))))), REPLACEPROP ( 5, PROP(4), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))) ) ), LINE ( IMPL(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), NOT(PREDVAR(1, L(VAR(2))))), MODUSPONENS (1, 6) ), LINE ( IMPL(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), GENERALIZATION (7, VAR(2)) ), LINE ( IMPL(IMPL(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), PROP(4)), IMPL(NOT(PROP(4)), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))))), REPLACEPROP ( 4, PROP(3), NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))) ) ), LINE ( IMPL(IMPL(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))))), REPLACEPROP ( 9, PROP(4), FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))) ) ), LINE ( IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), MODUSPONENS (8, 10) ), LINE ( IMPL(NOT(NOT(PROP(1))), PROP(1)), ADDSENTENCE ( LINK ("hilb6")) ), LINE ( IMPL(NOT(NOT(PROP(2))), PROP(2)), REPLACEPROP ( 12, PROP(1), PROP(2) ) ), LINE ( IMPL(NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), REPLACEPROP ( 13, PROP(2), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), OR(NOT(PROP(1)), PROP(2))), ADDSENTENCE ( LINK ("defimpl1")) ), LINE ( IMPL(OR(NOT(PROP(1)), PROP(2)), IMPL(PROP(1), PROP(2))), ADDSENTENCE ( LINK ("defimpl2")) ), 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 ( 17, PROP(1), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(4), PROP(5)), IMPL(OR(PROP(3), PROP(4)), OR(PROP(3), PROP(5)))), REPLACEPROP ( 18, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(4), PROP(5)), IMPL(OR(PROP(6), PROP(4)), OR(PROP(6), PROP(5)))), REPLACEPROP ( 19, PROP(3), PROP(6) ) ), LINE ( IMPL(IMPL(NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))), PROP(5)), IMPL(OR(PROP(6), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), OR(PROP(6), PROP(5)))), REPLACEPROP ( 20, PROP(4), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))) ) ), LINE ( IMPL(IMPL(NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), IMPL(OR(PROP(6), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), OR(PROP(6), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), REPLACEPROP ( 21, PROP(5), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))) ) ), LINE ( IMPL(IMPL(NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), IMPL(OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), REPLACEPROP ( 22, PROP(6), NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))) ) ), LINE ( IMPL(OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))), MODUSPONENS (14, 23) ), LINE ( IMPL(IMPL(PROP(3), PROP(2)), OR(NOT(PROP(3)), PROP(2))), REPLACEPROP ( 15, PROP(1), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(3), PROP(4)), OR(NOT(PROP(3)), PROP(4))), REPLACEPROP ( 25, PROP(2), PROP(4) ) ), LINE ( IMPL(IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), PROP(4)), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), PROP(4))), REPLACEPROP ( 26, PROP(3), NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))) ) ), LINE ( IMPL(IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))))), REPLACEPROP ( 27, PROP(4), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(3), PROP(1)), IMPL(PROP(3), PROP(2)))), ADDSENTENCE ( LINK ("hilb1")) ), LINE ( IMPL(IMPL(PROP(4), PROP(2)), IMPL(IMPL(PROP(3), PROP(4)), IMPL(PROP(3), PROP(2)))), REPLACEPROP ( 29, PROP(1), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(4), PROP(5)), IMPL(IMPL(PROP(3), PROP(4)), IMPL(PROP(3), PROP(5)))), REPLACEPROP ( 30, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(4), PROP(5)), IMPL(IMPL(PROP(6), PROP(4)), IMPL(PROP(6), PROP(5)))), REPLACEPROP ( 31, PROP(3), PROP(6) ) ), LINE ( IMPL(IMPL(OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), PROP(5)), IMPL(IMPL(PROP(6), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))))), IMPL(PROP(6), PROP(5)))), REPLACEPROP ( 32, PROP(4), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))) ) ), LINE ( IMPL(IMPL(OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))), IMPL(IMPL(PROP(6), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))))), IMPL(PROP(6), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))))), REPLACEPROP ( 33, PROP(5), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))) ) ), LINE ( IMPL(IMPL(OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))), IMPL(IMPL(IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))))), IMPL(IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))))), REPLACEPROP ( 34, PROP(6), IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))) ) ), LINE ( IMPL(IMPL(IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))))), IMPL(IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), MODUSPONENS (24, 35) ), LINE ( IMPL(IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))), MODUSPONENS (28, 36) ), LINE ( IMPL(OR(NOT(PROP(3)), PROP(2)), IMPL(PROP(3), PROP(2))), REPLACEPROP ( 16, PROP(1), PROP(3) ) ), LINE ( IMPL(OR(NOT(PROP(3)), PROP(4)), IMPL(PROP(3), PROP(4))), REPLACEPROP ( 38, PROP(2), PROP(4) ) ), LINE ( IMPL(OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), PROP(4)), IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), PROP(4))), REPLACEPROP ( 39, PROP(3), NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))) ) ), LINE ( IMPL(OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))), REPLACEPROP ( 40, PROP(4), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))) ) ), LINE ( IMPL(IMPL(OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), PROP(5)), IMPL(IMPL(PROP(6), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))), IMPL(PROP(6), PROP(5)))), REPLACEPROP ( 32, PROP(4), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))) ) ), LINE ( IMPL(IMPL(OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))), IMPL(IMPL(PROP(6), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))), IMPL(PROP(6), IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))))), REPLACEPROP ( 42, PROP(5), IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))) ) ), LINE ( IMPL(IMPL(OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))), IMPL(IMPL(IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))), IMPL(IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))))), REPLACEPROP ( 43, PROP(6), IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))) ) ), LINE ( IMPL(IMPL(IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), OR(NOT(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2))))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))), IMPL(IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), MODUSPONENS (41, 44) ), LINE ( IMPL(IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))), IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))), MODUSPONENS (37, 45) ), LINE ( IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), MODUSPONENS (11, 46) ), LINE ( IMPL(NOT(FORALL(VAR(1), NOT(PREDVAR(1, L(VAR(1)))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), RENAMEBOUNDVARIABLE (47, VAR(2), VAR(1), 1) ) ) ) ), PARAGRAPH ( LABEL ("predtheo4"), "Exchange of universal quantors:", PROPOSITION ( SENTENCE ( IMPL(FORALL(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), FORALL(VAR(2), FORALL(VAR(1), PREDVAR(1, L(VAR(1), VAR(2)))))) ), PROOF ( LINE ( IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), PREDVAR(1, L(VAR(2)))), ADDAXIOM ( LINK ("axiom5")) ), LINE ( IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), PREDVAR(1, L(VAR(6)))), RENAMEFREEVARIABLE (1, VAR(2), VAR(6)) ), LINE ( IMPL(FORALL(VAR(7), PREDVAR(1, L(VAR(7)))), PREDVAR(1, L(VAR(6)))), RENAMEBOUNDVARIABLE (2, VAR(1), VAR(7), 1) ), LINE ( IMPL(FORALL(VAR(7), PREDVAR(1, L(VAR(7)))), PREDVAR(1, L(VAR(4)))), RENAMEFREEVARIABLE (3, VAR(6), VAR(4)) ), LINE ( IMPL(FORALL(VAR(2), PREDVAR(1, L(VAR(2)))), PREDVAR(1, L(VAR(4)))), RENAMEBOUNDVARIABLE (4, VAR(7), VAR(2), 1) ), LINE ( IMPL(FORALL(VAR(2), PREDVAR(1, L(VAR(3), VAR(2)))), PREDVAR(1, L(VAR(3), VAR(4)))), REPLACEPREDICATE ( 5, PREDVAR(1, L(SPATTERN(1))), PREDVAR(1, L(VAR(3), SPATTERN(1))) ) ), LINE ( IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), PREDVAR(1, L(VAR(7)))), RENAMEFREEVARIABLE (1, VAR(2), VAR(7)) ), LINE ( IMPL(FORALL(VAR(8), PREDVAR(1, L(VAR(8)))), PREDVAR(1, L(VAR(7)))), RENAMEBOUNDVARIABLE (7, VAR(1), VAR(8), 1) ), LINE ( IMPL(FORALL(VAR(8), PREDVAR(1, L(VAR(8)))), PREDVAR(1, L(VAR(3)))), RENAMEFREEVARIABLE (8, VAR(7), VAR(3)) ), LINE ( IMPL(FORALL(VAR(5), PREDVAR(1, L(VAR(5)))), PREDVAR(1, L(VAR(3)))), RENAMEBOUNDVARIABLE (9, VAR(8), VAR(5), 1) ), LINE ( IMPL(FORALL(VAR(5), FORALL(VAR(6), PREDVAR(1, L(VAR(5), VAR(6))))), FORALL(VAR(6), PREDVAR(1, L(VAR(3), VAR(6))))), REPLACEPREDICATE ( 10, PREDVAR(1, L(SPATTERN(1))), FORALL(VAR(6), PREDVAR(1, L(SPATTERN(1), VAR(6)))) ) ), LINE ( IMPL(FORALL(VAR(12), FORALL(VAR(6), PREDVAR(1, L(VAR(12), VAR(6))))), FORALL(VAR(6), PREDVAR(1, L(VAR(3), VAR(6))))), RENAMEBOUNDVARIABLE (11, VAR(5), VAR(12), 1) ), LINE ( IMPL(FORALL(VAR(12), FORALL(VAR(13), PREDVAR(1, L(VAR(12), VAR(13))))), FORALL(VAR(6), PREDVAR(1, L(VAR(3), VAR(6))))), RENAMEBOUNDVARIABLE (12, VAR(6), VAR(13), 1) ), LINE ( IMPL(FORALL(VAR(12), FORALL(VAR(13), PREDVAR(1, L(VAR(12), VAR(13))))), FORALL(VAR(14), PREDVAR(1, L(VAR(3), VAR(14))))), RENAMEBOUNDVARIABLE (13, VAR(6), VAR(14), 1) ), LINE ( IMPL(FORALL(VAR(1), FORALL(VAR(13), PREDVAR(1, L(VAR(1), VAR(13))))), FORALL(VAR(14), PREDVAR(1, L(VAR(3), VAR(14))))), RENAMEBOUNDVARIABLE (14, VAR(12), VAR(1), 1) ), LINE ( IMPL(FORALL(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), FORALL(VAR(14), PREDVAR(1, L(VAR(3), VAR(14))))), RENAMEBOUNDVARIABLE (15, VAR(13), VAR(2), 1) ), LINE ( IMPL(FORALL(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), FORALL(VAR(2), PREDVAR(1, L(VAR(3), VAR(2))))), RENAMEBOUNDVARIABLE (16, VAR(14), VAR(2), 1) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(3), PROP(1)), IMPL(PROP(3), PROP(2)))), ADDSENTENCE ( LINK ("hilb1")) ), LINE ( IMPL(IMPL(PROP(5), PROP(2)), IMPL(IMPL(PROP(3), PROP(5)), IMPL(PROP(3), PROP(2)))), REPLACEPROP ( 18, PROP(1), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(5), PROP(6)), IMPL(IMPL(PROP(3), PROP(5)), IMPL(PROP(3), PROP(6)))), REPLACEPROP ( 19, PROP(2), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(5), PROP(6)), IMPL(IMPL(PROP(7), PROP(5)), IMPL(PROP(7), PROP(6)))), REPLACEPROP ( 20, PROP(3), PROP(7) ) ), LINE ( IMPL(IMPL(FORALL(VAR(2), PREDVAR(1, L(VAR(3), VAR(2)))), PROP(6)), IMPL(IMPL(PROP(7), FORALL(VAR(2), PREDVAR(1, L(VAR(3), VAR(2))))), IMPL(PROP(7), PROP(6)))), REPLACEPROP ( 21, PROP(5), FORALL(VAR(2), PREDVAR(1, L(VAR(3), VAR(2)))) ) ), LINE ( IMPL(IMPL(FORALL(VAR(2), PREDVAR(1, L(VAR(3), VAR(2)))), PREDVAR(1, L(VAR(3), VAR(4)))), IMPL(IMPL(PROP(7), FORALL(VAR(2), PREDVAR(1, L(VAR(3), VAR(2))))), IMPL(PROP(7), PREDVAR(1, L(VAR(3), VAR(4)))))), REPLACEPROP ( 22, PROP(6), PREDVAR(1, L(VAR(3), VAR(4))) ) ), LINE ( IMPL(IMPL(FORALL(VAR(2), PREDVAR(1, L(VAR(3), VAR(2)))), PREDVAR(1, L(VAR(3), VAR(4)))), IMPL(IMPL(FORALL(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), FORALL(VAR(2), PREDVAR(1, L(VAR(3), VAR(2))))), IMPL(FORALL(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), PREDVAR(1, L(VAR(3), VAR(4)))))), REPLACEPROP ( 23, PROP(7), FORALL(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))) ) ), LINE ( IMPL(IMPL(FORALL(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), FORALL(VAR(2), PREDVAR(1, L(VAR(3), VAR(2))))), IMPL(FORALL(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), PREDVAR(1, L(VAR(3), VAR(4))))), MODUSPONENS (6, 24) ), LINE ( IMPL(FORALL(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), PREDVAR(1, L(VAR(3), VAR(4)))), MODUSPONENS (17, 25) ), LINE ( IMPL(FORALL(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), FORALL(VAR(3), PREDVAR(1, L(VAR(3), VAR(4))))), GENERALIZATION (26, VAR(3)) ), LINE ( IMPL(FORALL(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), FORALL(VAR(4), FORALL(VAR(3), PREDVAR(1, L(VAR(3), VAR(4)))))), GENERALIZATION (27, VAR(4)) ), LINE ( IMPL(FORALL(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), FORALL(VAR(2), FORALL(VAR(3), PREDVAR(1, L(VAR(3), VAR(2)))))), RENAMEBOUNDVARIABLE (28, VAR(4), VAR(2), 1) ), LINE ( IMPL(FORALL(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), FORALL(VAR(2), FORALL(VAR(1), PREDVAR(1, L(VAR(1), VAR(2)))))), RENAMEBOUNDVARIABLE (29, VAR(3), VAR(1), 1) ) ) ) ), PARAGRAPH ( LABEL ("predtheo5"), "Implication of changing seqence of existence and universal quantor:", PROPOSITION ( SENTENCE ( IMPL(EXISTS(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), FORALL(VAR(2), EXISTS(VAR(1), PREDVAR(1, L(VAR(1), VAR(2)))))) ), PROOF ( LINE ( IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), PREDVAR(1, L(VAR(2)))), ADDAXIOM ( LINK ("axiom5")) ), LINE ( IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), PREDVAR(1, L(VAR(6)))), RENAMEFREEVARIABLE (1, VAR(2), VAR(6)) ), LINE ( IMPL(FORALL(VAR(7), PREDVAR(1, L(VAR(7)))), PREDVAR(1, L(VAR(6)))), RENAMEBOUNDVARIABLE (2, VAR(1), VAR(7), 1) ), LINE ( IMPL(FORALL(VAR(7), PREDVAR(1, L(VAR(7)))), PREDVAR(1, L(VAR(4)))), RENAMEFREEVARIABLE (3, VAR(6), VAR(4)) ), LINE ( IMPL(FORALL(VAR(2), PREDVAR(1, L(VAR(2)))), PREDVAR(1, L(VAR(4)))), RENAMEBOUNDVARIABLE (4, VAR(7), VAR(2), 1) ), LINE ( IMPL(FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2)))), PREDVAR(1, L(VAR(1), VAR(4)))), REPLACEPREDICATE ( 5, PREDVAR(1, L(SPATTERN(1))), PREDVAR(1, L(VAR(1), SPATTERN(1))) ) ), LINE ( IMPL(PREDVAR(1, L(VAR(2))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), ADDAXIOM ( LINK ("axiom6")) ), LINE ( IMPL(PREDVAR(1, L(VAR(5))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), RENAMEFREEVARIABLE (7, VAR(2), VAR(5)) ), LINE ( IMPL(PREDVAR(1, L(VAR(5))), EXISTS(VAR(6), PREDVAR(1, L(VAR(6))))), RENAMEBOUNDVARIABLE (8, VAR(1), VAR(6), 1) ), LINE ( IMPL(PREDVAR(1, L(VAR(1))), EXISTS(VAR(6), PREDVAR(1, L(VAR(6))))), RENAMEFREEVARIABLE (9, VAR(5), VAR(1)) ), LINE ( IMPL(PREDVAR(1, L(VAR(1))), EXISTS(VAR(3), PREDVAR(1, L(VAR(3))))), RENAMEBOUNDVARIABLE (10, VAR(6), VAR(3), 1) ), LINE ( IMPL(PREDVAR(1, L(VAR(1), VAR(4))), EXISTS(VAR(3), PREDVAR(1, L(VAR(3), VAR(4))))), REPLACEPREDICATE ( 11, PREDVAR(1, L(SPATTERN(1))), PREDVAR(1, L(SPATTERN(1), VAR(4))) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(3), PROP(1)), IMPL(PROP(3), PROP(2)))), ADDSENTENCE ( LINK ("hilb1")) ), LINE ( IMPL(IMPL(PROP(5), PROP(2)), IMPL(IMPL(PROP(3), PROP(5)), IMPL(PROP(3), PROP(2)))), REPLACEPROP ( 13, PROP(1), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(5), PROP(6)), IMPL(IMPL(PROP(3), PROP(5)), IMPL(PROP(3), PROP(6)))), REPLACEPROP ( 14, PROP(2), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(5), PROP(6)), IMPL(IMPL(PROP(7), PROP(5)), IMPL(PROP(7), PROP(6)))), REPLACEPROP ( 15, PROP(3), PROP(7) ) ), LINE ( IMPL(IMPL(PREDVAR(1, L(VAR(1), VAR(4))), PROP(6)), IMPL(IMPL(PROP(7), PREDVAR(1, L(VAR(1), VAR(4)))), IMPL(PROP(7), PROP(6)))), REPLACEPROP ( 16, PROP(5), PREDVAR(1, L(VAR(1), VAR(4))) ) ), LINE ( IMPL(IMPL(PREDVAR(1, L(VAR(1), VAR(4))), EXISTS(VAR(3), PREDVAR(1, L(VAR(3), VAR(4))))), IMPL(IMPL(PROP(7), PREDVAR(1, L(VAR(1), VAR(4)))), IMPL(PROP(7), EXISTS(VAR(3), PREDVAR(1, L(VAR(3), VAR(4))))))), REPLACEPROP ( 17, PROP(6), EXISTS(VAR(3), PREDVAR(1, L(VAR(3), VAR(4)))) ) ), LINE ( IMPL(IMPL(PREDVAR(1, L(VAR(1), VAR(4))), EXISTS(VAR(3), PREDVAR(1, L(VAR(3), VAR(4))))), IMPL(IMPL(FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2)))), PREDVAR(1, L(VAR(1), VAR(4)))), IMPL(FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2)))), EXISTS(VAR(3), PREDVAR(1, L(VAR(3), VAR(4))))))), REPLACEPROP ( 18, PROP(7), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2)))) ) ), LINE ( IMPL(IMPL(FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2)))), PREDVAR(1, L(VAR(1), VAR(4)))), IMPL(FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2)))), EXISTS(VAR(3), PREDVAR(1, L(VAR(3), VAR(4)))))), MODUSPONENS (12, 19) ), LINE ( IMPL(FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2)))), EXISTS(VAR(3), PREDVAR(1, L(VAR(3), VAR(4))))), MODUSPONENS (6, 20) ), LINE ( IMPL(EXISTS(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), EXISTS(VAR(3), PREDVAR(1, L(VAR(3), VAR(4))))), PARTICULARIZATION (21, VAR(1)) ), LINE ( IMPL(EXISTS(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), FORALL(VAR(4), EXISTS(VAR(3), PREDVAR(1, L(VAR(3), VAR(4)))))), GENERALIZATION (22, VAR(4)) ), LINE ( IMPL(EXISTS(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), FORALL(VAR(12), EXISTS(VAR(3), PREDVAR(1, L(VAR(3), VAR(12)))))), RENAMEBOUNDVARIABLE (23, VAR(4), VAR(12), 1) ), LINE ( IMPL(EXISTS(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), FORALL(VAR(12), EXISTS(VAR(13), PREDVAR(1, L(VAR(13), VAR(12)))))), RENAMEBOUNDVARIABLE (24, VAR(3), VAR(13), 1) ), LINE ( IMPL(EXISTS(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), FORALL(VAR(2), EXISTS(VAR(13), PREDVAR(1, L(VAR(13), VAR(2)))))), RENAMEBOUNDVARIABLE (25, VAR(12), VAR(2), 1) ), LINE ( IMPL(EXISTS(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), FORALL(VAR(2), EXISTS(VAR(1), PREDVAR(1, L(VAR(1), VAR(2)))))), RENAMEBOUNDVARIABLE (26, VAR(13), VAR(1), 1) ) ) ) ) ) )