Editing Intuitionistic logic (section)

==Syntax==
[[File:Rieger-Nishimura.svg|thumb|right|280px|The [[Rieger–Nishimura lattice]]. Its nodes are the propositional formulas in one variable up to intuitionistic [[logical equivalence]], ordered by intuitionistic logical implication.]]
The [[syntax]] of formulas of intuitionistic logic is similar to [[propositional logic]] or [[first-order logic]].  However, intuitionistic [[logical connective|connective]]s are not definable in terms of each other in the same way as in [[classical logic]], hence their choice matters. In intuitionistic propositional logic (IPL) it is customary to use →, ∧, ∨, ⊥ as the basic connectives, treating ¬''A'' as an abbreviation for {{nowrap|(''A'' → ⊥)}}. In intuitionistic first-order logic both [[quantifier (logic)|quantifier]]s ∃, ∀ are needed.

=== 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.

===Sequent calculus===
{{Main|Sequent calculus}}
[[Gerhard Gentzen]] discovered that a simple restriction of his system LK (his sequent calculus for classical logic) results in a system that is sound and complete with respect to intuitionistic logic. He called this system LJ. In LK any number of formulas is allowed to appear on the conclusion side of a sequent; in contrast LJ allows at most one formula in this position.

Other derivatives of LK are limited to intuitionistic derivations but still allow multiple conclusions in a sequent.  LJ'{{sfn|Takeuti|2013}} is one example.