# intuitionistic interpretation of classical logic

Basically intuitionistic logic is classical logic minus the law of the excluded middle, i.e. $\neg A\vee A$ is not necessarily valid for all formulas. So I would take this to mean that classical logic allows one to prove more theorems but apparently this view is too naive because yesterday I read the following in a book on proof theory:

Given a formula C, there is a translation giving a formula C* such that C and C* are classically equivalent and C* is intuitionistically derivable if C is classically derivable. … The translation gives an interpretation of classical logic in intuitionistic logic.

How am I supposed to understand the above statement? Is it saying that every theorem that uses the law of excluded middle in its proof can be done without the law of excluded middle or is it saying something more subtle?

Edit: Thanks to the answers I received the interpretation of the quote is in fact much more subtle than I was thinking. The double negation translation allows us to prove $\neg\neg C=C^*$ if we can classically prove $C$ but in intuitionistic logic $\neg\neg C$ and $C$ are not necessarily equivalent. I think intuitively this means that there is a subtle semantic difference between $C$ and $\neg\neg C$. In intuitionistic logic a single classical theorem is potentially two intuitionistic theorems since knowing $\neg\neg C$ does not tell us much about $C$. So my naive interpretation was quite wrong. There are potentially more theorems in intuitionistic logic than there are in classical logic.

Edit 2: The last sentence is not precise and Reid Barton has an excellent comment on what I was actually thinking.

-
"More" is a tricky word, and both "there are more theorems in intuitionistic logic than in classical logic" and "there are more theorems in classical logic than in intuitionistic logic" have natural true interpretations. –  Reid Barton Dec 9 '09 at 5:21
Well, the double negation translation gives us the injection of classical logic into intuitionistic logic but it seems to me that the map going back would have to collapse not-not-C and C which are different in intuitionistic logic into just C. We can make more subtle distinction in intuitionistic logic so it seems to me that the inclusion is only one way. –  davidk01 Dec 9 '09 at 5:48
@Andrew Critch: The book I was reading when I stumbled upon that statement is called "Structural Proof Theory" by Sara Negri & Jan Von Plato page 27, 3rd paragraph. Although the specific construction was mentioned by Joel Hamkins and it's called Godel-Gentzen negative translation. –  davidk01 Dec 9 '09 at 8:51
davidk01: you can convert intuitionistic logic into classical modal logic using the Godel translation. Basically you introduce a modality "provable", and view intuitionistic $A \to B$ as classical $provable(A) \to B$. So intuitionistic implications are weaker than classical ones, since their assumptions are stronger, but its conclusions are stronger than classical ones, since you get actual existence proofs. This contravariance makes comparing it to classical logic hard, and show why there are constructively legit principles that are false classically. (E.g., all functions are continuous.) –  Neel Krishnaswami Dec 9 '09 at 16:18
@davidk01: that's how you can interpret the first statement; the second statement can be interpreted as "Every theorem of intuitionistic logic is a theorem of classical logic, but not conversely." Maybe a better way of capturing your idea is the observation that given n variables, there are more intuitionistically nonequivalent formulas in those variables (but still finitely many!) than there are classically nonequivalent formulas (2^2^n). –  Reid Barton Dec 9 '09 at 18:52

Note that the statements are classically equivalent; the intuitionistically derivable statement may be intuitionistically weaker.

For example, the classical ‘law of the excluded middle’ $\lnot A \vee A$ is classically equivalent to $\top$, which is certainly intuitionistically derivable, even though the law of the excluded middle is not.

Does that help to understand the meaning of the statement?

EDIT: fqpc points out that the symbol $\top$ might be non-standard in this context. It probably comes from too much recent reading of the computer-science literature, where it's used for ‘top’ (the type of which all other types are a subtype; as opposed to ‘bottom’, $\bot$, which is a subtype of all other types)—and, indeed, that's the TeX code for it.

I thought it was common usage as a sort of visual pun on ‘true’ or ‘tautology’—an abbreviation for the empty statement.

-
Could you define that symbol T for those of us who aren't familiar with that symbol in this context? –  Harry Gindi Dec 9 '09 at 4:18
Ah, yes. There was an equivalence relation that I was not paying attention to. So this translation does not necessarily preserve the entire semantics of the classical statement. –  davidk01 Dec 9 '09 at 4:18

The translation you refer to is just the double-negative. That is, C is classically derivable if and only if not-not-C is intuitionistically derivable.

What this fact shows is that the use of the law of excluded middle in classical logic can be contained entirely in the proof that C and not-not-C are equivalent.

Edit. Here is a reference to the Gödel–Gentzen negative translation, which explains the translation. The situation is that in propositional logic, one can just use the double negation, but in first order logic, one must perform double negation hereditarily, applying the translation to the subformulas fo the formula. The basic idea is that classical laws of deduction become intuitionistically valid for the double negated forms.

-
I thought some more: Intuitionistically, C and not-not-C are in general not equivalent so just because we can prove not-not-C intuitionistically does not mean that we can do the same for C. Let me know if I'm on the right track. –  davidk01 Dec 9 '09 at 4:44
Yes, that's right. I added a link to the Wikepedia article on the double negation translation. –  Joel David Hamkins Dec 9 '09 at 5:08

There exists a translation, T, applicable to both propositions and proofs with the property that:

If $P$ is a classical proof of $\phi$ then $P^T$ is an intuitionistic proof of $\phi^T$.

(Trivially, any intuitionistic proof is also a perfectly good classical one.)

The details of some versions of the translation of the proof can be found in computer science texts under the name "CPS translation", though with different notation. Surprisingly this translation has an alter-ego as one of the stages when compiling certain programming languages.

Update: Adding (1) more detail and (2) something on the CPS translation.

(1) These translations don't allow you to completely remove double-negation elimination from classical proofs. But they do allow you to pull all of the double negation eliminations all the way out of the body of the proof to the very last line. So starting with a classical proof of $\phi$ we can translate it into an intuitionistic proof of $\neg\neg\phi$ and then we can tack one double negation elimination step onto the end to turn this back into a classical proof of $\phi$.

(2) According to the Curry-Howard isomorphism, a proof $P$ of a theorem $\phi$ can be interpreted as a program $P$ that produces a result of type $\phi$. When we convert a program to "continuation passing style", instead of just accepting a result of type $\phi$ back from our program, we instead write a program that accepts an extra argument (known as a continuation) that tells the program what it should do with its result. Ie. instead of writing a program of type $\phi$ we write a program of type $(\phi\rightarrow k)\rightarrow k$. The continuation is the extra argument of type $\phi\rightarrow k$ and we now get a final result of type $k$. The CPS translation takes an already existing program of type $\phi$ and converts it to one of type $(\phi\rightarrow k)\rightarrow k$. It's a bit fiddly but you can get a translation by following your nose, so to speak. Every function that your program calls also has to be modified so that it too uses the continuation and you thread the continuation all the way through the code.

But by the Curry-Howard isomorphism, this means you're translating a proof of the proposition $\phi$ into a proof of $(\phi\rightarrow k)\rightarrow k$. This is basically a version of the Godel-Gentzen translation as described in Constructivism in Mathematics: an Introduction Studies in Logic and the Foundations of Mathematics (by A. S. Troelstra and D. van Dalen.) A nice result of this is that you can now interpret classical proofs as computer programs.

I think it is a pretty amazing fact that you can take some esoteric mathematics comparing two systems of logic and turn it directly into code that can be used in a compiler.

-
Please elaborate. I have often heard of "CPS translation" but I don't have a good intuitive grasp of it. Every explanation I stumble upon just says the "CPS translation" takes functions and tacks on an extra argument. –  davidk01 Dec 9 '09 at 5:53
One should also comment that in the CPS translation, one can trivially implement callcc, whose type is Peirce's law, providing the link to classical logic. –  Reid Barton Dec 9 '09 at 18:56
What bothers me here is that Curry-Howard isomorphism, i.e. simple types, only yields minimal logic. Does the Godel-Gentzen translation also hold for minimal logic as a target? We would need to add a type constant for $\bot \rightarrow A$ to minimal logic (Ex Falso Quodlibet), to have inituitionist logic. –  Countably Infinite Jun 5 '11 at 13:03
You can always get a $\bot$ equivalent if you set it to the conjunction of all atomic formulae in your proof. Furthermore, in the calculus of constructions, you can define $\bot$ as an inductive predicate with zero constructors, and ex falso quodlibet becomes the induction principle over $\bot$. –  Christoph-Simon Senjak Dec 15 '14 at 23:23