Intuitionistic propositional logic (IPL) is the propositional logic obtained after removing classical principles, such as excluded middle.
IPL shares the same syntax as classical propositional logic: its formulas are defined by
As usual, the are propositional variables.
It is possible to give a finite axiomatization of IPL
This axiomatization assumes that .
Basic inference rules:
Conjunction:
Disjunction:
Falsity:
It is clear that this axiomatization is inspired by the universal properties of as greatest lower bound, as least upper bound, and as bottom/initial object.
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:
Conjunction:
Disjunction:
Negation:
There are many kinds of semantics for intuitionistic propositional logic:
[Bezhanishvili and Holliday 2019] argue that there is a strict hierarchy of generality of these semantics:
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].
Deciding whether a formula of IPL is valid (i.e. a theorem) is PSPACE-complete [Statman 1979].
The satisfiability problem for IPL is discussed in this Mathoverflow question.
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.
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},
}
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}
}
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},
}