<p>As you note, there is a possible constructive interpretation of classical logic in this sense. The fact that classical logic is <em>equiconsistent</em> with intuitionistic logic (say, Heyting Arithmetic) has been known for quite some time (already in 1933, e.g. <a href="http://en.wikipedia.org/wiki/Double-negation_translation" rel="nofollow noreferrer">Godel</a>) using a double negation translation.</p>

<p>By a more sophisticated argument, it can be shown that Peano Arithmetic is <em>conservative</em> 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 <a href="http://en.wikipedia.org/wiki/Continuation-passing_style" rel="nofollow noreferrer">CPS</a> transformation).</p>

<p>However this is <strong>not true</strong> 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 <em>philosophical</em> considerations: have we proven the existence of something, or not?</p>

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

<p>That being said, there is <em>a lot</em> 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 <a href="http://www.mscs.dal.ca/~selinger/papers/krivine.pdf" rel="nofollow noreferrer">here</a> for an overview.</p>

<p>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 (<a href="http://www.pps.univ-paris-diderot.fr/~krivine/articles/quote.pdf" rel="nofollow noreferrer">krivine</a>, <a href="http://www.jstor.org/discover/10.2307/2586854?sid=21105900141221&amp;uid=3739256&amp;uid=3739696&amp;uid=4&amp;uid=2129&amp;uid=70&amp;uid=2" rel="nofollow noreferrer">Berardi <em>et al.</em></a>)</p>

<p><strong>Edit:</strong> A very relevant question on mathoverflow appears here: <a href="https://mathoverflow.net/questions/29577/solved-sequent-calculus-as-programming-language">https://mathoverflow.net/questions/29577/solved-sequent-calculus-as-programming-language</a></p>

CC BY-SA 3.0
2015-04-06T21:46:12.330Z
Is this equiconsistency true constructively?
Geoffrey Irving
CC BY-SA 3.0
2015-04-06T21:51:55.177Z
@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.
cody
CC BY-SA 3.0
2015-04-07T00:59:30.570Z
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?
Jake
CC BY-SA 3.0
2015-04-07T02:42:23.743Z
@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.
cody
CC BY-SA 3.0
2015-04-07T04:13:41.403Z
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.
Jake
CC BY-SA 3.0
2015-04-06T14:42:30.833Z
2015-04-06T21:44:48.513Z
2017-04-13T12:57:54.777Z
cody
<p>I agree with both Andrej's and Cody's answer. However, I think it is also worth mentioning why constructivists <em>should</em> care about control operators (call/cc).</p>

<p>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.</p>

<p>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.</p>

<p>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 <a href="http://pauillac.inria.fr/~herbelin/articles/lics-Her10-markov+errata.pdf">Markov's Principle</a>  or the <a href="http://hal.inria.fr/hal-00647389">Double Negation Shift</a>. 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.</p>

CC BY-SA 3.0
2015-04-30T10:23:20.167Z
2015-04-30T10:23:20.167Z
Danko Ilik
<p>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.</p>

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

<ol>
<li>We provide a function $f$ which allegedly proves $\lnot p$. In reality $f$ is a bag of tricks.</li>
<li>If anyone ever applies $f$ to a proof of $p$, then $f$ unleashes <code>call/cc</code> 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$.</li>
</ol>

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

CC BY-SA 3.0
2015-04-07T00:47:11.743Z
Ah!! I think that is the kind thing I was looking for.
Jake
CC BY-SA 3.0
2015-04-06T21:29:49.797Z
2015-04-06T21:29:49.797Z
Andrej Bauer
<p>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? </p>

<p>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?</p>

<p>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?</p>

CC BY-SA 3.0
2015-04-06T10:42:35.997Z
[CPS](http://en.wikipedia.org/wiki/Continuation-passing_style), [call w/ cc](http://en.wikipedia.org/wiki/Call-with-current-continuation)
Kaveh
CC BY-SA 3.0
2015-04-06T10:43:39.197Z
Also [A new constructive logic: classic logic](http://dx.doi.org/10.1017/S0960129500001328).
Kaveh
<lo.logic><type-theory><lambda-calculus><proof-theory><constructive-mathematics>
Why do constructivists not seem to care too much about call/cc
Jake
# Why do constructivists not seem to care too much about call/cc

(Asked by: username_0 on 2015-04-06)

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?

**Tags:** lo.logic, type-theory, lambda-calculus, proof-theory, constructive-mathematics
> **Comments:**
> **username_1**: [CPS](http://en.wikipedia.org/wiki/Continuation-passing_style), [call w/ cc](http://en.wikipedia.org/wiki/Call-with-current-continuation)  
> **username_1**: Also [A new constructive logic: classic logic](http://dx.doi.org/10.1017/S0960129500001328).  

---

## 3 answers

### Answer by username_5 on 2015-04-06. Score: 21 | Accepted answer

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.)

> **Comments:**
> **username_0**: Ah!! I think that is the kind thing I was looking for.  

---

### Answer by username_2 on 2015-04-06. Score: 11

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](http://en.wikipedia.org/wiki/Double-negation_translation)) 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](http://en.wikipedia.org/wiki/Continuation-passing_style) 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](http://www.mscs.dal.ca/~selinger/papers/krivine.pdf) 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](http://www.pps.univ-paris-diderot.fr/~krivine/articles/quote.pdf), [Berardi *et al.*](http://www.jstor.org/discover/10.2307/2586854?sid=21105900141221&uid=3739256&uid=3739696&uid=4&uid=2129&uid=70&uid=2))

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

> **Comments:**
> **username_3**: Is this equiconsistency true constructively?  
> **username_2**: @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.  
> **username_0**: 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?  
> **username_2**: @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.  
> **username_0**: 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.  

---

### Answer by username_4 on 2015-04-30. Score: 9

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](http://pauillac.inria.fr/~herbelin/articles/lics-Her10-markov+errata.pdf) or the [Double Negation Shift](http://hal.inria.fr/hal-00647389). 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.


---

