MODULE (
  HEADER (
    SPEC (
      NAME ("predaxiom"),
      VERSION ("1.00.00"),
      VERSION ("1.00.00"),
      LOCATIONS (
        LOCATION (".")
      )
    ),
    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} (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 `Principia Mathematica II' see \href{http://www.meyling.com/principia/principia.html}{project homepage}."
    ),
    EMAIL ("principa@meyling.com"),
    AUTHORS (
      AUTHOR ("Michael Meyling",EMAIL ("michael@meyling.com"))
    )
  ),
  USEDBY (
    SPEC (
        NAME ("predtheo1"),
      VERSION ("1.00.00"),
      VERSION ("1.00.00"),
      LOCATIONS (
        LOCATION (".")
      )
    ),
    SPEC (
        NAME ("predtheo2"),
      VERSION ("1.00.00"),
      VERSION ("1.00.00"),
      LOCATIONS (
        LOCATION (".")
      )
    ),
    SPEC (
        NAME ("predtheo2"),
      VERSION ("1.00.00"),
      VERSION ("1.02.00"),
      LOCATIONS (
        LOCATION (".")
      )
    )
  ),
  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{rules_1.00.00.html#renameboundvariable}{rename bound variable}"
    ),
    PARAGRAPH (
      LABEL ("predrule2"),
      DECLARERULE (
        "RENAMEFREEVARIABLE", 
        "Rename Free Variable"
      ),
      "For an explanation see \href{rules_1.00.00.html#renamefreevariable}{rename free variable}"
    ),
    PARAGRAPH (
      LABEL ("predrule3"),
      DECLARERULE (
        "REPLACEPREDICATE", 
        "Particularize"
      ),
      "For an explanation see \href{rules_1.00.00.html#replacepredicate}{rename predicate variable}"
    ),
    PARAGRAPH (
      LABEL ("predrule4"),
      DECLARERULE (
        "PARTICULARIZATION", 
        "Particularize"
      ),
      "For an explanation see \href{rules_1.00.00.html#particularization}{particularization}"
    ),
    PARAGRAPH (
      LABEL ("predrule5"),
      DECLARERULE (
        "GENERALIZATION", 
        "Generalize"
      ),
      "For an explanation see \href{rules_1.00.00.html#generalization}{generalization}"
    )
  )
)