This is a follow up question to

What is the difference between proofs and programs (or between propositions and types)?

What program would correspond to a non-constructive (classical) proof of the form $\forall k \ T(e,k) \lor \lnot \forall k \ T(e,k)$? (Assume that $T$ is some interesting decidable relation e.g. $e$-th TM does not halt in $k$ steps.)

(ps: I am posting this question partly because I am interested in learning more about what Neel means by "the Godel-Gentzen translation is a continuation-passing transformation" in his comment.)

  • 2
    Partial answer on page 2 of these lecture notes. It's a bit cryptic; I'll try to dig up something more complete. – Dave Clarke Mar 2 '11 at 18:28
  • It's taking me a little longer than planned to write my answer, since I made the mistake of deciding to prove the things I knew rather than just asserting them. :) – Neel Krishnaswami Mar 2 '11 at 23:09
  • 1
    The most recent JSL had this article. The gist is that the computational content of classical proofs may strongly depend on how you chose to extract it. I haven't really digested it yet, but I thought I'd throw it out there. – Mark Reitblatt Mar 3 '11 at 0:38
  • But you've specified that T is a decidable relation, so it follows that there are constructive proofs of your proposition. Classical logic is a subset of intuitionistic logic and you specified that T belongs to that subset by calling it decidable. – wren romano Mar 5 '11 at 2:59
  • wren, that's what I thought at first too! But the proposition P in the P \/ ~P example in the question if actually quantified over all k, and this quantification of T is not necessarily decidable. – jbapple Mar 5 '11 at 4:58
up vote 25 down vote accepted

This an interesting question. Obviously one can't expect to have a program that decides for each $e$ whether $\forall k T(e, k)$ holds or not, as this would decide the Halting Problem. As mentioned already, there are several ways of interpreting proofs computationally: extensions of Curry-Howard, realizability, dialectica, and so on. But they would all computationally interpret the theorem you mentioned more or less in the following way.

For simplicity consider the equivalent classical theorem

(1) $\exists i \forall j (\neg T(e, j) \to \neg T(e, i))$

This is (constructively) equivalent to the one mentioned because given $i$ we can decide whether $\forall k T(e, k)$ holds or not by simply checking the value of $\neg T(e, i)$. If $\neg T(e, i)$ holds then $\exists i \neg T(e, i)$ and hence $\neg \forall i T(e, i)$. If on the other hand $\neg T(e, i)$ does not hold then by (1) we have $\forall j (\neg T(e, j) \to \bot)$ which implies $\forall j T(e, j)$.

Now, again we can't compute $i$ in (1) for each given $e$ because we would again solve the Halting Problem. What all interpretations mentioned above would do is to look at the equivalent theorem

(2) $\forall f \exists i' (\neg T(e, f(i')) \to \neg T(e, i'))$

The function $f$ is called the Herbrand function. It tries to compute a counter example $j$ for each given potential witness $i$. It is clear that (1) and (2) are equivalent. From left to right this is constructive, simply take $i' = i$ in (2), where $i$ is the assumed witness of (1). From right to left one has to reason classically. Assume (1) was not true. Then,

(3) $\forall i \exists j \neg (\neg T(e, j) \to \neg T(e, i))$

Let $f'$ be a function witnessing this, i.e.

(4) $\forall i \neg (\neg T(e, f'(i)) \to \neg T(e, i))$

Now, take $f = f'$ in (2) and we have $(\neg T(e, f'(i')) \to \neg T(e, i'))$, for some $i'$. But taking $i = i'$ in (4) we obtain the negation of that, contradiction. Hence (2) implies (1).

So, we have that (1) and (2) are classically equivalent. But the interesting thing is that (2) has now a very simple constructive witness. Simply take $i' = f(0)$ if $T(e, f(0))$ does not hold, because then the conclusion of (2) is true; or else take $i' = 0$ if $T(e, f(0))$ holds, because then $\neg T(e, f(0))$ does not hold and the premise of (2) is false, making it again true.

Hence, the way to computationally interpret a classical theorem like (1) is to look at a (classically) equivalent formulation which can be proven constructively, in our case (2).

The different interpretations mentioned above only diverge on the way the function $f$ pops up. In the case of realizability and the dialectica interpretation this is explicitly given by the interpretation, when combined with some form of negative translation (like Goedel-Gentzen's). In the case of Curry-Howard extensions with call-cc and continuation operators the function $f$ arises from the fact that the program is allowed to "know" how a certain value (in our case $i$) will be used, so $f$ is the continuation of the program around the point where $i$ is computed.

Another important point is that you want the passage from (1) to (2) to be "modular", i.e. if (1) is used to prove (1'), then its interpretation (2) should be used used in similar way to prove the interpretation of (1'), say (2'). All the interpretations mentioned above do that, including the Goedel-Gentzen negative translation.

  • 8
    Welcome! It's great to see an expert proof theorist here. – Neel Krishnaswami Mar 3 '11 at 14:39
  • 1
    Thanks Paulo, your answer has clarified a part of the picture in a related problem that I am working on. – Kaveh Mar 10 '11 at 8:48

It's fairly well-known that classical and intuitionistic arithmetic are equiconsistent.

One way of showing this is via the "negative embeddings" of classical logic into intuitionistic logic. So, suppose $\phi$ are formulas of classical first-order arithmetic. Now, we can define a formula of intuitionistic logic as follows:

$$ \begin{array}{lcl} G(\top) & = & \lnot\lnot\top \\ G(\phi \land \psi) & = & \lnot\lnot(G(\phi) \land G(\psi)) \\ G(\bot) & = & \lnot\top \\ G(\lnot\phi) & = & \lnot G(\phi) \\ G(\phi \vee \psi) & = & \lnot(\lnot G(\phi) \land \lnot G(\psi)) \\ G(\forall x.\;\phi) & = & \forall x.\; \lnot\lnot G(\phi) \\ G(\exists x.\;\phi) & = & \lnot \forall x.\; \lnot(G(\phi)) \\ G(P) & = & \lnot\lnot P \\ \end{array} $$

Note that $G(\phi)$ is basically a homomorphism that sticks in extra not-not's everywhere, except that at disjunctions and existentials, it uses de Morgan duality to turn them into conjunctions and universals. (I'm pretty confident this is not the exact Godel-Gentzen translation, since I cooked it up for this answer -- basically anything you write using double-negation + de Morgan duality will work. This variety actually turns out to be important for computational interpretations of classical logic; see below.)

First: It's obvious that this translation preserves classical truth, so that $G(\phi)$ is true if and only if $\phi$ is, classically speaking.

Second: It's less obvious, but still the case, that for formulas in the $\forall, \implies, \land, \lnot$ fragment, provability in intuitionistic and classical logic coincide. The way to prove this is to first look at formulas drawn from this grammar:

$$ \newcommand{\bnfalt}{\;\;|\;\;} \begin{array}{lcl} A,B & ::= & \forall x.\;A(x) \bnfalt A \implies B \bnfalt A \land B \bnfalt \lnot A \bnfalt \lnot\lnot P \end{array} $$

And then we can prove as a lemma (by induction on $A$) that $G(A) \implies A$ is derivable intuitionistically. So now, we can show the equiderivability of negative formulas by doing an induction over the structure of the proof (in, say, the sequent calculus) and use the previous lemma to simulate the law of the excluded middle.

So, how should you think about this intuitively?

  • First, the proof-theoretic view. If you look at the rules of the sequent calculus, you can see that the only place classical and intuitionistic logic seriously differ is in the rules for disjunction and existentials. So we are using this fact to show that that proofs in one logic of these formulas can be translated to proofs in the other. This shows how to think of constructive logic as an extension of classical logic with the two new connectives $\exists$ and $\vee$. What we call "classical existence" and "classical disjunction" were just abbreviations involving $\forall$, conjunction, and negation, and so to talk about actual existence we needed to introduce new connectives.

  • Second, there's a topological view. Now, the model of a classical logic (as a family of sets) is a Boolean algebra (ie, a family of subsets closed under arbitrary unions, intersections and complements). It turns out that the model of intuitionsitic logic is as a topological space, with the propositions being interpreted as open sets. Them the interpretation of negation is the interior of the complement, and then it's easy to show that $\lnot\lnot\lnot P = \lnot P$, which means that double-negation sends us into the smallest clopen covering each open --- and the clopens form a Boolean algebra.

Now, thanks to Curry-Howard, we know how to interpret proofs in intuitionistic logic as functional programs. So, one possible answer (but not the only one) to the question of "what is the constructive content of a classical proof?" is the following:

The computational content of a classical proof is whatever the computational content of the translation of its proof (according to the negative translation) is.

So let's look at the translation of $G(A \vee \lnot A) = \lnot(\lnot G(A) \land \lnot\lnot G(A))$. So this says that the constructive content of the excluded middle is the same as saying that it's not the case that $\lnot P$ and and $\lnot\lnot P$ hold -- ie, noncontradiction. So in this sense, there's not actually very much computational content to the law of the excluded middle.

To see what it is concretely, recall that constructively, negation is defined as $\lnot A == A \implies \bot$. So this formula is $((G(A) \implies \bot) \land ((G(A) \implies \bot) \implies \bot)) \implies \bot$. The following bit of Ocaml code will illustrate:

type bot = Void of bot
type 'a not = 'a -> bot

let excluded_middle : ('a not * 'a not not) not = fun (u, k) -> k u 

That is, if you get not-A and not-not-A, you can just pass the first negation to the second to derive the contradiction you want.

Now, what is a continuation passing-style transformations?

  • A continuation of type $\tau$ is something that takes a value of type $\tau$ and computes a final answer from it.
  • Continuations are used to model program contexts. That is we might have a term $3+5$ evaluating as part of a much larger program $C[3+5]$. All that stuff around it will take the result of computing $3 + 5$ and compute the final answer.
  • So you can think of a continuation of type $\tau$ as a function $\tau \to \alpha$, where $\alpha$ is whatever the answer type is.
  • So if you have a program $e$ of type $\tau$, we can "CPS-convert" it by finding a term of type $(\tau \to \alpha) \to \alpha$, which will end up passing whatever $e$ would have computed to its continuation. (Basically, this just makes control flow explicit.)
  • But we have to do this hereditarily, so that every subterm of the program has made its continuation explicit.

Now,

  • The negative translation basically hereditarily sends $\phi$ to $\lnot\lnot\phi$.
  • However, while our translation uses negation, it never actually eliminates the false proposition -- so the translation works parametrically in that proposition.
  • In particular, we can replace $\bot$ with any answer type $\alpha$.
  • So we hereditarily replace $\phi$ with $(\phi \to \alpha) \to \alpha$.
  • This is a CPS transformation.

I saw "a" CPS transformation, since as I mentioned earlier, there are many negative translations which let you prove this theorem, and each one corresponds to a different CPS trasnformation. In operational terms, each transformation corresponds to a different evaluation order. So there is no unique computational interpretation of classical logic, since you've got choices to make and the difference choices have very different operational characteristics.

  • 3
    This is a great answer. It reminded me of Wadler's paper "Call-by-value is dual to call-by-name": homepages.inf.ed.ac.uk/wadler/topics/call-by-need.html, which includes a very memorable anecdote in section 4 to explain the relationship between callCC and the excluded middle. – sclv Mar 3 '11 at 17:49

There are whole conferences on the subject of non-constructive proofs as programs, and I am no expert on the subject. Above, Neel Krishnaswami alluded to a longer answer he is preparing, which, judging from his work here, will be excellent. This is just a taste of an answer.

It turns out the the type of call-with-current-continuation corresponds to the proposition known as Peirce's law, which can be used to prove the Law of Excluded Middle ($\forall P, P \lor \lnot P$). An LEM program can be written using callcc. In Coq:

Set Implicit Arguments.

Axiom callcc : forall (A B : Set), ((A -> B) -> A) -> A.

Lemma lem : forall (A B:Set), sum A (A -> B).
Proof.
  intros.
  eapply callcc.
  intros H.
  right.
  intros.
  apply H.
  left.
  assumption.
Defined.

Recursive Extraction lem.

gives the O'Caml code:

type ('a, 'b) sum =
  | Inl of 'a
  | Inr of 'b

(** val callcc : (('a1 -> 'a2) -> 'a1) -> 'a1 **)

let callcc =
  failwith "AXIOM TO BE REALIZED"

(** val lem : ('a1, 'a1 -> no) sum **)

let lem =
    callcc (fun h -> Inr (fun h0 -> h (Inl h0)))

The cleanest introduction to this I have seen is in Tim Griffin's "A formulae-as-types notion of control".

  • 3
    You should try extracting into Scheme and tell the extraction procedure should extract your callcc to Scheme's callcc. Then you can actually try things out. – Andrej Bauer Mar 4 '11 at 14:47

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.