MODULE (
  HEADER (
    SPEC (
      NAME ("predtheo3"),
      VERSION ("1.00.00"),
      VERSION ("1.02.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.02.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(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(1), PREDVAR(1, L(VAR(1)))), PREDVAR(1, L(VAR(5)))),
            RENAMEFREEVARIABLE (1, VAR(2), VAR(5))
          ),
          LINE (
            IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), PREDVAR(1, L(VAR(5)))),
            RENAMEBOUNDVARIABLE (2, VAR(2), VAR(6), 1)
          ),
          LINE (
            IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), PREDVAR(1, L(VAR(5)))),
            RENAMEBOUNDVARIABLE (4, VAR(3), VAR(5), 1)
          ),
          LINE (
            IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), PREDVAR(1, L(VAR(5)))),
            RENAMEBOUNDVARIABLE (5, VAR(2), VAR(6), 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(2)))),
            RENAMEBOUNDVARIABLE (1, VAR(3), VAR(6), 1)
          ),
          LINE (
            IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), PREDVAR(1, L(VAR(2)))),
            RENAMEBOUNDVARIABLE (7, VAR(2), VAR(7), 1)
          ),
          LINE (
            IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), PREDVAR(1, L(VAR(2)))),
            RENAMEBOUNDVARIABLE (9, VAR(3), VAR(6), 1)
          ),
          LINE (
            IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), PREDVAR(1, L(VAR(2)))),
            RENAMEBOUNDVARIABLE (10, VAR(2), VAR(7), 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(5), FORALL(VAR(6), PREDVAR(1, L(VAR(5), VAR(6))))), FORALL(VAR(6), PREDVAR(1, L(VAR(3), VAR(6))))),
            RENAMEBOUNDVARIABLE (11, VAR(9), VAR(10), 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))))),
            RENAMEBOUNDVARIABLE (12, VAR(8), VAR(11), 2)
          ),
          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))))),
            RENAMEBOUNDVARIABLE (13, VAR(7), VAR(12), 1)
          ),
          LINE (
            IMPL(FORALL(VAR(5), FORALL(VAR(6), PREDVAR(1, L(VAR(5), VAR(6))))), FORALL(VAR(6), PREDVAR(1, L(VAR(13), VAR(6))))),
            RENAMEFREEVARIABLE (14, VAR(3), VAR(13))
          ),
          LINE (
            IMPL(FORALL(VAR(5), FORALL(VAR(6), PREDVAR(1, L(VAR(5), VAR(6))))), FORALL(VAR(6), PREDVAR(1, L(VAR(13), VAR(6))))),
            RENAMEBOUNDVARIABLE (16, VAR(9), VAR(10), 1)
          ),
          LINE (
            IMPL(FORALL(VAR(5), FORALL(VAR(6), PREDVAR(1, L(VAR(5), VAR(6))))), FORALL(VAR(6), PREDVAR(1, L(VAR(13), VAR(6))))),
            RENAMEBOUNDVARIABLE (17, VAR(8), VAR(11), 2)
          ),
          LINE (
            IMPL(FORALL(VAR(5), FORALL(VAR(6), PREDVAR(1, L(VAR(5), VAR(6))))), FORALL(VAR(6), PREDVAR(1, L(VAR(13), VAR(6))))),
            RENAMEBOUNDVARIABLE (18, VAR(7), VAR(12), 1)
          ),
          LINE (
            IMPL(FORALL(VAR(5), FORALL(VAR(6), PREDVAR(1, L(VAR(5), VAR(6))))), FORALL(VAR(6), PREDVAR(1, L(VAR(13), VAR(6))))),
            RENAMEBOUNDVARIABLE (19, VAR(3), VAR(13), 1)
          ),
          LINE (
            IMPL(FORALL(VAR(1), FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2))))), PREDVAR(1, L(VAR(3), VAR(4)))),
            HYPOTHETICALSYLLOGISM (19, 6)
          ),
          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 (20, 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 (21, 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 (22, 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 (23, 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(5)))),
            RENAMEFREEVARIABLE (1, VAR(2), VAR(5))
          ),
          LINE (
            IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), PREDVAR(1, L(VAR(5)))),
            RENAMEBOUNDVARIABLE (2, VAR(2), VAR(6), 1)
          ),
          LINE (
            IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), PREDVAR(1, L(VAR(5)))),
            RENAMEBOUNDVARIABLE (4, VAR(3), VAR(5), 1)
          ),
          LINE (
            IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), PREDVAR(1, L(VAR(5)))),
            RENAMEBOUNDVARIABLE (5, VAR(2), VAR(6), 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(2))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))),
            RENAMEBOUNDVARIABLE (7, VAR(3), VAR(4), 1)
          ),
          LINE (
            IMPL(PREDVAR(1, L(VAR(2))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))),
            RENAMEBOUNDVARIABLE (8, VAR(2), VAR(5), 1)
          ),
          LINE (
            IMPL(PREDVAR(1, L(VAR(2))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))),
            RENAMEBOUNDVARIABLE (10, VAR(3), VAR(4), 1)
          ),
          LINE (
            IMPL(PREDVAR(1, L(VAR(2))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1))))),
            RENAMEBOUNDVARIABLE (11, VAR(2), VAR(5), 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(FORALL(VAR(2), PREDVAR(1, L(VAR(1), VAR(2)))), EXISTS(VAR(3), PREDVAR(1, L(VAR(3), VAR(4))))),
            HYPOTHETICALSYLLOGISM (6, 12)
          ),
          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 (13, 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 (14, VAR(4))
          ),
          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)))))),
            RENAMEBOUNDVARIABLE (15, VAR(8), VAR(9), 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)))))),
            RENAMEBOUNDVARIABLE (16, VAR(7), VAR(10), 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)))))),
            RENAMEBOUNDVARIABLE (17, VAR(6), VAR(11), 2)
          ),
          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)))))),
            RENAMEBOUNDVARIABLE (18, VAR(5), VAR(12), 2)
          ),
          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)))))),
            RENAMEBOUNDVARIABLE (20, VAR(8), VAR(9), 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)))))),
            RENAMEBOUNDVARIABLE (21, VAR(7), VAR(10), 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)))))),
            RENAMEBOUNDVARIABLE (22, VAR(6), VAR(11), 2)
          ),
          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)))))),
            RENAMEBOUNDVARIABLE (23, VAR(5), VAR(12), 2)
          )
        )
      )
    )
  )
)