This may be a duplicate question but I am curious as to the answer regarding the statement "some theorems can only be proved by contradiction".

In Can every proof by contradiction also be shown without contradiction the highly voted answer claims that

It is known that there are statements that are provable in intuitionistic logic but not in minimal logic, and there are statements that are provable in classical logic that are not provable in intuitionistic logic.

Further in Theorems that we can only prove by contradiction the answer claims that

There are in fact numerous theorems that cannot be proved without arguing by contradiction. A nice example is the extreme value theorem (EVT). One cannot prove this theorem without an argument by contradiction, whose main ingredient is the Law of Excluded Middle (LEM). There are alternatives to classical logic where the LEM is not part of the package. Such logics are generally known as intuitionistic logics. It turns out that the extreme value theorem is actually false in one such setting. From this it follows that the EVT cannot be proved without LEM.

My problem is that as far as I am aware classical logic can be embedded in intuitionistic logic via double-negation translation. See Double-negation translation

What does this mean? Does it simply mean that the consistency strength is the same, or does it mean that all classical theorems can be proved in a classically equivalent form without contradiction? In fact is there a difference between those two statements?

• Please clarify your question: what does what mean? Does what mean that the consistency strength of what and what is the same? Is there a difference between which two statements? – Rob Arthan Feb 9 '15 at 20:56
• @RobArthan my question is what does the fact that classical logic can be embedded in intuitionistic logic mean? Does it mean simply that classical logic and intuitionistic logic have the same consistency strength given that intuitionistic logic can also be embedded in classical logic or does it mean the stronger statement, if indeed it is stronger, that all classical theorems can be proved without contradiction? – GYL Feb 10 '15 at 11:47
• From the point of view of classical logic, intuitionsitic logic, being a subsystem of the classical one, is consistent if classical logic is. Of course, form the point of view of intuitionistic logic, the classical one is "unsound", because it proves false formulae, like $P \lor \lnot P$. – Mauro ALLEGRANZA Feb 17 '15 at 7:57
• From the point of view of intuitionistic logic, the Double-negation translation means that if the classical logic is inconsistent, then also the intuitionistic one is. – Mauro ALLEGRANZA Feb 17 '15 at 8:13

Yes, classical logic can be embedded in intuitionistic logic through double-negation, and the double-negation must satisfy the requirement of being classically provable to be regarded as consistent, though they are not equivalent intuitionistically.

In regards to classical theorems (C-wff's for the purpose of this post) being proved in a classically equivalent form without contradiction, it would require constructivism as the proof would be an attempt to prove a positive case. A proof of a positive case can only be supported, and to prove a wff without assuming the opposite and deriving a contradiction is impossible. A wff by definition is a theorem of a system which means it is a self-contained proof.

The consistency is system dependent, for example if the C-wff has an equivalent intuitionistic wff (I-wff) the constructivism generates an object example of a positive case - but to truly prove that the positive case holds in all instances of that object it would require the use of modal logic and a proof of the object and correlated properties maintaining existence and properties in all possible worlds.

The result is that the system of logic would lose consistency given the completeness is being furthered by use of alternating systems to assert the positive.

All classical theorems cannot be proven in a classically equivalent form without contradiction. The proof would require premises to support the conclusion, which does not prove the conclusion and is not a wff in any respect.

• This is very unclear, particularly your statements about constructivism and modal logic. The logical structure of the last two sentences is impenetrable. – Rob Arthan Feb 9 '15 at 21:00

I'm going to have a stab at answering my question myself.

There is a difference between proof by negation and proof by contradiction.

In proof by negation ¬$\phi$ is proved by assuming $\phi$ and deriving a contradiction.

In proof by contradiction $\phi$ is proved by assuming ¬$\phi$ and deriving a contradiction.

The former is based on the principle of explosion and is thus admissible in intuitionistic logic whereas the latter requires excluded middle and thus is only admissible in classical logic.

By double negation translation we can convert a proof by contradiction into a proof by negation, in other words, we can prove ¬¬$\phi$ by assuming ¬$\phi$ and deriving a contradiction.

The upshot of all of this is that some theorems can only be proved by negation in the intuitionistic setting and some theorems can only be proved by contradiction in the classical setting.

• "Proof by negation" isn't standard terminology (in fact, the negation $\lnot \phi$ is often defined to be a short-hand for $\phi \Rightarrow \bot$, so that your proof by negation is just the usual rule for proving an implication). – Rob Arthan Feb 11 '15 at 11:19

GYL's answer is good, so this answer is mainly trying to explain the standard terminology.

The difference between minimal logic and intuitionistic logic is the presence of a logical constant (which I will call $\bot$) for falsehood and the rule ex false quodlibet (EFQ) for short. EFQ says you can infer anything from $\bot$: from $\phi \Rightarrow \bot$ you can infer $\phi \Rightarrow \psi$ for any $\psi$. It is then convenient to define negation $\lnot \phi$ to be an abbreviation for $\phi \Rightarrow \bot$, because the axioms or rules for negation follow from this: e.g., $\lnot \phi \Rightarrow \phi \Rightarrow \psi$ is just a restatement of EFQ.

The difference between intuitionistic logic and classical logic can be captured by several principles, the two common ones being the law of the excluded middle (LEM) and the law of double negation elimination (DNE). LEM asserts $\phi \lor \lnot\phi$ for every $\phi$ and DNE asserts that $\lnot\lnot\phi\Rightarrow\phi$ for every $\phi$. DNE is your principle of proof by contradiction, since it is the same as $(\lnot\phi \Rightarrow\bot) \Rightarrow\phi$. It can be shown that intuitionistic logic proves that LEM and DNE are equivalent. Most of the literature takes LEM as the defining axiom that distinguishes classical logic from intuitionistic logic.

Classical logic can indeed be embedded in intuitionistic logic via one of several double negation translation schemes, e.g., see http://www.eecs.qmul.ac.uk/~pbo/papers/paper039.pdf. However, this does not mean that any classically provable $\phi$ can be proved without using LEM or DNE, but rather that, for any $\phi$, the translation $\phi^*$ say of $\phi$, which is classically equivalent to $\phi$, is provable intuitionistically iff $\phi$ is provable classically.