Axiom 2.2.1. Each axioms represents a scheme, where \(\phi, \psi,\) and \(\theta\) are formulas, \(x\) is a variable, and \(t\) and \(u\) are terms.
- \(\phi \rightarrow(\psi \rightarrow \phi).\)
- \((\phi \rightarrow(\psi \rightarrow \theta)) \rightarrow((\phi \rightarrow \psi) \rightarrow(\phi \rightarrow \theta)).\)
- \(((\neg \phi) \rightarrow(\neg \psi)) \rightarrow(\psi \rightarrow \phi).\)
- \((\forall x) \phi \rightarrow \phi[t / x].\)
- \((\forall x)(\phi \rightarrow \psi) \rightarrow(\phi \rightarrow(\forall x) \psi),\) if there is no free occurrence of \(x\) in \(\phi.\)
- \(t=t\) for any term \(t.\)
- \((t=u) \rightarrow(u=t)\) for any terms \(t\) and \(u.\)
- \((t=u) \rightarrow((u=v) \rightarrow(t=v))\) for any terms \(t,u,\) and \(v.\)
- \((t=u) \rightarrow(\phi[t / x] \rightarrow \phi[u / x]) .\)
Rule 2.2.2 (Rules of inference). Let \(\phi\) and \(\psi\) be formulas, and let \(x\) be a variable. Also we let a set of formulas have no formula in which \(x\) is a free variable.
- (Modus Ponens) From \(\phi\) and \(\phi \rightarrow \psi,\) infer \(\psi.\)
- (Generalization) From \(\phi\) infer \((\forall x)\phi.\)
References
- Cameron, P. J. (1998). Sets, logic and categories. Springer. https://doi.org/10.1007/978-1-4471-0589-3