11
$\begingroup$

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.

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ "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. $\endgroup$
    – Reid Barton
    Commented Dec 9, 2009 at 5:21
  • $\begingroup$ Upvote for showing me an awesome theorem in the question :) Can you provide a reference for it? $\endgroup$
    – Andrew Critch
    Commented Dec 9, 2009 at 7:15
  • 1
    $\begingroup$ 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.) $\endgroup$
    – Neel Krishnaswami
    Commented Dec 9, 2009 at 16:18
  • 1
    $\begingroup$ @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). $\endgroup$
    – Reid Barton
    Commented Dec 9, 2009 at 18:52
  • $\begingroup$ Actually, there are infinitely many intuitionistically nonequivalent formulas in just one propositional variable. Search for Rieger–Nishimura lattice. $\endgroup$
    – Emil Jeřábek
    Commented Dec 4, 2014 at 15:29

4 Answers 4

Reset to default
6
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Could you define that symbol T for those of us who aren't familiar with that symbol in this context? $\endgroup$
    – Harry Gindi
    Commented Dec 9, 2009 at 4:18
11
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Yes, that's right. I added a link to the Wikepedia article on the double negation translation. $\endgroup$
    – Joel David Hamkins
    Commented Dec 9, 2009 at 5:08
6
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • $\begingroup$ 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. $\endgroup$
    – Reid Barton
    Commented Dec 9, 2009 at 18:56
  • $\begingroup$ 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. $\endgroup$
    – Countably Infinite
    Commented Jun 5, 2011 at 13:03
  • $\begingroup$ 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$. $\endgroup$
    – Christoph-Simon Senjak
    Commented Dec 15, 2014 at 23:23
1
$\begingroup$

The translations into INT are derivable iff the classical expressions so translated are derivable. For instance, A v ¬ A is not intuitionistically derivable. A v ~ A is classically derivable. Now, one of the available translations from classical to intuitionistic is the Gödel translation, such that: g(A v ~ A) = ¬ (¬ g(A) & ¬ g(~ A)) = ¬ (¬ ¬ ¬ A & ¬ ¬ g(A)) = ¬ (¬ ¬ ¬ A & ¬ ¬ ¬ ¬ A). This should be intuitionistically derivable then although [A v ¬ A] is not.

Improve this answer
$\endgroup$

You must log in to answer this question.