Intuitionistic logic

Intuitionistic logic can be defined using the following Hilbert-style calculus. This is similar to a way of axiomatizing classical propositional logic.

In propositional logic, the inference rule is modus ponens

• MP: from ${\displaystyle \phi }$ and ${\displaystyle \phi \to \psi }$ infer ${\displaystyle \psi }$

and the axioms are

• THEN-1: ${\displaystyle \phi \to (\chi \to \phi )}$
• THEN-2: ${\displaystyle (\phi \to (\chi \to \psi ))\to ((\phi \to \chi )\to (\phi \to \psi ))}$
• AND-1: ${\displaystyle \phi \land \chi \to \phi }$
• AND-2: ${\displaystyle \phi \land \chi \to \chi }$
• AND-3: ${\displaystyle \phi \to (\chi \to (\phi \land \chi ))}$
• OR-1: ${\displaystyle \phi \to \phi \lor \chi }$
• OR-2: ${\displaystyle \chi \to \phi \lor \chi }$
• OR-3: ${\displaystyle (\phi \to \psi )\to ((\chi \to \psi )\to ((\phi \lor \chi )\to \psi ))}$
• FALSE: ${\displaystyle \bot \to \phi }$

To make this a system of first-order predicate logic, the generalization rules

• ${\displaystyle \forall }$-GEN: from ${\displaystyle \psi \to \phi }$ infer ${\displaystyle \psi \to (\forall x\ \phi )}$, if ${\displaystyle x}$ is not free in ${\displaystyle \psi }$
• ${\displaystyle \exists }$-GEN: from ${\displaystyle \phi \to \psi }$ infer ${\displaystyle (\exists x\ \phi )\to \psi }$, if ${\displaystyle x}$ is not free in ${\displaystyle \psi }$

are added, along with the axioms

• PRED-1: ${\displaystyle (\forall x\ \phi (x))\to \phi (t)}$, if the term ${\displaystyle t}$ is free for substitution for the variable ${\displaystyle x}$ in ${\displaystyle \phi }$ (i.e., if no occurrence of any variable in ${\displaystyle t}$ becomes bound in ${\displaystyle \phi (t)}$)
• PRED-2: ${\displaystyle \phi (t)\to (\exists x\ \phi (x))}$, with the same restriction as for PRED-1

If one wishes to include a connective ${\displaystyle \lnot }$ for negation rather than consider it an abbreviation for ${\displaystyle \phi \to \bot }$, it is enough to add:

• NOT-1': ${\displaystyle (\phi \to \bot )\to \lnot \phi }$
• NOT-2': ${\displaystyle \lnot \phi \to (\phi \to \bot )}$

There are a number of alternatives available if one wishes to omit the connective ${\displaystyle \bot }$ (false). For example, one may replace the three axioms FALSE, NOT-1', and NOT-2' with the two axioms

• NOT-1: ${\displaystyle (\phi \to \chi )\to ((\phi \to \lnot \chi )\to \lnot \phi )}$
• NOT-2: ${\displaystyle \phi \to (\lnot \phi \to \chi )}$

as at Propositional calculus § Axioms. Alternatives to NOT-1 are ${\displaystyle (\phi \to \lnot \chi )\to (\chi \to \lnot \phi )}$ or ${\displaystyle (\phi \to \lnot \phi )\to \lnot \phi }$.

The connective ${\displaystyle \leftrightarrow }$ for equivalence may be treated as an abbreviation, with ${\displaystyle \phi \leftrightarrow \chi }$ standing for ${\displaystyle (\phi \to \chi )\land (\chi \to \phi )}$. Alternatively, one may add the axioms

• IFF-1: ${\displaystyle (\phi \leftrightarrow \chi )\to (\phi \to \chi )}$
• IFF-2: ${\displaystyle (\phi \leftrightarrow \chi )\to (\chi \to \phi )}$
• IFF-3: ${\displaystyle (\phi \to \chi )\to ((\chi \to \phi )\to (\phi \leftrightarrow \chi ))}$

IFF-1 and IFF-2 can, if desired, be combined into a single axiom ${\displaystyle (\phi \leftrightarrow \chi )\to ((\phi \to \chi )\land (\chi \to \phi ))}$ using conjunction.

The system of classical logic is obtained by adding any one of the following axioms:

• ${\displaystyle \phi \lor \lnot \phi }$ (Law of the excluded middle. May also be formulated as ${\displaystyle (\phi \to \chi )\to ((\lnot \phi \to \chi )\to \chi )}$.)
• ${\displaystyle \lnot \lnot \phi \to \phi }$ (Double negation elimination)
• ${\displaystyle ((\phi \to \chi )\to \phi )\to \phi }$ (Peirce's law)
• ${\displaystyle (\lnot \phi \to \lnot \chi )\to (\chi \to \phi )}$ (Law of contraposition)

In general, one may take as the extra axiom any classical tautology that is not valid in the two-element Kripke frame ${\displaystyle \circ {\longrightarrow }\circ }$ (in other words, that is not included in Smetanich's logic).

In 1932, Kurt Gödel defined a system of logics intermediate between classical and intuitionistic logic; Gödel logics are concomitantly known as intermediate logics.

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'[5] is one example.

It does merely "not affirm" the law of the excluded middle because while it is not necessarily the case that the law 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 is not allowed in a strict weakening like intuitionistic logic. Formally, it is a simple theorem that ${\displaystyle {\big (}(\psi \lor (\psi \to \varphi ))\to \varphi {\big )}\to \varphi }$ for any two propositions. By considering any ${\displaystyle \varphi }$ established to be false indeed shows that the double negation of the law ${\displaystyle \neg \neg (\psi \lor \neg \psi )}$ is retained as a tautology already in minimal logic. So the propositional calculus is always compatible with classical logic. When assuming the law 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.

Akin to the above, from modus ponens in the form ${\displaystyle \psi \to ((\psi \to \varphi )\to \varphi )}$ follows ${\displaystyle \psi \to \neg \neg \psi }$. 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 ${\displaystyle (\neg \neg \psi )\to \phi }$ holds, then so does ${\displaystyle \psi \to \phi }$, and even weaker than the latter are the four equivalent statements ${\displaystyle \psi \to (\neg \neg \phi )}$, ${\displaystyle \neg \phi \to \neg \psi }$, ${\displaystyle (\neg \neg \psi )\to (\neg \neg \phi )}$ as well as ${\displaystyle \neg \neg (\psi \to \phi )}$. Propositions for which double-negation elimination is possible are also called stable. Intuitionistic logic proves stability only for restricted types of propositions, such as those of negated form. A formula for which excluded middle holds can be proven stable using the disjunctive syllogism, but the converse does not hold in general, unless the excluded middle statement is stable itself.

When ${\displaystyle \psi }$ expresses a claim, then its double-negation ${\displaystyle \neg \neg \psi }$ merely expresses the claim that a refutation of ${\displaystyle \psi }$ would be inconsistent. Having proven such a mere double-negation also still aids in negating other statements through negation introduction ${\displaystyle (\phi \to \neg \psi )\to \neg \phi }$. 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.

Weakening statements by adding two negations before existential quantifiers (and atoms) is also the core step in the 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. Therefore, intuitionistic logic can be seen as a means of extending classical logic with constructive semantics.

In classical propositional logic, it is possible to take one of conjunction, disjunction, or implication as primitive, and define the other two in terms of it together with negation, such as in Łukasiewicz's three axioms of propositional logic. It is even possible to define all four 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 functions. 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.

Firstly, when ${\displaystyle x}$ is not free in the proposition ${\displaystyle \varphi }$, then

${\displaystyle {\big (}\exists x\,(\phi (x)\to \varphi ){\big )}\,\,\to \,\,{\Big (}{\big (}\forall x\ \phi (x){\big )}\to \varphi {\Big )}}$

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 ${\displaystyle \forall x\,\phi (x)}$, the two sides become equivalent. Indeed, classically they are also equivalent to a disjunctive form discussed further below. Constructively, existence claims are however harder to come by.

If the domain of discourse is not empty and ${\displaystyle \phi }$ is moreover independent of ${\displaystyle x}$, such principles are equivalent to formulas in the propositional calculus. Here, the formula then just expresses the identity ${\displaystyle (\phi \to \varphi )\to (\phi \to \varphi )}$. This is the curried form of modus ponens ${\displaystyle ((\phi \to \varphi )\land \phi )\to \varphi }$, which in the special the case with ${\displaystyle \varphi }$ as a false proposition results in the law of non-contradiction principle ${\displaystyle \neg (\phi \land \neg \phi )}$. Considering a false proposition ${\displaystyle \varphi }$ for the original implication results in the important

• ${\displaystyle (\exists x\ \neg \phi (x))\to \neg (\forall x\ \phi (x))}$

In words: "If there exists an entity ${\displaystyle x}$ that does not have the property ${\displaystyle \phi }$, then the following is refuted: Each entity has the property ${\displaystyle \phi }$."

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 ${\displaystyle \neg (\neg \neg \phi \land \neg \phi )}$. To derive a contradiction given ${\displaystyle \neg \phi }$, it suffices to establish its negation ${\displaystyle \neg \neg \phi }$ (as opposed to the stronger ${\displaystyle \phi }$) and this makes proving double-negations valuable also. By the same token, the original quantifier formula in fact still holds with ${\displaystyle \forall x\ \phi (x)}$ weakened to ${\displaystyle \forall x{\big (}(\phi (x)\to \varphi )\to \varphi {\big )}}$. And so really

${\displaystyle (\exists x\ \neg \phi (x))\to \neg (\forall x\,\neg \neg \phi (x))}$

In words: "If there exists an entity ${\displaystyle x}$ that does not have the property ${\displaystyle \phi }$, then the following is refuted: For each entity, one is not able to prove that it does not have the property ${\displaystyle \phi }$".

Secondly,

${\displaystyle {\big (}\forall x\,(\phi (x)\to \varphi ){\big )}\,\,\leftrightarrow \,\,{\big (}(\exists x\ \phi (x))\to \varphi {\big )}}$

where similar considerations apply. Here the existential part is always a hypothesis and this is an equivalence. Considering the special case again,

• ${\displaystyle (\forall x\ \neg \phi (x))\leftrightarrow \neg (\exists x\ \phi (x))}$

Lastly, by using the axiom THEN-1 once, THEN-2 can be reduced to its special case ${\displaystyle (\phi \to \neg \chi )\leftrightarrow (\chi \to \neg \phi )}$ and this conversion can then be used to obtain two further implications:

• ${\displaystyle (\forall x\ \phi (x))\to \neg (\exists x\ \neg \phi (x))}$
• ${\displaystyle (\exists x\ \phi (x))\to \neg (\forall x\ \neg \phi (x))}$

For simplicity, in the discussion here and below, the formulas are generally presented in weakened forms without double-negations. To name but one, a special case of the first formula here is ${\displaystyle (\forall x\,\neg \phi (x))\to \neg (\exists x\,\neg \neg \phi (x))}$. Note how also this formula indeed immediately implies the ${\displaystyle \to }$-direction of the equivalence bullet point listed above. The double-negations can also be placed in the antecedent.

More complicated variants hold. Incorporating the predicate ${\displaystyle \psi }$ and currying, the following generalization also entails the relation between implication and conjunction in the predicate calculus, discussed below.

${\displaystyle {\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 )}}$

If the predicate ${\displaystyle \psi }$ is decidedly false for all ${\displaystyle x}$, then this equivalence is trivial. If ${\displaystyle \psi }$ is decidedly true for all ${\displaystyle x}$, the schema simply reduces to the previously stated equivalence. In the language of classes, ${\displaystyle A=\{x\mid \phi (x)\}}$ and ${\displaystyle B=\{x\mid \psi (x)\}}$, the special case of this equivalence with false ${\displaystyle \varphi }$ equates two characterizations of disjointness ${\displaystyle A\cap B=\emptyset }$:

${\displaystyle \forall (x\in A).x\notin B\,\,\leftrightarrow \,\,\neg \exists (x\in A).x\in B}$

There are finite variations of the quantifier formulas, with just two propositions:

• ${\displaystyle (\neg \phi \lor \neg \psi )\to \neg (\phi \land \psi )}$
• ${\displaystyle (\neg \phi \land \neg \psi )\leftrightarrow \neg (\phi \lor \psi )}$

And conversely,

• ${\displaystyle (\phi \land \psi )\to \neg (\neg \phi \lor \neg \psi )}$
• ${\displaystyle (\phi \lor \psi )\to \neg (\neg \phi \land \neg \psi )}$

And as mentioned, stronger forms of these formulas hold. For example, ${\displaystyle (\neg \phi \lor \neg \psi )\to \neg (\neg \neg \phi \land \neg \neg \psi )}$. This can easily be derived from the non-contradiction principle, as all of the formulas are about deriving absurd consequences from hypotheticals, and these statements do not have to be placed in a particular order. By the same reasoning, one may obtain the mixed form of the implication and its converse

${\displaystyle (\neg \phi \lor \psi )\to \neg (\phi \land \neg \psi )}$

${\displaystyle (\neg \phi \land \psi )\to \neg (\phi \lor \neg \psi )}$

But in particular, there is no distributivity principle deriving the claim ${\displaystyle \neg \phi \lor \neg \psi }$ from ${\displaystyle \neg (\phi \land \psi )}$. Negated propositions are comparably weak, in that the classically valid De Morgan's law, granting a disjunction from a single negative hypothetical, does not automatically hold constructively. See also the LLPO for a variant concerning two existentially closed decidable predicates. 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. Instead, the intuitionistic propositional calculus and some of its extensions exhibit the disjunction property, implying the disjuncts individually would have to be derivable as well. When the fourth law is adopted, the weak excluded middle, i.e. the statement ${\displaystyle \neg \phi \lor \neg \neg \phi }$ for negated propositions, immediately follows.

From the general equivalence also follows the following special case, expressing incompatibility of two predicates using two different connectives:

• ${\displaystyle (\phi \to \neg \psi )\leftrightarrow \neg (\phi \land \psi )}$

It may be understood as a special case of currying and uncurrying. Many more considerations regarding double-negations again apply. For example, as ${\displaystyle \phi \to \psi }$ is stronger than ${\displaystyle \phi \to \neg \neg \psi }$, from this equivalence the implication ${\displaystyle (\phi \to \psi )\to \neg (\phi \land \neg \psi )}$ follows. However, this cannot generally be reversed, as for true ${\displaystyle \phi }$ the double-negation elimination principle would follow.

Finally, conversely,

• ${\displaystyle (\phi \land \psi )\to \neg (\phi \to \neg \psi )}$

For either of the propositions established to be true, this again reduces to the double-negation principle for the other, and such an implication cannot generally be reversed.

Due to the symmetry of the conjunction connective, the equivalence formula for the negated conjunction again implies the already established ${\displaystyle (\phi \to \neg \psi )\leftrightarrow (\psi \to \neg \phi )}$.

Clearly ${\displaystyle (\phi \lor \psi )\to ((\phi \to \psi )\to \psi )}$ and classically this is an equivalence. Indeed, minimal logic already proves more general variants of this implication. In intuitionistic logic, one obtains variants involving ${\displaystyle \bot }$, as follows.

Firstly, note that two different formulas for ${\displaystyle \neg (\phi \land \psi )}$ mentioned above can be used to imply ${\displaystyle (\neg \phi \vee \neg \psi )\to (\phi \to \neg \psi )}$. The latter are forms of the disjunctive syllogism for negated propositions, ${\displaystyle \neg \psi }$. A strengthened form still holds in intuitionistic logic:

• ${\displaystyle (\neg \phi \lor \psi )\to (\phi \to \psi )}$

As in previous sections, the positions of ${\displaystyle \neg \phi }$ and ${\displaystyle \phi }$ may be switched and ${\displaystyle \phi }$ may be weakened to ${\displaystyle \neg \neg \phi }$. These principles are provable from non-contradiction and explosion. So, for example, intuitionistically "Either ${\displaystyle P}$ or ${\displaystyle Q}$" is a stronger propositional formula than "If not ${\displaystyle P}$, then ${\displaystyle Q}$", whereas these are classically interchangeable. The implication cannot generally be reversed, as that immediatenly implies excluded middle.

Considering ${\displaystyle \neg \neg \psi }$ in place of ${\displaystyle \phi }$ in the above form of the syllogism shows how excluded middle implies double-negation elimination. And in this way intuitionistic logic proves ${\displaystyle \neg \neg (\neg \neg \psi \to \psi )}$.

Of course the formulas established here may be combined to obtain yet more variations. For example, the disjunctive syllogism as presented generalizes to

${\displaystyle {\Big (}{\big (}\exists x\ \neg \phi (x){\big )}\lor \varphi {\Big )}\,\,\to \,\,{\Big (}{\big (}\forall x\ \phi (x){\big )}\to \varphi {\Big )}}$

If some term exists at all, the antecedent here even implies ${\displaystyle \exists x{\big (}\phi (x)\to \varphi {\big )}}$, 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 ${\displaystyle \psi }$, minimal logic can at most prove ${\displaystyle (\neg \phi \lor \psi )\to (\neg \neg \phi \to \psi ')}$ where ${\displaystyle \psi '}$ denotes ${\displaystyle \neg \neg \psi \land (\psi \lor \neg \psi )}$. The conclusion here can only be simplified to ${\displaystyle \psi }$ using explosion.

The above lists also contain equivalences. The equivalence involving a conjunction and a disjunction stems from ${\displaystyle (P\lor Q)\to R}$ actually being stronger than ${\displaystyle P\to R}$. Both sides of the equivalence can be understood as conjunctions of independent implications. Above, absurdity ${\displaystyle \bot }$ is used for ${\displaystyle R}$. In functional interpretations, it corresponds to if-clause constructions. So e.g. "Not (${\displaystyle P}$ or ${\displaystyle Q}$)" is equivalent to "Not ${\displaystyle P}$, and also not ${\displaystyle Q}$".

An equivalence itself is generally defined as, and then equivalent to, a conjunction of implications

• ${\displaystyle (\phi \leftrightarrow \psi )\leftrightarrow {\big (}(\phi \to \psi )\land (\psi \to \phi ){\big )}}$

With it, such connectives become in turn definable from it:

• ${\displaystyle (\phi \to \psi )\leftrightarrow ((\phi \lor \psi )\leftrightarrow \psi )}$
• ${\displaystyle (\phi \to \psi )\leftrightarrow ((\phi \land \psi )\leftrightarrow \phi )}$
• ${\displaystyle (\phi \land \psi )\leftrightarrow ((\phi \to \psi )\leftrightarrow \phi )}$
• ${\displaystyle (\phi \land \psi )\leftrightarrow (((\phi \lor \psi )\leftrightarrow \psi )\leftrightarrow \phi )}$

In turn, ${\displaystyle \{\lor ,\leftrightarrow ,\bot \}}$ and ${\displaystyle \{\land ,\leftrightarrow ,\neg \}}$ are complete bases of intuitionistic connectives.

As shown by 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:[6]

• ${\displaystyle {\big (}(P\lor Q)\land \neg R{\big )}\lor {\big (}\neg P\land (Q\leftrightarrow R){\big )}}$
• ${\displaystyle P\to {\big (}Q\land \neg R\land (S\lor T){\big )}}$

In classical logic, we often discuss the truth values that a formula can take. The values are usually chosen as the members of a Boolean algebra. The 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—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.[8] In this algebra we have:

${\displaystyle {\begin{aligned}{\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{aligned}}}$

where int(X) is the interior of X and X^∁ its complement.

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

${\displaystyle {\begin{aligned}{\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{aligned}}}$

With these assignments, intuitionistically valid formulas are precisely those that are assigned the value of the entire line.[8] 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:

${\displaystyle {\begin{aligned}{\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{aligned}}}$

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:

${\displaystyle {\begin{aligned}{\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{aligned}}}$

The 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.[8] Conversely, for every invalid formula, there is an assignment of values to the variables that yields a valuation that differs from the top element.[9][10] No finite Heyting algebra has the second of these two properties.[8]

Building upon his work on semantics of modal logic, Saul Kripke created another semantics for intuitionistic logic, known as Kripke semantics or relational semantics.[11]

It was discovered that Tarski-like semantics for intuitionistic logic were not possible to prove complete. However, 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.[12]

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 ${\displaystyle (\neg A)\to (B\lor C)}$ is provable, then so is ${\displaystyle (\neg A\to B)\lor (\neg A\to C)}$. Another example is that ${\displaystyle (A\to B)\to (A\lor C)}$ being provable always also means that so is ${\displaystyle {\big (}(A\to B)\to A{\big )}\lor {\big (}(A\to B)\to C{\big )}}$. One says the system is closed under these implications as rules and they may be adopted.

Intuitionistic logic is related by duality to a paraconsistent logic known as Brazilian, anti-intuitionistic or dual-intuitionistic logic.[13] The subsystem of intuitionistic logic with the FALSE axiom removed is known as minimal logic and some differences have been elaborated on above.

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.

Kurt Gödel's work involving many-valued logic showed in 1932 that intuitionistic logic is not a finite-valued logic.[14] (See the section titled Heyting algebra semantics above for an infinite-valued logic interpretation of intuitionistic logic.)

Any formula of the intuitionistic propositional logic (IPC) may be translated into the language of the normal modal logic S4 as follows:

${\displaystyle {\begin{aligned}\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{aligned}}}$

and it has been demonstrated[15] that the translated formula is valid in the propositional modal logic S4 if and only if the original formula is valid in IPC. The above set of formulae are called the Gödel–McKinsey–Tarski translation. There is also an intuitionistic version of modal logic S4 called Constructive Modal Logic CS4.[16]

There is an extended Curry–Howard isomorphism between IPC and simply-typed lambda calculus.[16]