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?
Why do constructivists not seem to care too much about call/cc
lo.logic;type theory;lambda calculus;proof theory;constructive mathematics
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:We provide a function $f$ which allegedly proves $\lnot p$. In reality $f$ is a bag of tricks.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.)