Editing Intuitionistic logic (section)

=== Hilbert-style calculus ===
Intuitionistic logic can be defined using the following [[Hilbert-style deduction system|Hilbert-style calculus]]. This is similar to a way of axiomatizing classical [[propositional logic]].{{sfn|Bezhanishvili|De Jongh|page=8}}

In propositional logic, the inference rule is [[modus ponens]]
* MP: from <math>\phi \to \psi</math> and <math>\phi</math> infer <math>\psi</math>
and the axioms are
* THEN-1: <math>\psi \to (\phi \to \psi )</math>
* THEN-2: <math>\big(\chi \to (\phi \to \psi )\big) \to \big((\chi \to \phi) \to (\chi \to \psi )\big)</math>
* AND-1: <math>\phi \land \chi \to \phi </math>
* AND-2: <math>\phi \land \chi \to \chi </math>
* AND-3: <math>\phi \to \big(\chi \to (\phi \land \chi )\big)</math>
* OR-1: <math>\phi \to \phi \lor \chi </math>
* OR-2: <math>\chi \to \phi \lor \chi </math>
* OR-3: <math>(\phi \to \psi ) \to \Big((\chi \to \psi ) \to \big((\phi \lor \chi) \to \psi )\Big)</math>
* FALSE: <math>\bot \to \phi </math>
To make this a system of first-order predicate logic, the [[generalization (logic)|generalization rules]]
* <math>\forall </math>-GEN: from <math>\psi \to \phi </math> infer <math>\psi \to (\forall x \ \phi )</math>, if <math>x</math> is not free in <math>\psi </math>
* <math>\exists </math>-GEN: from <math>\phi \to \psi </math> infer <math>(\exists x \ \phi ) \to \psi </math>, if <math>x</math> is not free in <math>\psi </math>
are added, along with the axioms
* PRED-1: <math>(\forall x \ \phi (x)) \to \phi (t)</math>, if the term <math>t</math> is free for substitution for the variable <math>x</math> in <math>\phi</math> (i.e., if no occurrence of any variable in <math>t</math> becomes bound in <math>\phi (t)</math>)
* PRED-2: <math>\phi (t) \to (\exists x \ \phi (x))</math>, with the same restriction as for PRED-1

==== Negation ====
If one wishes to include a connective <math>\neg</math> for negation rather than consider it an abbreviation for <math>\phi \to \bot </math>, it is enough to add:
* NOT-1': <math>(\phi \to \bot ) \to \neg \phi </math>
* NOT-2': <math>\neg \phi \to (\phi \to \bot )</math>

There are a number of alternatives available if one wishes to omit the connective <math>\bot </math> (false). For example, one may replace the three axioms FALSE, NOT-1', and NOT-2' with the two axioms
* NOT-1: <math>(\phi \to \chi ) \to \big((\phi \to \neg \chi ) \to \neg \phi \big)</math>
* NOT-2: <math>\chi \to (\neg \chi \to \psi)</math>
as at {{section link|Propositional calculus|Axioms}}. Alternatives to NOT-1 are <math>(\phi \to \neg \chi ) \to (\chi \to \neg \phi )</math> or <math>(\phi \to \neg \phi ) \to \neg \phi </math>.

==== Equivalence ====
The connective <math>\leftrightarrow </math> for equivalence may be treated as an abbreviation, with <math>\phi \leftrightarrow \chi </math> standing for <math>(\phi \to \chi ) \land (\chi \to \phi )</math>. Alternatively, one may add the axioms

* IFF-1: <math>(\phi \leftrightarrow \chi ) \to (\phi \to \chi )</math>
* IFF-2: <math>(\phi \leftrightarrow \chi ) \to (\chi \to \phi )</math>
* IFF-3: <math>(\phi \to \chi ) \to ((\chi \to \phi ) \to (\phi \leftrightarrow \chi ))</math>

IFF-1 and IFF-2 can, if desired, be combined into a single axiom <math>(\phi \leftrightarrow \chi ) \to ((\phi \to \chi ) \land (\chi \to \phi ))</math> using conjunction.