15
$\begingroup$

So a little while back I first had someone tell me that call/cc could allow proof objects for classical proofs by implementing Peirce's law. I did some thinking about the topic recently and I can't seem to find a flaw with it. However I can't really seem to see anyone else talking about it. It seems void of discussion. What gives?

It seems to me that if you have a construction like $f : \neg(\neg P)$ in some context then 1 of two things is true. Either you have access to an instance $\bot$ somehow in the current context in which case control flow would never reach here and we are safe to assume whatever OR given that $f : \neg(\neg P)$ means $f : (P \to \bot) \to \bot$ the only way $f$ can return $\bot$ is by constructing an instance of $P$ and applying it two it's argument (an instance of $P \to \bot)$. In such a case there was already SOME way of constructing an instance of $P$; it seems reasonable for call/cc to pull this construction out for me. My reasoning here seems somewhat suspect to me but my confusion still stands. If call/cc isn't just creating an instance of $P$ out of thin air (I don't see how it is) then what is the issue?

Do some well typed terms not containing call/cc not have normal forms? Is there some other property of such expressions that causes them to be suspect? Is there any noted reason why a constructivist shouldn't like call/cc?

$\endgroup$
19
$\begingroup$

Constructive mathematics is not just a formal system but rather an understanding of what mathematics is about. Or to put it differently, not every kind of semantics is accepted by a constructive mathematician.

To a constructive mathematician call/cc looks like cheating. Consider how we witness $p \lor \lnot p$ using call/cc:

  1. We provide a function $f$ which allegedly proves $\lnot p$. In reality $f$ is a bag of tricks.
  2. If anyone ever applies $f$ to a proof of $p$, then $f$ unleashes call/cc to roll back time, and with a proof of $p$ in hand, changes its mind about $p \lor \lnot p$: this time claiming that it is a proof of $p$.

The constructive understanding of disjunction is algorithmic decidability, but the above is hardly making any decisions. As a test, a constructive mathematician might ask you how call/cc helps prove that every Turing machine halts or diverges. And what is the program witnessing this fact? (It ought to be the Halting Oracle.)

$\endgroup$
  • $\begingroup$ Ah!! I think that is the kind thing I was looking for. $\endgroup$ – Jake Apr 7 '15 at 0:47
9
$\begingroup$

As you note, there is a possible constructive interpretation of classical logic in this sense. The fact that classical logic is equiconsistent with intuitionistic logic (say, Heyting Arithmetic) has been known for quite some time (already in 1933, e.g. Godel) using a double negation translation.

By a more sophisticated argument, it can be shown that Peano Arithmetic is conservative over HA for $\Pi^0_2$ statements. The essence of the result is that the classical proofs of $\Pi^0_2$ involving $\mathrm{call/cc}$ have the same computational content as a statement without that construct (by a CPS transformation).

However this is not true for statements above $\Pi^0_2$: statements in $\Sigma^0_3$, provable in PA, may not have a normal form amenable to extracting a witness! Computer scientists may not care about computing with proofs at this level, but it is somewhat inconvenient for philosophical considerations: have we proven the existence of something, or not?

I think this summarizes why "fixing" non-constructive logic by addition of $\mathrm{call/cc}$ may be unsatisfactory.

That being said, there is a lot of work exploring the computational aspects of computation within the "classical Curry-Howard" framework, e.g. the Krivine Machine, the Parigot calculus ($\lambda\overline{\mu}\tilde\mu$) and many others. See here for an overview.

Finally, it might be useful to note that while the situation is rather well understood in the predicate calculus and arithmetic cases, more powerful theories are much less explored. For example, IIRC, ZFC is conservative over IZF for $\Pi^0_2$ sentences as well (ZFC is conservative over ZF for arithmetic sentences, and ZF is conservative over IZF), which suggests there is a computational meaning for the axiom of choice. However this is very much an active field of research (krivine, Berardi et al.)

Edit: A very relevant question on mathoverflow appears here: https://mathoverflow.net/questions/29577/solved-sequent-calculus-as-programming-language

$\endgroup$
  • 1
    $\begingroup$ Is this equiconsistency true constructively? $\endgroup$ – Geoffrey Irving Apr 6 '15 at 21:46
  • 3
    $\begingroup$ @GeoffreyIrving: yes it is, one can completely "bootstrap" belief in classical consistency (if not classical reasoning per se) using only intuitionistic reasoning. This was Gödel's original motivation for the $\neg\neg$-translation. $\endgroup$ – cody Apr 6 '15 at 21:51
  • $\begingroup$ What is meant by "may not have a normal form amenable to extracting a witness". Does it just semantically mean that these terms have bottom for semantics or does it mean something stranger? $\endgroup$ – Jake Apr 7 '15 at 0:59
  • 3
    $\begingroup$ @Jake: terms still have normal forms, but possibly not those you would expect: e.g. the proof of $A\vee \neg A$ is inr (fun x -> callcc(...)) even though $A$ may be true. $\endgroup$ – cody Apr 7 '15 at 2:42
  • $\begingroup$ Got it. Thanks! I'm still digesting parts of your answer. I'm not very familiar with the arithmetical hierarchy so it took me a bit more to process. $\endgroup$ – Jake Apr 7 '15 at 4:13
8
$\begingroup$

I agree with both Andrej's and Cody's answer. However, I think it is also worth mentioning why constructivists should care about control operators (call/cc).

These operators are usually connected to classical logic because when people looked at their typing rules (Felleisen, Griffin) they noticed that the types have the form of Peirce's Law or double-negation elimination ($\neg\neg P\vdash P$). Nevertheless, control operators were invented in the untyped setting of the Scheme programming language. Their purpose was to be able to enrich the programming language: instead of writing programs in continuation-passing style, one would be able to write programs in direct style using control operators.

One gain in using control operators in Proof Theory is the methodological one: instead of using a double-negation- and A-translation to extract programs from proofs of $\Pi^0_2$-theorems of Classical Arithmetic, one would use a control operator and perform direct rewriting normalization on the proof.

Another gain a constructivist should care about is that control operators show a way how to build a Curry-Howard extension of intuitionistic logic which is still constructive. For example, limiting the $P$ from the double negation elimination law to the $\Sigma^0_1$-class of formulas, allows to have a typed control operator that can prove for example Markov's Principle or the Double Negation Shift. These principles are usually not accepted by constructivists, but for hardly a good reason, since it is known that they do not destroy the Disjunction and Existence properties when added to intuitionistic logic.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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