View source for Intuitionistic logic

{{Short description|Various systems of symbolic logic}}
'''Intuitionistic logic''', sometimes more generally called '''constructive logic''', refers to systems of [[symbolic logic]] that differ from the systems used for [[classical logic]] by more closely mirroring the notion of [[constructive proof]]. In particular, systems of intuitionistic logic do not assume the [[law of excluded middle]] and [[double negation elimination]], which are fundamental [[inference rules]] in classical logic.

Formalized intuitionistic logic was originally developed by [[Arend Heyting]] to provide a formal basis for [[Luitzen Egbertus Jan Brouwer|L. E. J. Brouwer]]'s programme of [[intuitionism]]. From a [[proof-theoretic]] perspective, Heyting’s calculus is a restriction of classical logic in which the law of excluded middle and double negation elimination have been removed.  Excluded middle and double negation elimination can still be proved for some propositions on a case by case basis, however, but do not hold universally as they do with classical logic. The standard explanation of intuitionistic logic is the [[BHK interpretation]].{{sfn|Van Atten|2022}}

Several systems of semantics for intuitionistic logic have been studied. One of these semantics mirrors classical [[Boolean-valued semantics]] but uses [[Heyting algebra]]s in place of [[Boolean algebra]]s. Another semantics uses [[Kripke semantics|Kripke models]]. These, however, are technical means for studying Heyting’s deductive system rather than formalizations of Brouwer’s original informal semantic intuitions. Semantical systems claiming to capture such intuitions, due to offering meaningful concepts of “constructive truth” (rather than merely validity or provability), are [[Kurt Gödel]]’s [[dialectica interpretation]], [[Stephen Cole Kleene]]’s [[realizability]], Yurii Medvedev’s logic of finite problems,{{sfn|Shehtman|1990}} or [[Giorgi Japaridze]]’s [[computability logic]]. Yet such semantics persistently induce logics properly stronger than Heyting’s logic. Some authors have argued that this might be an indication of inadequacy of Heyting’s calculus itself, deeming the latter incomplete as a constructive logic.{{sfn|Japaridze|2009}}

== Mathematical constructivism ==
In the semantics of classical logic, [[propositional formula]]e are assigned [[truth value]]s from the two-element set <math>\{\top, \bot\}</math> ("true" and "false" respectively), regardless of whether we have direct [[evidence]] for either case. This is referred to as the 'law of excluded middle', because it excludes the possibility of any truth value besides 'true' or 'false'. In contrast, propositional formulae in intuitionistic logic are ''not'' assigned a definite truth value and are ''only'' considered "true" when we have direct evidence, hence ''proof''. We can also say, instead of the propositional formula being "true" due to direct evidence, that it is [[Inhabited set|inhabited]] by a proof in the [[Curry–Howard correspondence|Curry–Howard]] sense. Operations in intuitionistic logic therefore preserve [[Theory of justification|justification]], with respect to evidence and provability, rather than truth-valuation.

Intuitionistic logic is a commonly-used tool in developing approaches to [[Constructivism (mathematics)|constructivism]] in mathematics. The use of constructivist logics in general has been a controversial topic among mathematicians and philosophers (see, for example, the [[Brouwer–Hilbert controversy]]). A common objection to their use is the above-cited lack of two central rules of classical logic, the law of excluded middle and double negation elimination. [[David Hilbert]] considered them to be so important to the practice of mathematics that he wrote:
{{blockquote|1=''Taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists. To prohibit existence statements and the principle of excluded middle is tantamount to relinquishing the science of mathematics altogether.''|2=Hilbert (1927), see {{harvtxt|Van Heijenoort|2002|page=476}}}}
Intuitionistic logic has found practical use in mathematics despite the challenges presented by the inability to utilize these rules. One reason for this is that its restrictions produce proofs that have the [[disjunction and existence properties]], making it also suitable for other forms of [[mathematical constructivism]]. Informally, this means that if there is a constructive proof that an object exists, that constructive proof may be used as an algorithm for generating an example of that object, a principle known as the [[Curry–Howard correspondence]] between proofs and algorithms. One reason that this particular aspect of intuitionistic logic is so valuable is that it enables practitioners to utilize a wide range of computerized tools, known as [[proof assistants]]. These tools assist their users in the generation and verification of large-scale proofs, whose size usually precludes the usual human-based checking that goes into publishing and reviewing a mathematical proof. As such, the use of proof assistants (such as [[Agda (programming language)|Agda]] or [[Coq (software)|Coq]]) is enabling modern mathematicians and logicians to develop and prove extremely complex systems, beyond those that are feasible to create and check solely by hand. One example of a proof that was impossible to satisfactorily verify without formal verification is the famous proof of the [[four color theorem]]. This theorem stumped mathematicians for more than a hundred years, until a proof was developed that ruled out large classes of possible counterexamples, yet still left open enough possibilities that a computer program was needed to finish the proof. That proof was controversial for some time, but, later, it was verified using Coq.

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

==Theorems==
The theorems of the pure logic are the statements provable from the axioms and inference rules. For example, using THEN-1 in THEN-2 reduces it to <math>\big(\chi \to (\phi \to \psi )\big) \to \big(\phi \to (\chi \to \psi )\big)</math>. A formal proof of the latter using the [[Hilbert_system#Some_useful_theorems_and_their_proofs|Hilbert system]] is given on that page. With <math>\bot</math> for <math>\psi</math>, this in turn implies <math>(\chi \to \neg\phi) \to (\phi \to \neg\chi)</math>. In words: "If <math>\chi</math> being the case implies that <math>\phi</math> is absurd, then if <math>\phi</math> does hold, one has that <math>\chi</math> is not the case." Due to the symmetry of the statement, one in fact obtained
:<math>(\chi \to \neg\phi) \leftrightarrow (\phi \to \neg\chi)</math>
When explaining the theorems of intuitionistic logic in terms of classical logic, it can be understood as a weakening thereof: It is more conservative in what it allows a reasoner to infer, while not permitting any new inferences that could not be made under classical logic. Each theorem of intuitionistic logic is a theorem in classical logic, but not conversely. Many [[Tautology (logic)|tautologies]] in classical logic are not theorems in intuitionistic logic{{snd}}in particular, as said above, one of intuitionistic logic's chief aims is to not affirm the law of the excluded middle so as to vitiate the use of non-constructive [[proof by contradiction]], which can be used to furnish existence claims without providing explicit examples of the objects that it proves exist. 

===Double negations===
A double negation  does not affirm the law of the excluded middle ([[Principle of excluded middle|PEM]]); while it is not necessarily the case that PEM is upheld in any context, no counterexample can be given either. Such a counterexample would be an inference (inferring the negation of the law for a certain proposition) disallowed under classical logic and thus PEM is not allowed in a strict weakening like intuitionistic logic. Formally, it is a simple theorem that <math>\big((\psi\lor(\psi\to\varphi))\to\varphi\big) \leftrightarrow \varphi</math> for any two  propositions. By considering any <math>\varphi</math> established to be false this indeed shows that the double negation of the law <math>\neg\neg(\psi\lor\neg\psi)</math> is retained as a tautology already in [[minimal logic]]. This means any <math>\neg(\psi\lor\neg\psi)</math> is established to be inconsistent and the propositional calculus is in turn always compatible with classical logic.

When assuming the law of excluded middle implies a proposition, then by applying contraposition twice and using the double-negated excluded middle, one may prove double-negated variants of various strictly classical tautologies. The situation is more intricate for predicate logic formulas, when some quantified expressions are being negated.

==== Double negation and implication====
Akin to the above, from modus ponens in the form <math>\psi\to((\psi\to\varphi)\to\varphi)</math> follows <math>\psi\to\neg\neg\psi</math>. The relation between them may always be used to obtain new formulas: A weakened premise makes for a strong implication, and vice versa. For example, note that if <math>(\neg\neg \psi) \to \phi</math> holds, then so does <math>\psi \to \phi</math>, but the schema in the other direction would imply the double-negation elimination principle. Propositions for which double-negation elimination is possible are also called '''stable'''. Intuitionistic logic proves stability only for restricted types of propositions. A formula for which excluded middle holds can be proven stable using the [[disjunctive syllogism]], which is discussed more thoroughly below. The converse does however not hold in general, unless the excluded middle statement at hand is stable itself.

An implication <math>\psi \to \neg\phi</math> can be proven to be equivalent to <math>\neg\neg\psi \to \neg\phi</math>, whatever the propositions. As a special case, it follows that propositions of negated form (<math>\psi=\neg\phi</math> here) are stable, i.e. <math>\neg\neg\neg\phi \to \neg\phi</math> is always valid.

In general, <math>\neg\neg \psi \to \phi</math> is stronger than <math>\psi \to \phi</math>, which is stronger than <math>\neg\neg (\psi \to \phi)</math>, which itself implies the three equivalent statements <math>\psi \to (\neg\neg \phi)</math>, <math>(\neg\neg \psi) \to (\neg\neg \phi)</math> and <math>\neg\phi\to\neg\psi</math> . Using the disjunctive syllogism, the previous four are indeed equivalent. This also gives an intuitionistically valid derivation of <math>\neg\neg(\neg\neg\phi\to\phi)</math>, as it is thus equivalent to an [[law of identity|identity]].

When <math>\psi</math> expresses a claim, then its double-negation <math>\neg\neg\psi</math> merely expresses the claim that a refutation of <math>\psi</math> would be inconsistent. Having proven such a mere double-negation also still aids in negating other statements through [[negation introduction]], as then <math>(\phi\to\neg\psi)\to\neg\phi</math>. A double-negated existential statement does not denote existence of an entity with a property, but rather the absurdity of assumed non-existence of any such entity. Also all the principles in the next section involving quantifiers explain use of implications with hypothetical existence as premise.

====Formula translation====
Weakening statements by adding two negations before existential quantifiers (and atoms) is also the core step in the [[Gödel-Gentzen translation|double-negation translation]]. It constitutes an [[embedding]] of classical first-order logic into intuitionistic logic: a first-order formula is provable in classical logic if and only if its Gödel–Gentzen translation is provable intuitionistically. For example, any theorem of classical propositional logic of the form  <math>\psi\to\phi</math> has a proof consisting of an intuitionistic proof of <math>\psi\to\neg\neg\phi</math> followed by one application of double-negation elimination. Intuitionistic logic can thus be seen as a means of extending classical logic with constructive semantics.

===Non-interdefinability of operators===
Already minimal logic easily proves the following theorems, relating [[logical conjunction|conjunction]] resp. [[logical disjunction|disjunction]] to the [[material conditional|implication]] using [[logical negation|negation]]. Firstly,
* <math>(\phi \lor \psi) \to \neg (\neg \phi \land \neg \psi)</math>
In words: "<math>\phi</math> and <math>\psi</math> each imply that it is not the case that both <math>\phi</math> and <math>\psi</math> fail to hold together."

And here the logically negative conclusion <math>\neg (\neg \phi \land \neg \psi)</math> is in fact equivalent to <math>\neg \phi \to \neg \neg \psi</math>. The alternative implied theorem, <math>(\phi \lor \psi) \to (\neg \phi \to \neg \neg \psi)</math>, represents a weakened variant of the disjunctive syllogism.
Secondly,
* <math>(\phi \land \psi) \to \neg (\neg \phi \lor \neg \psi)</math>
In words: "<math>\phi</math> and <math>\psi</math> both together imply that neither <math>\phi</math> nor <math>\psi</math> fail to hold."

And here the logically negative conclusion <math>\neg (\neg \phi \lor \neg \psi)</math> is in fact equivalent to <math>\neg(\phi \to \neg \psi)</math>. A variant of the converse of the implied theorem here does also hold, namely
* <math>(\phi \to \psi) \to \neg (\phi \land \neg\psi)</math>
In words: "<math>\phi</math> implying <math>\psi</math> implies that it is not the case that <math>\phi</math> holds while <math>\psi</math> fails to hold."

And indeed, stronger variants of all of these still do hold - for example the antecedents may be double-negated, as noted, or all <math>\psi</math> may be replaced by <math>\neg\neg\psi</math> on the antecedent sides, as will be discussed.

However, neither of these five implications above can be reversed without immediately implying excluded middle (consider <math>\neg \psi</math> for <math>\phi</math>) resp. double-negation elimination (consider true <math>\phi</math>). Hence, the left hand sides do not constitute a possible definition of the right hand sides.

In contrast, in classical propositional logic it is possible to take one of those three connectives plus negation as primitive and define the other two in terms of it, in this way. Such is done, for example, in [[Jan Łukasiewicz|Łukasiewicz]]'s [[propositional logic#Łukasiewicz's_P2|three axioms of propositional logic]]. 
It is even possible to define all in terms of a [[sole sufficient operator]] such as the [[Peirce arrow]] (NOR) or [[Sheffer stroke]] (NAND). Similarly, in classical first-order logic, one of the quantifiers can be defined in terms of the other and negation.
These are fundamentally consequences of the [[law of bivalence]], which makes all such connectives merely [[Boolean function]]s.
The law of bivalence is not required to hold in intuitionistic logic. As a result, none of the basic connectives can be dispensed with, and the above axioms are all necessary. So most of the classical identities between connectives and quantifiers are only theorems of intuitionistic logic in one direction. Some of the theorems go in both directions, i.e. are equivalences, as subsequently discussed.

====Existential vs. universal quantification====
Firstly, when <math>x</math> is not free in the proposition <math>\varphi</math>, then
:<math>\big(\exists x\, (\phi(x)\to \varphi)\big)\,\,\to\,\,\Big(\big(\forall x \ \phi(x)\big)\to\varphi\Big)</math>
When the [[domain of discourse]] is empty, then by the [[principle of explosion]], an existential statement implies anything. When the domain contains at least one term, then assuming excluded middle for <math>\forall x \, \phi(x)</math>, the inverse of the above implication becomes provably too, meaning the two sides become equivalent. This inverse direction is equivalent to the [[drinker's paradox]] (DP). Moreover, an existential and dual variant of it is given by the [[independence of premise]] principle (IP). Classically, the statement above is moreover equivalent to a more disjunctive form discussed further below. Constructively, existence claims are however generally harder to come by.

If the domain of discourse is not empty and <math>\phi</math> is moreover independent of <math>x</math>, such principles are equivalent to formulas in the propositional calculus. Here, the formula then just expresses the identity <math>(\phi\to\varphi)\to(\phi\to\varphi)</math>. This is the [[currying|curried]] form of [[modus ponens]] <math>((\phi\to\varphi)\land\phi)\to\varphi</math>, which in the special the case with <math>\varphi</math> as a false proposition results in the [[law of non-contradiction]] principle <math>\neg(\phi\land\neg\phi)</math>.

Considering a false proposition <math>\varphi</math> for the original implication results in the important
* <math>(\exists x \ \neg \phi(x)) \to \neg (\forall x \ \phi(x))</math>
In words: "If there exists an entity <math>x</math> that does ''not'' have the property <math>\phi</math>, then the following is ''refuted'': Each entity has the property <math>\phi</math>."

The quantifier formula with negations also immediately follows from the non-contradiction principle derived above, each instance of which itself already follows from the more particular <math>\neg(\neg\neg\phi\land\neg\phi)</math>. To derive a contradiction given <math>\neg\phi</math>, it suffices to establish its negation <math>\neg\neg\phi</math> (as opposed to the stronger <math>\phi</math>) and this makes proving double-negations valuable also. By the same token, the original quantifier formula in fact still holds with <math>\forall x \ \phi(x)</math> weakened to <math>\forall x \big((\phi(x)\to\varphi)\to\varphi\big)</math>. And so, in fact, a stronger theorem holds:
:<math>(\exists x \ \neg \phi(x)) \to \neg (\forall x \, \neg\neg\phi(x))</math>
In words: "If there exists an entity <math>x</math> that does ''not'' have the property <math>\phi</math>, then the following is ''refuted'': For each entity, one is ''not'' able to prove that it does ''not'' have the property <math>\phi</math>".

Secondly,
:<math>\big(\forall x \, (\phi(x)\to \varphi)\big)\,\,\leftrightarrow\,\,\big((\exists x \ \phi(x))\to\varphi\big)</math>
where similar considerations apply. Here the existential part is always a hypothesis and this is an equivalence. Considering the special case again,
* <math>(\forall x \ \neg \phi(x)) \leftrightarrow \neg (\exists x \ \phi(x))</math>
The proven conversion <math>(\chi\to\neg \phi)\leftrightarrow(\phi\to\neg \chi)</math> can be used to obtain two further implications:
:<math>(\forall x \ \phi(x)) \to \neg (\exists x \ \neg \phi(x))</math>
:<math>(\exists x \ \phi(x)) \to \neg (\forall x \ \neg \phi(x))</math>
Of course, variants of such formulas can also be derived that have the double-negations in the antecedent.
A special case of the first formula here is <math>(\forall x \, \neg\phi(x)) \to \neg (\exists x \, \neg \neg \phi(x))</math> and this is indeed stronger than the <math>\to</math>-direction of the equivalence bullet point listed above. For simplicity of the discussion here and below, the formulas are generally presented in weakened forms without all possible insertions of double-negations in the antecedents.

More general variants hold. Incorporating the predicate <math>\psi</math> and currying, the following generalization also entails the relation between implication and conjunction in the predicate calculus, discussed below.
:<math>\big(\forall x \ \phi(x)\to (\psi(x)\to\varphi)\big)\,\,\leftrightarrow\,\,\Big(\big(\exists x \ \phi(x)\land \psi(x)\big)\to\varphi\Big)</math>
If the predicate <math>\psi</math> is decidedly false for all <math>x</math>, then this equivalence is trivial. If <math>\psi</math> is decidedly true for all <math>x</math>, the schema simply reduces to the previously stated equivalence. In the language of [[Constructive_set_theory#Classes|classes]], <math>A=\{x\mid\phi(x)\}</math> and <math>B=\{x\mid\psi(x)\}</math>, the special case of this equivalence with false <math>\varphi</math> equates two characterizations of [[Disjoint sets|disjointness]] <math>A\cap B=\emptyset</math>:
:<math>\forall(x\in A).x\notin B\,\,\leftrightarrow\,\,\neg\exists(x\in A).x\in B</math>

====Disjunction vs. conjunction====
There are finite variations of the quantifier formulas, with just two propositions:
* <math>(\neg \phi \lor \neg \psi) \to \neg (\phi \land \psi)</math>
* <math>(\neg \phi \land \neg \psi) \leftrightarrow \neg (\phi \lor \psi)</math>
The first principle cannot be reversed: Considering <math>\neg \psi</math> for <math>\phi</math> would imply the weak excluded middle, i.e. the statement <math>\neg \psi \lor \neg \neg \psi</math>. But intuitionistic logic alone does not even prove <math>\neg \psi \lor \neg \neg \psi\lor (\neg \neg \psi\to \psi)</math>. So in particular, there is no distributivity principle for negations deriving the claim <math>\neg \phi \lor \neg \psi</math> from <math>\neg(\phi \land \psi)</math>. For an informal example of the constructive reading, consider the following: From conclusive evidence it not to be the case that ''both'' Alice and Bob showed up to their date, one cannot derive conclusive evidence, ''tied to either'' of the two persons, that this person did not show up. Negated propositions are comparably weak, in that the classically valid [[De_Morgan%27s_laws#In_intuitionistic_logic|De Morgan's law]], granting a disjunction from a single negative hypothetical, does not automatically hold constructively. The intuitionistic propositional calculus and some of its extensions exhibit the [[disjunction property]] instead, implying one of the disjuncts of any disjunction individually would have to be derivable as well.

The converse variants of those two, and the equivalent variants with double-negated antecedents, had already been mentioned above. Implications towards the negation of a conjunction can often be proven directly from the non-contradiction principle. In this way one may also obtain the mixed form of the implications, e.g. <math>(\neg \phi \lor \psi) \to \neg (\phi \land \neg \psi)</math>. Concatenating the theorems, we also find
* <math>(\neg \neg \phi \lor \neg \neg \psi) \to \neg \neg (\phi \lor \psi)</math>
The reverse cannot be provable, as it would prove weak excluded middle.

In predicate logic, the constant domain principle is not valid: <math>\forall x \big(\varphi \lor \psi(x)\big)</math> does not imply the stronger <math>\varphi\lor \forall x\,\psi(x)</math>. The [[Distributive_property#Propositional_logic|distributive properties]] does however hold for any finite number of propositions. For a variant of the De Morgan law concerning two existentially closed [[Decidability (logic)|decidable]] predicates, see [[Limited principle of omniscience|LLPO]].

====Conjunction vs. implication====
From the general equivalence also follows [[Import–export (logic)|import-export]], expressing incompatibility of two predicates using two different connectives:
* <math>(\phi \to \neg \psi) \leftrightarrow \neg (\phi \land \psi)</math>
Due to the symmetry of the conjunction connective, this again implies the already established <math>(\phi \to \neg \psi) \leftrightarrow (\psi \to \neg \phi) </math>.
The equivalence formula for the negated conjunction may be understood as a special case of currying and uncurrying. Many more considerations regarding double-negations again apply. And both non-reversible theorems relating conjunction and implication mentioned in the introduction to non-interdefinability above follow from this equivalence. One is a simply proven variant of a converse, while <math>(\phi \to \psi) \to \neg (\phi \land \neg\psi)</math> holds simply because <math>\phi \to \psi</math> is stronger than <math>\phi \to \neg\neg\psi</math>.

Now when using the principle in the next section, the following variant of the latter, with more negations on the left, also holds:
* <math>\neg (\phi \to \psi) \leftrightarrow (\neg \neg \phi \land \neg \psi) </math>
A consequence is that
* <math>\neg \neg (\phi \land \psi) \leftrightarrow (\neg \neg \phi \land \neg \neg \psi) </math>

====Disjunction vs. implication====
Already minimal logic proves excluded middle equivalent to [[consequentia mirabilis]], an instance of [[Peirce's law]]. 
Now akin to modus ponens, clearly <math>(\phi \lor \psi)\to((\phi\to\psi)\to \psi)</math> already in minimal logic, which is a theorem that does not even involve negations. In classical logic, this implication is in fact an equivalence. With taking <math>\phi</math> to be of the form <math>\psi\to\varphi</math>, excluded middle together with explosion is seen to entail Peirce's law.

In intuitionistic logic, one obtains variants of the stated theorem involving <math>\bot</math>, as follows. Firstly, note that two different formulas for <math>\neg (\phi \land \psi)</math> mentioned above can be used to imply <math>(\neg \phi \vee \neg \psi) \to (\phi \to \neg \psi)</math>. It also followed from direct case-analysis, as do variants where the negations are moved around, such as the theorems <math>(\neg \phi \lor \psi) \to (\phi \to \neg \neg \psi)</math> or <math>(\phi \lor \psi) \to (\neg \phi \to \neg \neg \psi)</math>, the latter being mentioned in the introduction to non-interdefinability. These are forms of the disjunctive [[syllogism]] involving negated propositions <math>\neg\psi</math>. Strengthened forms still holds in intuitionistic logic, say
* <math>(\neg \phi \lor \psi) \to (\phi \to \psi)</math>
The implication cannot generally be reversed, as that would immediately imply excluded middle. So, intuitionistically, "Either <math>P</math> or <math>Q</math>" is generally also a stronger propositional formula than "If not <math>P</math>, then <math>Q</math>", whereas in classical logic these are interchangeable.

Non-contradiction and explosion together actually also prove the stronger variant <math>(\neg \phi \lor \psi) \to (\neg\neg\phi \to \psi)</math>. And this shows how excluded middle for <math>\psi</math> implies double-negation elimination for it. For a fixed <math>\psi</math>, this implication also cannot generally be reversed. However, as <math>\neg\neg(\psi\lor\neg \psi)</math> is always constructively valid, it follows that assuming double-negation elimination for all such disjunctions implies classical logic also.

Of course the formulas established here may be combined to obtain yet more variations. For example, the disjunctive syllogism as presented generalizes to
:<math>\Big(\big(\exists x \ \neg\phi(x)\big)\lor\varphi\Big)\,\,\to\,\,\Big(\big(\forall x \ \phi(x)\big)\to\varphi\Big)</math>
If some term exists at all, the antecedent here even implies <math>\exists x \big(\phi(x)\to\varphi\big)</math>, which in turn itself also implies the conclusion here (this is again the very first formula mentioned in this section).

The bulk of the discussion in these sections applies just as well to just minimal logic. But as for the disjunctive syllogism with general <math>\psi</math>, minimal logic can at most prove <math>(\neg\phi \lor \psi) \to (\neg\neg \phi \to \psi')</math> where <math>\psi'</math> denotes <math>\neg\neg\psi\land(\psi\lor\neg\psi)</math>. The conclusion here can only be simplified to <math>\psi</math> using explosion.

====Equivalences====
The above lists also contain equivalences.
The equivalence involving a conjunction and a disjunction stems from <math>(P\lor Q)\to R</math> actually being stronger than <math>P\to R</math>. Both sides of the equivalence can be understood as conjunctions of independent implications. Above, absurdity <math>\bot</math> is used for <math>R</math>. In functional interpretations, it corresponds to [[Conditional (computer programming)|if-clause]] constructions.
So e.g. "Not (<math>P</math> or <math>Q</math>)" is equivalent to "Not <math>P</math>, and also not <math>Q</math>".

An equivalence itself is generally defined as, and then equivalent to, a conjunction (<math>\land</math>) of implications (<math>\to</math>), as follows:
* <math>(\phi\leftrightarrow \psi) \leftrightarrow \big((\phi \to \psi)\land(\psi\to\phi)\big)</math>
With it, such connectives become in turn definable from it:
* <math>(\phi\to\psi) \leftrightarrow ((\phi\lor\psi) \leftrightarrow \psi)</math>
* <math>(\phi\to\psi) \leftrightarrow ((\phi\land\psi) \leftrightarrow \phi)</math>
* <math>(\phi\land\psi) \leftrightarrow ((\phi\to\psi)\leftrightarrow\phi)</math>
* <math>(\phi\land\psi) \leftrightarrow (((\phi\lor\psi)\leftrightarrow\psi)\leftrightarrow\phi)</math>

In turn, <math>\{\lor, \leftrightarrow, \bot\}</math> and <math>\{\land, \leftrightarrow, \neg\}</math> are complete bases of intuitionistic connectives, for example.

====Functionally complete connectives====
As shown by [[Alexander Kuznetsov (mathematician)|Alexander V. Kuznetsov]], either of the following connectives – the first one ternary, the second one quinary – is by itself [[functionally complete]]: either one can serve the role of a sole sufficient operator for intuitionistic propositional logic, thus forming an analog of the [[Sheffer stroke]] from classical propositional logic:{{sfn|Chagrov|Zakharyaschev|1997|pages=58-59}}
* <math>\big((P\lor Q)\land\neg R\big)\lor\big(\neg P\land(Q\leftrightarrow R)\big)</math>
* <math>P\to\big(Q\land\neg R\land(S\lor T)\big)</math>

==Semantics==
The semantics are rather more complicated than for the classical case. A [[model theory]] can be given by [[Heyting algebra|Heyting algebras]] or, equivalently, by [[Kripke semantics]]. In 2014, a [[Semantic theory of truth|Tarski-like model theory]] was proved complete by [[Robert Lee Constable|Bob Constable]], but with a different notion of completeness than classically.{{sfn|Constable|Bickford|2014}}

Unproved statements in intuitionistic logic are not given a intermediate or third truth value (as is sometimes mistakenly asserted). One can prove that such statements have no third truth value, a result dating back to [[Valery Glivenko|Glivenko]] in 1928.{{sfn|Van Atten|2022}} Instead they remain of unknown truth value, until they are either proved or disproved. Statements are disproved by deducing a contradiction from them.

A consequence of this point of view is that intuitionistic logic has no interpretation as a two-valued logic, nor even as a finite-valued logic, in the familiar sense. Although intuitionistic logic retains the trivial propositions <math>\{\top, \bot\}</math> from classical logic, each ''proof'' of a propositional formula is considered a valid propositional value, thus by [[Brouwer-Heyting-Kolmogorov|Heyting's]] notion of propositions-as-sets, propositional formulae are (potentially non-finite) sets of their proofs.

===Heyting algebra semantics===
In classical logic, we often discuss the [[truth value]]s that a formula can take. The values are usually chosen as the members of a [[Boolean algebra (structure)|Boolean algebra]].  The [[Join and meet|meet and join]] operations in the Boolean algebra are identified with the ∧ and ∨ logical connectives, so that the value of a formula of the form ''A'' ∧ ''B'' is the meet of the value of ''A'' and the value of ''B'' in the Boolean algebra.  Then we have the useful theorem that a formula is a valid proposition of classical logic if and only if its value is 1 for every [[valuation (logic)|valuation]]—that is, for any assignment of values to its variables.

A corresponding theorem is true for intuitionistic logic, but instead of assigning each formula a value from  a Boolean algebra, one uses values from a [[Heyting algebra]], of which Boolean algebras are a special case. A formula is valid in intuitionistic logic if and only if it receives the value of the top element for any valuation on any Heyting algebra.

It can be shown that to recognize valid formulas, it is sufficient to consider a single Heyting algebra whose elements are the open subsets of the real line '''R'''.{{sfn|Sørensen|Urzyczyn|2006|page=42}} In this algebra we have:

:<math>\begin{align}
\text{Value}[\bot] &=\emptyset \\
\text{Value}[\top] &= \mathbf{R} \\
\text{Value}[A \land B] &= \text{Value}[A] \cap \text{Value}[B] \\
\text{Value}[A \lor B]  &= \text{Value}[A] \cup \text{Value}[B] \\
\text{Value}[A \to B] &= \text{int} \left ( \text{Value}[A]^\complement \cup \text{Value}[B] \right )
\end{align}</math>

where int(''X'') is the [[interior (topology)|interior]] of ''X'' and  ''X''<sup>∁</sup> its [[complement (set theory)|complement]].

The last identity concerning ''A'' → ''B'' allows us to calculate the value of ¬''A'':

:<math>\begin{align}
\text{Value}[\neg A] &= \text{Value}[A \to \bot] \\
&=  \text{int} \left ( \text{Value}[A]^\complement \cup \text{Value}[\bot] \right ) \\
&= \text{int} \left ( \text{Value}[A]^\complement \cup \emptyset \right ) \\
&=  \text{int} \left ( \text{Value}[A]^\complement \right )
\end{align}</math>

With these assignments, intuitionistically valid formulas are precisely those that are assigned the value of the entire line.{{sfn|Sørensen|Urzyczyn|2006|page=42}} For example, the formula ¬(''A'' ∧ ¬''A'') is valid, because no matter what set ''X'' is chosen as the value of the formula ''A'', the value of ¬(''A'' ∧ ¬''A'') can be shown to be the entire line:

:<math>\begin{align}
\text{Value}[\neg(A \land \neg A)] &= \text{int} \left ( \text{Value} [A \land \neg A]^\complement   \right )  && \text{Value}[\neg B] = \text{int}\left ( \text{Value}[B]^\complement \right) \\
&= \text{int} \left ( \left (\text{Value}[A] \cap \text{Value}[\neg A] \right )^\complement \right )\\
&= \text{int} \left ( \left (\text{Value}[A]  \cap \text{int} \left (\text{Value}[A]^\complement \right ) \right )^\complement \right )  \\
&= \text{int} \left ( \left (X  \cap \text{int} \left (X^\complement \right ) \right )^\complement \right ) \\
&= \text{int} \left (\emptyset^\complement \right ) && \text{int} \left (X^\complement \right ) \subseteq X^\complement \\
&= \text{int} (\mathbf{R}) \\
&= \mathbf{R}
\end{align}</math>

So the valuation of this formula is true, and indeed the formula is valid. But the law of the excluded middle, ''A'' ∨ ¬''A'', can be shown to be ''invalid'' by using a specific value of the set of positive real numbers for ''A'':

:<math>\begin{align}
\text{Value}[A \lor \neg A] &=  \text{Value}[A] \cup \text{Value}[\neg A] \\
&=  \text{Value}[A] \cup \text{int} \left (  \text{Value}[A]^\complement \right) && \text{Value}[\neg B] = \text{int}\left ( \text{Value}[B]^\complement \right) \\
&=  \{ x > 0\} \cup \text{int} \left (  \{x > 0\}^\complement \right ) \\
&= \{ x > 0\} \cup \text{int} \left (  \{x \leqslant 0 \} \right) \\
&= \{ x > 0\} \cup  \{x < 0 \} \\
&=\{ x \neq 0 \} \\
&\neq \mathbf{R}
\end{align}</math>

The [[interpretation (logic)|interpretation]] of any intuitionistically valid formula in the infinite Heyting algebra described above results in the top element, representing true, as the valuation of the formula, regardless of what values from the algebra are assigned to the variables of the formula.{{sfn|Sørensen|Urzyczyn|2006|page=42}} Conversely, for every invalid formula, there is an assignment of values to the variables that yields a valuation that differs from the top element.{{sfn|Tarski|1938}}{{sfn|Rasiowa|Sikorski|1963|pages=385-386}} No finite Heyting algebra has the second of these two properties.{{sfn|Sørensen|Urzyczyn|2006|page=42}}

===Kripke semantics===
{{Main|Kripke semantics}}

Building upon his work on semantics of [[modal logic]], [[Saul Kripke]] created another semantics for intuitionistic logic, known as Kripke semantics or relational semantics.{{sfn|Kripke|1965}}{{sfn|Moschovakis|2022}}{{sfn|Bezhanishvili|De Jongh|page=8}}

===Tarski-like semantics===
It was discovered that Tarski-like semantics for intuitionistic logic were not possible to prove complete. However, [[Robert Lee Constable|Robert Constable]] has shown that a weaker notion of completeness still holds for intuitionistic logic under a Tarski-like model. In this notion of completeness we are concerned not with all of the statements that are true of every model, but with the statements that are true ''in the same way'' in every model. That is, a single proof that the model judges a formula to be true must be valid for every model. In this case, there is not only a proof of completeness, but one that is valid according to intuitionistic logic.{{sfn|Constable|Bickford|2014}}

==Metalogic==
===Admissible rules===
In intuitionistic logic or a fixed theory using the logic, the situation can occur that an implication always hold metatheoretically, but not in the language. For example, in the pure propositional calculus, if <math>(\neg A)\to(B\lor C)</math> is provable, [[independence of premise|then so is]] <math>(\neg A\to B)\lor(\neg A\to C)</math>. Another example is that <math>(A\to B)\to(A\lor C)</math> being provable always also means that so is <math>\big((A\to B)\to A\big)\lor\big((A\to B)\to C\big)</math>. One says the system is closed under these implications as [[admissible rule|rules]] and they may be adopted.

===Theories' features===
Theories over constructive logics can exhibit the [[disjunction property]]. The pure intuitionistic propositional calculus does so as well.

In particular, it means the excluded middle disjunction for an un-rejectable statement <math>A</math> is provable exactly when <math>A</math> is provable.
This also means, for examples, that the excluded middle disjunction for some the excluded middle disjunctions are not provable also.

===Relation to other logics===
==== Paraconsistent logic ====
Intuitionistic logic is related by [[duality (mathematics)|duality]] to a [[paraconsistent logic]] known as ''Brazilian'', ''anti-intuitionistic'' or ''dual-intuitionistic logic''.{{sfn|Aoyama|2004}}

The subsystem of intuitionistic logic with the FALSE (resp. NOT-2) axiom removed is known as [[minimal logic]] and some differences have been elaborated on above.

==== Intermediate logics ====
In 1932, [[Kurt Gödel]] defined a system of logics intermediate between classical and intuitionistic logic. Indeed, any finite Heyting algebra that is not equivalent to a Boolean algebra defines (semantically) an [[intermediate logic]]. On the other hand, validity of formulae in pure intuitionistic logic is not tied to any individual Heyting algebra but relates to any and all Heyting algebras at the same time.

So for example, for a [[Axiom schema|schema]] not involving negations, consider the classically valid <math>(A\to B)\lor(B\to A)</math>. Adopting this over intuitionistic logic gives the intermediate logic called [[Gödel-Dummett logic]].

==== Relation to classical logic ====
The system of classical logic is obtained by adding any one of the following axioms:
* <math>\phi \lor \neg \phi</math> (Law of the excluded middle)
* <math>\neg \neg \phi \to \phi</math> (Double negation elimination)
* <math>(\neg \phi \to \phi) \to \phi</math> ([[Consequentia mirabilis]], see also [[Peirce's law]])

Various reformulations, or formulations as schemata in two variables (e.g. Peirce's law), also exist. One notable one is the (reverse) law of contraposition
* <math>(\neg \phi \to \neg \chi ) \to (\chi \to \phi)</math>
Such are detailed on the [[intermediate logic]]s article.

In general, one may take as the extra axiom any classical tautology that is not valid in the two-element [[Kripke frame]] <math>\circ{\longrightarrow}\circ</math> (in other words, that is not included in [[intermediate logic|Smetanich's logic]]).

==== Many-valued logic ====
[[Kurt Gödel]]'s work involving [[many-valued logic]] showed in 1932 that intuitionistic logic is not a [[finite-valued logic]].{{sfn|Burgess|2014}} (See the section titled [[#Heyting algebra semantics|Heyting algebra semantics]] above for an [[infinite-valued logic]] interpretation of intuitionistic logic.)

==== Modal logic ====
Any formula of the intuitionistic propositional logic (IPC<!-- laking reference to this acronym, i found one usage here https://plato.stanford.edu/entries/logic-intuitionistic/ -->) may be translated into the language of the [[normal modal logic]] [[Kripke semantics#Correspondence and completeness|S4]] as follows:

:<math>\begin{align}
\bot^* &=  \bot \\
A^* &= \Box A && \text{if } A \text{ is prime (a positive literal)} \\
(A \wedge B)^*&= A^* \wedge B^* \\
(A \vee B)^* &=  A^* \vee B^* \\
(A \to B)^*&= \Box \left (A^* \to B^* \right ) \\
(\neg A)^*&= \Box(\neg (A^*)) &&  \neg A := A \to \bot
\end{align}</math>

and it has been demonstrated that the translated formula is valid in the propositional modal logic S4 if and only if the original formula is valid in IPC.{{sfn|Lévy|2011|pages=4-5}} The above set of formulae are called the [[Modal companion|Gödel–McKinsey–Tarski translation]].
There is also an intuitionistic version of modal logic S4 called Constructive Modal Logic CS4.{{sfn|Alechina|Mendler|De Paiva|Ritter|2003}}

===Lambda calculus===
There is an extended [[Curry–Howard isomorphism]] between IPC and [[simply-typed lambda calculus]].{{sfn|Alechina|Mendler|De Paiva|Ritter|2003}}

==See also==
{{cols}}
* [[BHK interpretation]]
* [[Computability logic]]
* [[Constructive analysis]]
* [[Constructive proof]]
* [[Constructive set theory]]
* [[Curry–Howard correspondence]]
* [[Game semantics]]
* [[Harrop formula]]
* [[Heyting arithmetic]]
* [[Inhabited set]]
* [[Intermediate logics]]
* [[Intuitionistic type theory]]
* [[Kripke semantics]]
* [[Linear logic]]
* [[Paraconsistent logic]]
* [[Realizability]]
* [[Relevance theory]]
* [[Smooth infinitesimal analysis]]
{{colend}}
{{Portal|Philosophy}}

==Notes==
{{Reflist}}

==References==
{{refbegin}}

*{{cite conference
|last1=Alechina
|first1=Natasha
|last2=Mendler
|first2=Michael
|last3=De Paiva
|first3=Valeria
|author3-link=Valeria de Paiva
|last4=Ritter
|first4=Eike
|date=January 2003
|title=Categorical and Kripke Semantics for Constructive S4 Modal Logic
|url=http://www.cs.nott.ac.uk/~nza/papers/Alechina++:01a.pdf
|series=[[Lecture Notes in Computer Science]]
|conference=Proceedings of the 15th International Workshop on Computer Science Logic
|doi=10.1007/3-540-44802-0_21
}}
*{{cite journal
|last=Aoyama
|first=Hiroshi
|year=2004
|title= LK, LJ, Dual Intuitionistic Logic, and Quantum Logic
|journal=[[Notre Dame Journal of Formal Logic]]
|volume=45
|issue= 4
|pages= 193–213
|doi=10.1305/ndjfl/1099238445
|doi-access=free
}}
*{{cite web
|url=http://www.cs.le.ac.uk/people/nb118/Publications/ESSLLI'05.pdf
|title=Intuitionistic Logic
|last1= Bezhanishvili 
|first1= Nick
|last2= De Jongh
|first2= Dick
|at=[[University of Amsterdam]] (Institute for Logic, Language and Computation)
}}
*{{Cite journal
|last1= Brunner
|first1= A.B.M.
|author1-link=
|last2= Carnielli
|first2= Walter
|author2-link= Walter Carnielli
|doi= 10.1016/j.jal.2004.07.016
|title= Anti-intuitionism and paraconsistency
|journal= Journal of Applied Logic
|volume= 3
|issue= 1
|date= March 2005
|pages= 161–184
|doi-access= free
}}
*{{cite web
|last=Burgess
|first=John
|date=January 2014
|title=Intuitions of Three Kinds in Gödel's Views on the Continuum
|url=https://www.princeton.edu/~jburgess/Goedel.pdf
|doi=10.1017/CBO9780511756306.002
|doi-broken-date=1 November 2024 <!-- This line generates a script warning. -->
}}
*{{cite book
|last1= Chagrov
|first1= Alexander
|last2= Zakharyaschev
|first2= Michael
|year=1997
|title=Modal Logic
|volume=35
|series=Oxford Logic Guides
|publisher=[[Oxford University Press]]
|pages=XV, 605
|isbn=0-19-853779-4
}}
*{{cite journal
|last1 = Constable 
|first1 = R.
|last2 = Bickford 
|first2 = M. 
|year = 2014
|title = Intuitionistic completeness of first-order logic
|journal = Annals of Pure and Applied Logic
|volume = 165
|pages = 164–198
|doi = 10.1016/j.apal.2013.07.009
|arxiv=1110.1614
|s2cid = 849930
}}
*{{Cite book
|last = Van Dalen
|first = Dirk
|author-link = Dirk van Dalen
|chapter= Intuitionistic Logic
|year = 2001
|title = The Blackwell Guide to Philosophical Logic
|pages = 224–257
|editor-last= Goble
|editor-first= Lou
|publisher = [[Wiley-Blackwell|Blackwell Publishing]]
|location = New York
|isbn = 9780631206934
|doi = 10.1002/9781405164801.ch11
}}
*{{cite book
|last=Van Heijenoort
|first=Jean
|title=From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931
|publisher=[[Harvard University Press]]
|year=2002
|orig-year=1967
|edition=reprinted with corrections
|isbn=9780674324497
|oclc=749638436
}}
*{{Cite book
|last= Heyting
|first= Arend
|author-link= Arend Heyting
|year= 1930
|language= de
|title= Die formalen Regeln der intuitionistischen Logik I, II, III
|series= Sitzungsberichte der preussischen Akademie der Wissenschaften
|pages= 42–56, 57–71, 158–169
|quote= In three parts
}}
*{{cite book
|last=Japaridze
|first=Giorgi
|author-link=Giorgi Japaridze
|date=January 2009
|chapter=In the Beginning was Game Semantics?
|chapter-url=https://link.springer.com/chapter/10.1007%2F978-1-4020-9374-6_11
|title=Games: Unifying Logic, Language and Philosophy
|volume=15
|url=https://www.springer.com/book/9781402093739
|editor1-last=Majer
|editor1-first=O.
|editor2-last=Pietarinen
|editor2-first=A.-V.
|editor3-last=Tulenheimo
|editor3-first=T.
|publisher=[[Springer Publishing|Springer]]
|pages=249–350
|doi=10.1007/978-1-4020-9374-6_11
|arxiv=cs/0507045
|isbn=978-1-4020-9373-9
}}
*{{Cite book
|last= Kripke
|first= Saul A.
|author-link= Saul Kripke
|date= 1965
|chapter= Semantical analysis of intuitionistic logic I
|series= Studies in Logic and the Foundations of Mathematics
|title= Formal Systems and Recursive Functions. Proceedings of the Eighth Logic Colloquium Oxford, July 1963
|chapter-url= https://www.princeton.edu/~hhalvors/restricted/kripke_intuitionism.pdf
|pages= 92–130
|doi= 10.1016/S0049-237X(08)71685-9
|publisher= [[Elsevier|North-Holland Publishing Company]]
|location= Amsterdam
|editor1-last= Crossley
|editor1-first= J.N.
|editor2-last= Dummett
|editor2-first= M.A.E.
|volume=40
|isbn= 9780444534057
}}
*{{Citation
|last=Lévy
|first=Michel
|date=29 April 2011
|title=Logique modale propositionnelle S4 et logique intuitioniste propositionnelle
|url=http://teachinglogic.liglab.fr/INT1/S4Lint.pdf
|language=fr
}}
*{{cite book
|last1=Rasiowa
|first1=Helena 
|last2=Sikorski
|first2=Roman
|year=1963
|title=The Mathematics of Metamathematics
|publisher=Państwowe Wydawn. Naukowe
|location=Warsaw
|series=Monografie matematyczne
|pages=519
}}
*{{cite journal
|last=Shehtman
|first=Valentin
|date=1990
|title=Modal counterparts of Medvedev logic of finite problems are not finitely axiomatizable
|url=https://link.springer.com/article/10.1007/BF00370370 |doi=10.1007/BF00370370
|journal=[[Studia Logica]]
|volume=49
|issue=3
|pages=365–385
}}
*{{Cite book
|last1= Sørensen
|first1= Morten H.
|last2= Urzyczyn
|first2= Paweł
|date= 2006
|title= Lectures on the Curry-Howard Isomorphism
|chapter= chapter 2: Intuitionistic Logic
|series= Studies in Logic and the Foundations of Mathematics
|edition= 1
|isbn= 978-0-444-52077-7
|publisher= [[Elsevier]]
|location= Amsterdam
|volume=149
}}
*{{cite book
|last=Takeuti
|first=Gaisi
|author-link=Gaisi Takeuti
|title=Proof theory
|edition=Second
|publisher=Dover Publications
|location=Mineola, New York
|year=2013
|orig-year=1975
|url=https://books.google.com/books?id=Idl6K-W69NYC
|isbn=978-0-486-49073-1
}}
*{{cite journal
|last=Tarski
|first=Alfred
|date=1938
|title=Der Aussagenkalkül und die Topologie
|url=http://matwbn.icm.edu.pl/tresc.php?wyd=1&tom=31 |doi=10.1007/BF00370370
|journal=[[Fundamenta Mathematicae]]
|volume=31
|pages=103–134
}}
* {{cite web
|last1=Troelstra
|first1=A.S.
|last2=Van Ulsen
|first2= P.
|title=The discovery of E.W. Beth's semantics for intuitionistic logic
|url=https://festschriften.illc.uva.nl/j50/contribs/troelstra/troelstra.pdf
|publisher=Institute for Logic, Language and Computation (ILLC)
|at=Universiteit van Amsterdam
}}
{{refend}}

==External links==
*{{cite SEP
|last=Van Atten
|first=Mark
|date=4 May 2022
|title=The Development of Intuitionistic Logic
|url-id=intuitionistic-logic-development
}}

*{{cite book
|last=McCarty
|first=David Charles
|chapter=Intuitionism in Mathematics
|title=The Oxford Handbook of Philosophy of Mathematics and Logic
|date=2009
|editor1-last=Shapiro
|editor1-first=Stewart
|pages=356–386
|doi=10.1093/oxfordhb/9780195325928.003.0010
|isbn=978-0-19-532592-8
}}

* {{Cite SEP
|last=Moschovakis
|first=Joan
|date=16 December 2022
|title=Intuitionistic Logic
|url-id=logic-intuitionistic
}}

*{{cite web
|publisher=Laboratoire d'Informatique de [[Grenoble]]
|title=Tableaux'method for intuitionistic logic through S4-translation
|url=http://teachinglogic.liglab.fr/INT1/index.php
|quote= tests the intuitionistic validity of propositional formulae
}}

{{Non-classical logic}}

{{Authority control}}

[[Category:Logic in computer science]]
[[Category:Non-classical logic]]
[[Category:Constructivism (mathematics)]]
[[Category:Systems of formal logic]]
[[Category:Intuitionism]]