2
$\begingroup$

I do understand that constructive logic forbids the "lemma of excluded middle" for various reasons (let's not discuss these now).

I do understand that lots & lots of classical theorems are done with LEM in place - mostly, implicitly, which renders them invalid within the constructive approach.

Recently I've met the double negation translation which states that:

If $T$ is a set of axioms and $\phi$ is a formula, then $T$ proves $\phi$ using classical logic if and only if $T^N$ proves $\phi^N$ using intuitionistic logic.

That sounds like the intuitionistic logic is at least as strong as the classical logic in the sense that at least all the classical theorems whatsoever are provable constructively. And then this answer emerges in front of my eyes stating: "a statement provable in PA (Peano arithmetic) but not in HA (Heyting arithmetic)".

I can't get it. Why could not some "double negation translation" be used here to prove it? What is the "double negation translation" essentially then? Where can I find a good example of some well known classical theorem to be "translated" using it?

P.S. It might be wrong, but terms "constructive logic" and "intuitionistic logic" are interchangeable to me.

From the discussion in the comments: not every statement provable classically can be proved within the constructive logic as is. However, translated instance of it could be proved indeed. That comes at the cost of being much weaker due to double negation constructive flavor: proving that "some set $X$ has some element" is one thing and proving that "it is not the case that the set $X$ does not has any element" - is another. The last statement is much weaker, especially in the constructive sense: in order for it to be as strong as the classical mate, it has to construct some element $x \in X$, which the double negation translation does not achieve.

$\endgroup$
7
  • $\begingroup$ Why does it sound like that? That’s not what it says at all. $\endgroup$
    – spaceisdarkgreen
    Mar 12 at 17:37
  • 3
    $\begingroup$ Yes and it has very important relative consistency implications. You say in the question “at least all the classical theorems are provable constructively” and in comment you say “whenever you prove something classically you can prove a translated version constructively”. See the difference? $\endgroup$
    – spaceisdarkgreen
    Mar 12 at 17:45
  • 2
    $\begingroup$ That’s the right way to look at it, with the minor correction that the translation for first order logic is not quite as simple as just double negation (for propositional logic it is that simple). $\endgroup$
    – spaceisdarkgreen
    Mar 12 at 17:55
  • 2
    $\begingroup$ In classical logic, $P$ and $\lnot\lnot P$ are equivalent. But in intuitionistic logic, although $\lnot\lnot P$ is weaker than $P$, in the sense that $P\to \lnot\lnot P$ but it is not always the case that $\lnot\lnot P\to P$. The double-negation translation shows that when $Q$ is classically valid, $\lnot\lnot Q$ is intuitionistically valid. But intuitionistically, $\lnot\lnot Q$ is not enough to prove $Q$. $\endgroup$
    – MJD
    Mar 12 at 18:26
  • 2
    $\begingroup$ For example, although $P\lor\lnot P$ is not intuitionistically valid, $\lnot\lnot(P\lor\lnot P)$ can be proven in intuitionistic logic; see math.stackexchange.com/q/140197/25554 $\endgroup$
    – MJD
    Mar 12 at 18:40

1 Answer 1

Reset to default
6
$\begingroup$

Say you have a propositional $\phi$ provable classically, then double negation translation basically says $\neg\neg\phi$ is provable intuitionistically, how can you then prove $\phi$ still with intuitionistic logic alone? Where classical logic can prove "set $X$ has an element", intuitionistic logic can (prima facie) only prove its double negation, that is "It's not the case that $X$ is empty", which is definitely weaker (saying that something is non-empty is not the same as producing an actual element of $X$, which is the requirement for a constructive proof that $X$ has an element).

That being said, I'd like to add if you have a negative proposition, then this is provable classically if and only if provable intuitionistically, since $\neg\neg\neg\phi\Rightarrow\neg\phi$ intuitionistically. So a corollary of double negation translation is that "A proposition $\neg\phi$ can be proved classically if and only if it can be proven intuitionistically".

$\endgroup$
3
  • $\begingroup$ Don’t you mean “prima facie” instead of “a priori”? $\endgroup$
    – PW_246
    Mar 12 at 18:45
  • $\begingroup$ Just to clarify, your claim “If $\phi$ is provable classically then $\neg \neg \phi$ is provable intuitionistically” only holds for for propositional logic. $\forall x (P(x) \lor \neg P(x))$ holds classically, but $\neg \neg \forall x (P(x) \lor \neg P(x))$ is not necessarily true intuitionistically. $\endgroup$
    – Mark Saving
    Mar 19 at 4:08
  • $\begingroup$ Actually, I meant first-order logic (otherwise the example "$X$ has an element" is not valid, being first-order). I messed up the translation in first-order and wrote it to double negation. $\endgroup$
    – Alessandro
    Mar 20 at 16:05

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .