for questions or link request: module admin

Axioms of Predicate Calculus

name: predaxiom, module version: 1.00.00, rule version: 1.00.00, orignal: predaxiom, author of this module: Michael Meyling

Description

This module contains the axioms of predicate calculus. The following quantification axioms and these of 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.
This file is part of the project `Principia Mathematica II' see project homepage.

Is used by the following modules:


Axiom of Specialization:

1. Axiom
      (" x (R(x)) Þ R(y))     (axiom5)


2. Axiom
      (R(y) Þ $ x (R(x)))     (axiom6)


3. Rule Declaration
      Rename Bound Variable     (predrule1)

For an explanation see rename bound variable


4. Rule Declaration
      Rename Free Variable     (predrule2)

For an explanation see rename free variable


5. Rule Declaration
      Particularize     (predrule3)

For an explanation see rename predicate variable


6. Rule Declaration
      Particularize     (predrule4)

For an explanation see particularization


7. Rule Declaration
      Generalize     (predrule5)

For an explanation see generalization

This module is used by the following modules: