Hilbert-style deduction systems are characterized by the use of numerous schemes of logical axioms. An axiom scheme is an infinite set of axioms obtained by substituting all formulas of some form into a specific pattern. The set of logical axioms includes not only those axioms generated from this pattern, but also any generalization of one of those axioms. A generalization of a formula is obtained by prefixing zero or more universal quantifiers on the formula; for example is a generalization of .
Logical axioms
There are several variant axiomatisations of predicate logic, since for any logic there is freedom in choosing axioms and rules that characterise that logic. We describe here a Hilbert system with nine axioms and just the rule modus ponens, which we call the one-rule axiomatisation and which describes classical equational logic. We deal with a minimal language for this logic, where formulas use only the connectives and and only the quantifier . Later we show how the system can be extended to include additional logical connectives, such as and , without enlarging the class of deducible formulas.
The first four logical axiom schemes allow (together with modus ponens) for the manipulation of logical connectives.
- P1.
- P2.
- P3.
- P4.
The axiom P1 is redundant, as it follows from P3, P2 and modus ponens (see proof). These axioms describe classical propositional logic; without axiom P4 we get positive implicational logic. Minimal logic is achieved either by adding instead the axiom P4m, or by defining as .
- P4m.
Intuitionistic logic is achieved by adding axioms P4i and P5i to positive implicational logic, or by adding axiom P5i to minimal logic. Both P4i and P5i are theorems of classical propositional logic.
- P4i.
- P5i.
Note that these are axiom schemes, which represent infinitely many specific instances of axioms. For example, P1 might represent the particular axiom instance , or it might represent : the is a place where any formula can be placed. A variable such as this that ranges over formulae is called a 'schematic variable'.
With a second rule of uniform substitution (US), we can change each of these axiom schemes into a single axiom, replacing each schematic variable by some propositional variable that isn't mentioned in any axiom to get what we call the substitutional axiomatisation. Both formalisations have variables, but where the one-rule axiomatisation has schematic variables that are outside the logic's language, the substitutional axiomatisation uses propositional variables that do the same work by expressing the idea of a variable ranging over formulae with a rule that uses substitution.
- US. Let be a formula with one or more instances of the propositional variable , and let be another formula. Then from , infer .[dubious – discuss]
The next three logical axiom schemes provide ways to add, manipulate, and remove universal quantifiers.
- Q5. where t may be substituted for x in
- Q6.
- Q7. where x is not free in .
These three additional rules extend the propositional system to axiomatise classical predicate logic. Likewise, these three rules extend system for intuitionstic propositional logic (with P1-3 and P4i and P5i) to intuitionistic predicate logic.
Universal quantification is often given an alternative axiomatisation using an extra rule of generalisation (see the section on Metatheorems), in which case the rules Q6 and Q7 are redundant.[dubious – discuss]
The final axiom schemes are required to work with formulas involving the equality symbol.
- I8. for every variable x.
- I9.