Intuitionistic propositional Logic

Intuitionistic propositional logic (IPL) is the propositional logic obtained after removing classical principles, such as excluded middle.

Syntax

IPL shares the same syntax as classical propositional logic: its formulas are defined by

\phi ::=
   		 p_i	
  \mid \top
  \mid \bot
  \mid \phi_1 \land \phi_2
  \mid \phi_1 \lor \phi_2
  \mid \phi_1 \to \phi_2
  \mid \lnot \phi

As usual, the p_i are propositional variables.

Axiomatizations

It is possible to give a finite axiomatization of IPL

Modern axiomatization

This axiomatization assumes that \lnot \phi \triangleq \phi \to \bot.

Basic inference rules:

\varphi \to (\psi \to \varphi)
(\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi))

Conjunction:

\varphi \land \psi \to \varphi
\varphi \land \psi \to \psi
\varphi \to (\psi \to \varphi \land \psi)

Disjunction:

\varphi \to \varphi \lor \psi
\psi \to \varphi \lor \psi
(\varphi \to \chi) \to ((\psi \to \chi) \to (\varphi \lor \psi \to \chi))

Falsity:

\bot \to \varphi

It is clear that this axiomatization is inspired by the universal properties of \land as greatest lower bound, \lor as least upper bound, and \bot as bottom/initial object.

Heyting's axiomatization

The original axiomatization presented by Heyting 1930 went through the Principia Mathematica axioms and removed the ones that were intuitionistically unacceptable. The remaining ones can be split into four groups.

Basic inference:

(\varphi \to \psi) \land (\psi \to \chi) \to (\varphi \to \chi)
\varphi \to (\psi \to \varphi)
\varphi \land (\varphi \to \psi) \to \psi

Conjunction:

\varphi \to \varphi \land \varphi
\varphi \land \psi \to \psi \land \varphi
(\varphi \to \psi) \to (\chi \land \varphi \to \chi \land \psi)

Disjunction:

\varphi \to \varphi \lor \psi
\varphi \lor \psi \to \psi \lor \varphi
(\varphi \to \chi) \lor (\psi \to \chi) \to (\varphi \lor \psi \to \chi)

Negation:

\lnot \varphi \to (\varphi \to \psi)
(\varphi \to \psi) \land (\varphi \to \lnot \psi) \to \lnot \varphi

Semantics

There are many kinds of semantics for intuitionistic propositional logic:

Kripke semantics
Beth semantics
Topological semantics
Dragalin semantics
Algebraic semantics, through Heyting algebras

Bezhanishvili and Holliday 2019 argue that there is a strict hierarchy of generality of these semantics:

\text{Kripke} < \text{Beth} < \text{Topological} < \text{Dragalin} < \text{Algebraic}

Decision procedures

A decision procedure for IPL was given by Gerhard Gentzen in his doctoral thesis.

That, as well as further developments, are surveyed by Dyckhoff 2016.

Complexity

Validity

Deciding whether a formula of IPL is valid (i.e. a theorem) is PSPACE-complete Statman 1979.

Satisfiability

The satisfiability problem for IPL is discussed in this Mathoverflow question.

References

Intuitionistic propositional logic was introduced by Arend Heyting in 1930:

Heyting, Arend. 1930. ‘Die Formalen Regeln Der Intuitionistischen Logik’. Sitzungsberichte Der Preussischen Akademie Der Wissenschaften 49: 42–65.

@article{heyting_formalen_1930,
	title = {Die formalen Regeln der intuitionistischen Logik},
	volume = {49},
	pages = {42--65},
	journaltitle = {Sitzungsberichte der Preussischen Akademie der Wissenschaften},
	author = {Heyting, Arend},
	date = {1930},
}

An English translation of this paper may be found in

Mancosu, Paolo, ed. 1998. From Brouwer to Hilbert: The Debate on the Foundations of Mathematics in the 1920s. New York: Oxford University Press.

The various semantics of intuitionistic propositional logic are surveyed in

Bezhanishvili, Guram, and Wesley H. Holliday. 2019. ‘A Semantic Hierarchy for Intuitionistic Logic’. Indagationes Mathematicae 30 (3): 403–69. https://doi.org/10.1016/j.indag.2019.01.001. pdf

@article{bezhanishvili_2019,
	title = {A semantic hierarchy for intuitionistic logic},
	volume = {30},
	doi = {10.1016/j.indag.2019.01.001},
	pages = {403--469},
	number = {3},
	journaltitle = {Indagationes Mathematicae},
	author = {Bezhanishvili, Guram and Holliday, Wesley H.},
	date = {2019},
}

A survey of decision procedures for IPL is given in

Dyckhoff, Roy. 2016. ‘Intuitionistic Decision Procedures Since Gentzen’. In Advances in Proof Theory, edited by Reinhard Kahle, Thomas Strahm, and Thomas Studer, 28:245–67. Progress in Computer Science and Applied Logic. Cham: Birkhäuser. https://doi.org/10.1007/978-3-319-29198-7_6. pdf

@incollection{dyckhoff_2016,
	address = {Cham},
	series = {Progress in {Computer} {Science} and {Applied} {Logic}},
	title = {Intuitionistic {Decision} {Procedures} {Since} {Gentzen}},
	volume = {28},
	booktitle = {Advances in {Proof} {Theory}},
	publisher = {Birkhäuser},
	author = {Dyckhoff, Roy},
	editor = {Kahle, Reinhard and Strahm, Thomas and Studer, Thomas},
	year = {2016},
	doi = {10.1007/978-3-319-29198-7_6},
	pages = {245--267}
}

The PSPACE-completeness of the validity problem for IPL was shown in

Statman, Richard. 1979. ‘Intuitionistic Propositional Logic Is Polynomial-Space Complete’. Theoretical Computer Science 9 (1): 67–72. https://doi.org/10.1016/0304-3975(79)90006-9.

@article{statman_1979,
	title = {Intuitionistic propositional logic is polynomial-space complete},
	volume = {9},
	doi = {10.1016/0304-3975(79)90006-9},
	number = {1},
	journal = {Theoretical Computer Science},
	author = {Statman, Richard},
	year = {1979},
	pages = {67--72},
}