MODULE (
  HEADER (
    SPEC (
      NAME ("predaxiom"),
      VERSION ("1.00.00"),
      VERSION ("1.00.00"),
      LOCATIONS (
        LOCATION ("http://www.qedeq.org/0_00_53")
      )
    ),
    HEADLINE ("Axioms of Predicate Calculus"),
    DESCRIPTION (
      "This module contains the axioms of predicate calculus. The following quantification axioms and these of \href{propaxiom_1.00.00_1.00.00.html}{propositional calculus} (or \href{propaxiom_1.00.00_1.00.00.o.html}{propositional calculus}) (together with some rules) allow the deduction of all theorems of predicate calculus. To learn about possible conclusions click through the following `.. used by..' list. \par This file is part of the project `Hilbert II' see \href{http://www.qedeq.org/}{project homepage}."
    ),
    EMAIL ("module@qedeq.org"),
    AUTHORS (
      AUTHOR ("Michael Meyling",EMAIL ("mime@qedeq.org"))
    )
  ),
  USEDBY (
    SPEC (
      NAME ("predtheo1"),
      VERSION ("1.00.00"),
      VERSION ("1.00.00"),
      LOCATIONS (
        LOCATION ("."),
        LOCATION ("http://www.qedeq.org/0_00_53")
      )
    ),
    SPEC (
      NAME ("predtheo2"),
      VERSION ("1.00.00"),
      VERSION ("1.00.00"),
      LOCATIONS (
        LOCATION ("."),
        LOCATION ("http://www.qedeq.org/0_00_53")
      )
    ),
    SPEC (
      NAME ("predtheo2"),
      VERSION ("1.00.00"),
      VERSION ("1.02.00"),
      LOCATIONS (
        LOCATION ("."),
        LOCATION ("http://www.qedeq.org/0_00_53")
      )
    )
  ),
  PARAGRAPHS (
    PARAGRAPH (
      LABEL ("axiom5"),
      "Axiom of Specialization:",
      AXIOM (
        IMPL(FORALL(VAR(1), PREDVAR(1, L(VAR(1)))), PREDVAR(1, L(VAR(2))))
      )
    ),
    PARAGRAPH (
      LABEL ("axiom6"),
      AXIOM (
        IMPL(PREDVAR(1, L(VAR(2))), EXISTS(VAR(1), PREDVAR(1, L(VAR(1)))))
      )
    ),
    PARAGRAPH (
      LABEL ("predrule1"),
      DECLARERULE (
        "RENAMEBOUNDVARIABLE", 
        "Rename Bound Variable"
      ),
      "For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#renameboundvar}{rename bound variable} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#renameboundvar}{rename bound variable (o)}"
    ),
    PARAGRAPH (
      LABEL ("predrule2"),
      DECLARERULE (
        "RENAMEFREEVARIABLE", 
        "Rename Free Variable"
      ),
      "For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#renamefreevar}{rename free variable} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#renamefreevar}{rename free variable (o)}"
    ),
    PARAGRAPH (
      LABEL ("predrule3"),
      DECLARERULE (
        "REPLACEPREDICATE", 
        "Particularize"
      ),
      "For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#replacepredicate}{rename predicate variable} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#replacepredicate}{rename predicate variable (o)}"
    ),
    PARAGRAPH (
      LABEL ("predrule4"),
      DECLARERULE (
        "PARTICULARIZATION", 
        "Particularize"
      ),
      "For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#particularization}{particularization} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#particularization}{particularization (o)}"
    ),
    PARAGRAPH (
      LABEL ("predrule5"),
      DECLARERULE (
        "GENERALIZATION", 
        "Generalize"
      ),
      "For an explanation see \href{http://www.qedeq.org/0_00_53/rules_1.00.00.html#generalization}{generalization} or \href{http://www.qedeq.org/0_00_53/rules_1.00.00.o.html#generalization}{generalization (o)}"
    )
  )
)