Intuitionistic logic rejects proof methods like double negation and proof by contradiction, making it impossible to make, for example, existence proofs without having a method of deriving what is trying to be proved to exist. Hence, intuitionistic logic is sometimes referred to as "constructive".

That certainly has value, but are there any cases where using classical methods of reasoning have derived results that are actually not true using methods like the law of the excluded middle, or the law of double negation?

From what I understand, to use something like the law of the excluded middle implicitly assumes that the system we are trying to construct a proof under is consistent, since if the system were inconsistent, the negation of a hypothesis leading to a contradiction does not nescesarialy lead to the truth of the hypothesis.

Are there issues, even hypothetical, with using classical logic to derive non-constructive results? I know many in the intuitionistic camp will reject proofs by the law of the excluded middle, but is that simply for preferential reasons, or is there good reason to believe that proofs by law of the excluded middle might somehow possibly be flawed, even theoretically? How may we know whether or not a given set of logical inference rules will be "correct" for proving results about a given axiomatic system or not, the set of logical inference rules being an axiomatic system itself?

  • 5
    $\begingroup$ What do you mean "an incorrect result"? Are you asking if classical logic is unsound somehow? If we had a proof of that, why would we be using classical logic nowadays at all? (HINT: We are using classical logic nowadays.) $\endgroup$
    – Asaf Karagila
    Oct 13, 2014 at 1:28
  • $\begingroup$ This is an old post, but it is worth mentioning that every reasonable meta-system is classical. Without classical logic, you cannot do any reasonable meta-logic. For instance, almost all the theorems about intuitionistic logic are proven using a classical meta-system. $\endgroup$
    – user21820
    Jan 7, 2019 at 14:18
  • 2
    $\begingroup$ @user21820 Do you have any examples of results that depend essentially on the use of a classical meta-theory? I'm having a hard time seeing how relevant that would be for (e.x.) basic theorems about intuitionistic logic -- given that so many of the results (at least in proof theory) are based on pretty constructive, combinatorial reasoning -- where all of the objects (e.x. the rules and derivations) are decidable. $\endgroup$ Jan 22, 2019 at 20:17
  • $\begingroup$ @NathanBeDell: Without LEM, you cannot even prove that every first-order theory is either consistent or inconsistent. $\endgroup$
    – user21820
    Jan 24, 2019 at 15:41
  • 1
    $\begingroup$ @user21820 It’s exactly the opposite. Meta logic is typically done in an intuitionist meta theory such as primitive recursive arithmetic. Godel deliberately did much of his work in logic using constructive metalogic. If you’re using classical meta logic and prove that a theory is inconsistent, you don’t necessarily know it actually is inconsistent since classical logic lacks a certain form of the existence property. $\endgroup$ Oct 24, 2021 at 2:48

2 Answers 2


There is a constructive proof that, if a theorem $T$ is provable classically, then a related theorem $T^N$ is provable constructively, and $T$ is classically equivalent to $T^N$. The theorem $T^N$ is obtained by what is called a "double negation translation" of $T$, although there are several ways to obtain this translation, as the linked article describes.

One of the original goals of this method was to give a consistency proof of classical logic. The theorem is: if a contradiction is provable in classical logic alone, then there is also a contradiction provable from constructive logic alone. Moreover, this theorem has a constructive proof. There is a section on this in the article Intuitionistic Logic in the Stanford Encyclopedia of Philosophy. It is a well known fact in the field of proof theory.

The relationship between classical and constructive logic has been studied by many people, but a phrase of Kolmogorov is particularly poignant. In his article "On the tertium non datur principle", Kolmogorov described theorems of classical logic as "pseudo-true" from a constructive viewpoint. By this, he meant essentially that they are not not true. He argued that, from a constructive viewpoint, classical mathematics could be seen as they study of "pseudo-truth".


Adding to Carl Mummert's statements:

Notation: $\vdash$ means "provable in constructive logic", while $\vdash_{classical}$ means "provable in classical logic".

Suppose we have a multi-sorted vocabulary $V$. Note: this result can be generalised to dependently typed logics, but we won't get into that here.

We define the double-negation translation of a formula $\phi$ as follows:

  • $translation(\top) = \top$, $translation(\bot) = \bot$
  • If $a, b$ are terms of the same sort, $translation(a = b) = \neg \neg (a = b)$
  • If $P$ is a predicate and $t_1, \ldots, t_n$ are terms of the appropriate sorts, $translation(P(t_1, \ldots, t_n)) = \neg \neg P(t_1, \ldots, t_n)$
  • If $\phi$ and $\xi$ are statements, then $translation(\phi \lor \xi) = \neg \neg (translation(\phi) \lor translation(\xi))$, $translation(\phi \land \xi) = translation(\phi) \land translation(\xi)$, and $translation(\phi \to \xi) = translation(\phi) \to translation(\xi)$
  • If $\phi(x)$ is a statement, then $translation(\forall x . \phi(x)) = \forall x . translation(\phi(x))$ and $translation(\exists x . \phi(x)) = \neg \neg \exists x . \phi(x)$.

Note here that $\neg \xi$ is taken as syntactic sugar for $\xi \to \bot$. So $translation(\neg \psi) = \neg translation(\psi)$.

I claim that for all sentences $\phi$, if $\vdash_{classical} \phi$ then $\vdash translation(\phi)$.

To prove this, we need to go through all the axioms in the classical Hilbert calculus one by one and, for each axiom $\xi$, prove $\vdash translation(\xi)$. This is a straightforward exercise, but a bit tedious.

Then, we need to prove the "modus ponens" rule as applied to translations.

Suppose we have $\vdash translation(a)$ and $\vdash translation(a \to b)$. Then we have $\vdash translation(a) \to translation(b)$. Then we have $\vdash translation(b)$.

This forms the base case and the inductive step for proving that for all derivations $\vdash_{classical} \psi$ in the Hilbert system, there is a derivation $\vdash \psi$.

It's also pretty easy to show that for all $\psi(x_1, \ldots, x_n)$, we have $\vdash_{classical} \forall x_1 \ldots \forall x_n . \psi(x_1, \ldots, x_n) \iff translation(\psi(x_1, \ldots, x_n))$. This follows from induction on $\psi$.

So in particular, for $\phi$ a sentence, we have $\vdash_{classical} \phi \iff translation(\phi)$. So if $\vdash \phi$, then $\vdash_{classical} \phi$, and thus $\vdash_{classical} translation(\phi)$.

Therefore, for all sentences $\phi$, we have $\vdash_{classical} \phi$ if and only if $\vdash translation(\phi)$.

Now consider a set $S$ of sentences over $V$. Let $translation(S) = \{translation(s) \mid s \in S\}$. I claim that $translation(S) \vdash translation(\psi)$ if and only if $S \vdash_{classical} \psi$.

For note that given any sentences $s_1, \ldots, s_n, \phi$, we have $\vdash translation(s_1) \land \cdots \land translation(s_2) \to translation(\phi)$ if and only if $\vdash translation(s_1 \cdots\ldots \land s_n \to \phi)$ if and only if $\vdash_{classical} s_1 \land \cdots \land s_n \to \phi$.

If $translation(S) \vdash translation(\psi)$, then there are $s_1, \ldots, s_n \in S$ such that $\vdash translation(s_1) \land \cdots \land translation(s_n) \vdash translation(\psi)$, and therefore $\vdash_{classical} s_1 \land \cdots \land s_n \to \psi$, and therefore $S \vdash_{classical} \phi$. And conversely, if $S \vdash_{classical} \phi$ then there are $s_1, \ldots, s_n \in S$ such that $\vdash_{classical} s_1 \land \cdots \land s_n \to \psi$, and therefore $\vdash translation(s_1) \land \cdots \land translation(s_n) \to translation(\psi)$, and therefore $translation(s) \vdash translation(\psi)$.

This gives us the following result:

Let $S$ be a set of sentences. Then $S$ is logically inconsistent in classical logic if and only if $translation(S)$ is logically consistent in intuitionist logic.

In other words, $S \vdash_{classical} \bot$ if and only if $S \vdash translation(\bot)$. But $translation(\bot) = \bot$.

Let's call a set $S$ of sentences "nice" if and only if $S \vdash translation(S)$. Then if $S$ is nice, we see that $S$ is logically inconsistent in classical logic if and only if $S$ is logically inconsistent in constructive logic.

There are quite a few nice theories which can be described this way. For example, let $V$ be the 1-sorted vocabulary $\{0, S, +, \cdot\}$, and let $S$ be the axioms of Peano Arithmetic. Then $S \vdash translation(S)$, as can be manually verified. Thus, classical Peano Arithmetic is equiconsistent with constructive Peano arithmetic (also known as Heyting arithmetic).

Unfortunately, not all theories can be approached in this way. For example, the axioms of ZF are not "nice" (if you use replacement and $\in$-induction, that is). However, using some more advanced techniques, we can prove that ZF is equiconsistent with intuitionist ZF formulated using collection. There are many other equiconsistency proofs applying to weaker versions of set theory such as ETCS.

So in this sense, classical logic can no more lead to contradiction than intuitionist logic can in most common cases.

If you don't believe the law of excluded middle, however, then classical logic proves something "wrong" just by accepting the law of excluded middle. This is more of a philosophical argument than a mathematical one.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.