MODULE (
  HEADER (
    SPEC (
      NAME ("predtheo2"),
      VERSION ("1.00.00"),
      VERSION ("1.02.00"),
      LOCATIONS (
        LOCATION ("http://www.qedeq.org/0_00_53")
      )
    ),
    HEADLINE ("Some more theorems of Predicate Calculus"),
    DESCRIPTION (
      "This module includes first proofs of predicate calculus theorems."
    ),
    EMAIL ("module@qedeq.org"),
    AUTHORS (
      AUTHOR ("Michael Meyling",EMAIL ("mime@qedeq.org"))
    )
  ),
  IMPORTS (
    IMPORT (
      SPEC (
        NAME ("predaxiom"),
        VERSION ("1.00.00"),
        VERSION ("1.00.00"),
        LOCATIONS (
          LOCATION ("."),
          LOCATION ("http://www.qedeq.org/0_00_53")
        )
      )
    ),
    IMPORT (
      SPEC (
        NAME ("prophilbert3"),
        VERSION ("1.00.00"),
        VERSION ("1.02.00"),
        LOCATIONS (
          LOCATION ("."),
          LOCATION ("http://www.qedeq.org/0_00_53")
        )
      )
    )
  ),
  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(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))),
            HYPOTHETICALSYLLOGISM (1, 2)
          )
        )
      )
    ),
    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(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), NOT(PREDVAR(1, L(VAR(2))))),
            APPLYSENTENCE (1, LINK("hilb7"))
          ),
          LINE (
            IMPL(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))), FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))),
            GENERALIZATION (2, VAR(2))
          ),
          LINE (
            IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), NOT(NOT(EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))))),
            APPLYSENTENCE (3, LINK("hilb7"))
          ),
          LINE (
            IMPL(NOT(FORALL(VAR(2), NOT(PREDVAR(1, L(VAR(2)))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))),
            IMPLICATIONEQUIVALENT (4, LINK("hilb6"), LINK("hilb5"), 1)
          ),
          LINE (
            IMPL(NOT(FORALL(VAR(1), NOT(PREDVAR(1, L(VAR(1)))))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))),
            RENAMEBOUNDVARIABLE (5, 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(2), PREDVAR(1, L(VAR(2)))), PREDVAR(1, L(VAR(4)))),
            SUBSTLINE (1)
          ),
          LINE (
            IMPL(FORALL(VAR(2), PREDVAR(1, L(VAR(3), VAR(2)))), PREDVAR(1, L(VAR(3), VAR(4)))),
            REPLACEPREDICATE (
              2, 
              PREDVAR(1, L(SPATTERN(1))),
              PREDVAR(1, L(VAR(3), SPATTERN(1)))
            )
          ),
          LINE (
            IMPL(FORALL(VAR(5), PREDVAR(1, L(VAR(5)))), PREDVAR(1, L(VAR(3)))),
            SUBSTLINE (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 (
              4, 
              PREDVAR(1, L(SPATTERN(1))),
              FORALL(VAR(6), PREDVAR(1, L(SPATTERN(1), VAR(6))))
            )
          ),
          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))))),
            SUBSTLINE (5)
          ),
          LINE (
            IMPL(FORALL(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), PREDVAR(1, L(VAR(3), VAR(4)))),
            HYPOTHETICALSYLLOGISM (6, 3)
          ),
          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 (7, 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 (8, 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 (9, 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 (10, VAR(3), VAR(1), 1)
          )
        )
      )
    ),
    PARAGRAPH (
      LABEL ("predtheo5"),
      "Implication of changing sequence 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(2), PREDVAR(1, L(VAR(2)))), PREDVAR(1, L(VAR(4)))),
            SUBSTLINE (1)
          ),
          LINE (
            IMPL(FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2)))), PREDVAR(1, L(VAR(1), VAR(4)))),
            REPLACEPREDICATE (
              2, 
              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(1))), EXISTS(VAR(3), PREDVAR(1, L(VAR(3))))),
            SUBSTLINE (4)
          ),
          LINE (
            IMPL(PREDVAR(1, L(VAR(1), VAR(4))), EXISTS(VAR(3), PREDVAR(1, L(VAR(3), VAR(4))))),
            REPLACEPREDICATE (
              5, 
              PREDVAR(1, L(SPATTERN(1))),
              PREDVAR(1, L(SPATTERN(1), VAR(4)))
            )
          ),
          LINE (
            IMPL(FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2)))), EXISTS(VAR(3), PREDVAR(1, L(VAR(3), VAR(4))))),
            HYPOTHETICALSYLLOGISM (3, 6)
          ),
          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 (7, 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 (8, VAR(4))
          ),
          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)))))),
            SUBSTLINE (9)
          )
        )
      )
    )
  )
)