MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Assume we have a proof term of the form $(a^{A\rightarrow^c B\rightarrow^{nc} C}b^Ac^B)^C$, where $c$ is classical (that is, contains free instances of duplex negatio affirmat). The extracted term would not depend on $c$ anymore, so in fact, from a pragmatic point of view, one could accept this proof as "constructive" in the sense that the computational content of it is constructive, and only additional assertions (which are not computationally relevant) and which hence do only have to be "true", but not "constructive", are non-constructive.

My question now is, to what extent the system becomes stronger, when allowing this. Of course, it is trivial to give examples where this method is stronger, for example, as $B$ is arbitrary, we can just set $B$ to something that is only classically provable. But I did not find any example where this strengthening is relevant for the algorithm to work, that is, where it actually makes sense to allow classical reasoning, and the additional assertion $B$ cannot just be dropped.

Edit: $\rightarrow^c$ and $\rightarrow^{nc}$ mean computational ad non-computational implication, respectively. That is, the type $\tau(A\rightarrow^c B)=\tau(A)\rightarrow\tau(B)$, while $\tau(A\rightarrow^{nc}B)=\tau(B)$. In there can be found a definition of this, they write $\rightarrow^U$ for $\rightarrow^{nc}$. I hope this clears up the notation.

Edit 2: To make it clearer: Assume I have a list-sorting algorithm $sort_R^{\forall_{l^{L_\alpha}} (\forall_{a^\alpha}\forall_{b^\alpha}. Rab\vee\lnot Rab)\rightarrow^c \forall_{a^\alpha} Raa \rightarrow^{nc} (\forall_{a^\alpha,b^\alpha,c^\alpha}. Rab\rightarrow^{nc}Rbc\rightarrow^{nc}Rac)\rightarrow^{nc}\exists_{m^{L_\alpha}}.X(m,l)}$ where $X(m,l)$ shall stand for $m$ being sorted with respect to $R$ and containing the same elements as $l$ (It would not become clearer if I wrote that part out). The type signature sais that it needs a function deciding whether $Rab$ holds for $a$ and $b$, but it does not need a realizer of $\forall_a Raa$, nor does it need a realizer of transitivity - it just needs to know that $R$ is reflexive and transitive, but the parts where this is proved will never be called in the extracted term. So in theory, we could as well allow that these are proven classically rather than intuitionistically, since we do not need any realizers. Even worse, we might allow them to use some strong version of Choice, as long as we "believe" choice. My question is whether somebody can give an example where this is actually relevant. I tried to construct one using the given example, but I failed so far.

share|cite|improve this question
Sorry, can't follow. You're writing down proof terms? What are those c's and nc's on the arrows? I think it would help if you used standard first-order logic notation. – Andrej Bauer Jan 6 '12 at 21:05
Ok, I edited it, is it clearer now? – Christoph-Simon Senjak Jan 6 '12 at 22:32
Yes thanks, you should have said "minilog" or "Schwichtenberg" at the very beginning. Say hi to prof. Schwichtenberg! – Andrej Bauer Jan 7 '12 at 7:42
I am not sure I really understand your question, but I think you want to look up independence of premise,, and wonder why the premise cannot be moved when it is classical. – Andrej Bauer Jan 7 '12 at 7:51
I am not currently working for Schwichtenberg. This is just something that interests me. However, I do not see a deeper connection to the principle of independence of premise. – Christoph-Simon Senjak Jan 7 '12 at 22:02

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.