for questions or link request: module admin

Axioms of Predicate Calculus

name: predaxiom, module version: 1.00.00, rule version: 1.00.00, original: 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 (or 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 `Hilbert II' see project homepage.

Content

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 or rename bound variable (o)


4. Rule Declaration
      Rename Free Variable     (predrule2)

For an explanation see rename free variable or rename free variable (o)


5. Rule Declaration
      Particularize     (predrule3)

For an explanation see rename predicate variable or rename predicate variable (o)


6. Rule Declaration
      Particularize     (predrule4)

For an explanation see particularization or particularization (o)


7. Rule Declaration
      Generalize     (predrule5)

For an explanation see generalization or generalization (o)

Cross References

This document is used by the following documents: