# Is there any case where classical logic has “proven” an incorrect result?

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?

• 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.) – Asaf Karagila Oct 13 '14 at 1:28
• 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. – user21820 Jan 7 at 14:18
• @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. – Nathan BeDell Jan 22 at 20:17
• @NathanBeDell: Without LEM, you cannot even prove that every first-order theory is either consistent or inconsistent. – user21820 Jan 24 at 15:41

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.