There is an unlimited amount of 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 \lnot and \to and only the quantifier \forall. Later we show how the system can be extended to include additional logical connectives, such as \land and \lor, without enlarging the class of deducible formulas. The first four logical axiom schemas allow (together with modus ponens) for the manipulation of logical connectives. :P1. \phi \to \phi :P2. \phi \to \left( \psi \to \phi \right) :P3. \left( \phi \to \left( \psi \rightarrow \xi \right) \right) \to \left( \left( \phi \to \psi \right) \to \left( \phi \to \xi \right) \right) :P4. \left ( \lnot \phi \to \lnot \psi \right) \to \left( \psi \to \phi \right) 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 \lnot \phi as \phi \to \bot. :P4m. \left( \phi \to \psi \right) \to \left(\left(\phi \to \lnot \psi \right) \to \lnot \phi \right)
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. \left(\phi \to \lnot \phi\right) \to \lnot \phi :P5i. \lnot\phi \to \left( \phi \to \psi \right) Note that these are axiom schemas, which represent infinitely many specific instances of axioms. For example, P1 might represent the particular axiom instance p \to p , or it might represent \left( p \to q \right) \to \left( p \to q \right) : the \phi 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 schemas 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 \phi(p) be a formula with one or more instances of the propositional variable p, and let \psi be another formula. Then from \phi(p), infer \phi(\psi). The next three logical axiom schemas provide ways to add, manipulate, and remove universal quantifiers. :Q5. \forall x \left( \phi \right) \to \phi[x:=t] where
t may be substituted for
x in \,\!\phi :Q6. \forall x \left( \phi \to \psi \right) \to \left( \forall x \left( \phi \right) \to \forall x \left( \psi \right) \right) :Q7. \phi \to \forall x \left( \phi \right) where
x is not free in \phi. These three additional rules extend the propositional system to axiomatise
classical predicate logic. Likewise, these three rules extend system for intuitionistic 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, in which case the rules Q6 and Q7 are redundant. •
Generalization: If \Gamma \vdash \phi and
x does not occur free in any formula of \Gamma then \Gamma \vdash \forall x \phi. The final axiom schemas are required to work with formulas involving the equality symbol. :I8. x = x for every variable
x. :I9. \left( x = y \right) \to \left( \phi[z:=x] \to \phi[z:=y] \right) == Conservative extensions ==