Negation

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 }$.

Equivalence

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.

Relation to classical logic

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.

Formula translation

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. For example, any theorem of classical propositional logic of the form ${\displaystyle \psi \to \phi }$ has a proof consisting of an intuitionistic proof of ${\displaystyle \psi \to \neg \neg \phi }$ followed by one application of double-negation elimination. Intuitionistic logic can thus be seen as a means of extending classical logic with constructive semantics.

Existential vs. universal quantification

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

Disjunction vs. conjunction

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 for negations 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. 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. 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. 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. Intuitionistic logic alone, however, does not even prove ${\displaystyle \neg \phi \lor \neg \neg \phi \lor (\neg \neg \phi \to \phi )}$.

In predicate logic, ${\displaystyle \forall x{\big (}\varphi \lor \psi (x){\big )}}$ does not imply the stronger ${\displaystyle \varphi \lor \forall x\,\psi (x)}$, albeit the distributive properties hold for any finite number of propositions. For a variant of the De Morgan law concerning two existentially closed decidable predicates, see LLPO.

Conjunction vs. implication

From the general equivalence also follows import-export, 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.

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. However, it holds when inserting double-negations on the left. In fact, the principle in the next section implies

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

Finally, 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 )}$.

Disjunction vs. implication

Akin to modus ponens, clearly ${\displaystyle (\phi \lor \psi )\to ((\phi \to \psi )\to \psi )}$. Indeed, minimal logic already proves this implication, and variants thereof. Classically, this is an equivalence. 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 immediately 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.

Equivalences

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.

Functionally complete 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:^[7]

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

Paraconsistent logic

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

Intermediate logics

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.

For a schema not involving negations, consider the classically valid ${\displaystyle (A\to B)\lor (B\to A)}$. Adopting this over intuitionistic logic gives the intermediate logic called Gödel-Dummett 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.^[15] (See the section titled Heyting algebra semantics above for an infinite-valued logic interpretation of intuitionistic logic.)

Modal 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 that the translated formula is valid in the propositional modal logic S4 if and only if the original formula is valid in IPC.^[16] 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.^[17]