Undecidability of constructive provability

Question

The paper A Lightweight Double-negation Translation states "However, as not all classical theorems are provable constructively – this question is even undecidable..." Can someone provide me with a proof/reference to proof of undecidability of constructive provability of classical theorems?

Answer 1

For a fixed Turing machine $T$, there is a formula $\phi_T(n)$ in HA (the constructive analogue of PA), that can be computed from a description of $T$, that expresses that $T$ has halted after being run for $n$ steps. Then whether or not $\psi_T := \exists n(\phi_T(n)) \lor \forall n(\neg\phi_T(n))$ is constructively provable is undecidable, although this is obviously a classical theorem. Let us spell out why.

HA has both the disjunction property and the existence property, which means that if $\psi_T$ is a theorem, then either $\exists n (\phi_T(n))$ or $\forall n(\neg \phi_T(n))$ has to be a theorem of it; and in the former case, that means that there must be a term (so: a numeral) $\bar n$ such that $\phi_T(\bar n)$ is a theorem. Suppose you could decide whether or not $\psi_T$ is constructively provable. If it is constructively provable, then you can start looking for proofs of either $\phi_T(\bar n)$ for numerals $\bar n$, or $\forall n(\neg \phi_T(n))$; regardless of which one you find, you have decided whether or not $T$ halts. If $\psi_T$ is not constructively provable, then clearly $T$ cannot halt, because any numeral greater than its halting time would witness $\exists n(\phi_T(n))$.