UniMath
famous problems
Don't we need a proof that problems like the Goldbach conjecture are not decidable by an algorithm, before we assert this?
I'd say the burden of proof is rather on the other shoe: whoever wants to assert LEM or LPO (in a constructive sense) has to provide an algorithm/construction. In the particular case, whoever wants to assert “GC or not GC” (where GC is the Goldbach conjecture) has to prove one of the two disjuncts.
This strategy has some historical precedence via Brouwer's “weak counterexamples”. Brouwer also pointed out that if the particular open problem becomes solved, we could take another one.
But even so: We could point to some meta-theoretical results about the non-derivability of LPO as well.
Hmm? But here we say LPO is not constructive. That gives us the burden of proof.
@DanGrayson "Don't we need a proof that problems like the Goldbach conjecture are not decidable by an algorithm,"
We could use the halting problem instead of GC. Let P_e,n(k) = 1 if the e-th Turing machine halts on input n in at most k steps, and =0 otherwise. (This is well-defined since the condition is decidable, even primitive recursive.) Now assume we have a constructive proof of LPO, that is, an element t: LPO in the empty context. Then t(P_e,n) is an element of a sum, so equal to inl(...) if the e-th Turing machine does not halt on input n, and inr(...) otherwise. This would solve the halting problem.
The expository challenge is that "LPO is not constructively provable" is a metastatement and requires canonicity. One has to normalize t(P_e,n) for given numerals e and n. Probably best to have a remark, with the metastuff in a margin note. I will make a proposal and then we can discuss this.
@DanGrayson GC is an arithmetical statement with an ∀∃ prefix. It is a non-trivial result in logic that such sentences are constructively provable whenever they are provable in Peano Arithmetic. AFAIK there is no computational decidability question concerning GC. The big open problem is whether GC is provable in PA, or possibly in ZFC. (arithmetical ∀∃ statements provable in ZFC need not be constructively provable).
There is a generalization GC_k such that GC = GC_2: for all n there exists p>=n such that p and p+i are prime for some i <= k (`twin primes at distance at most k'). GC_k has been proved for certain (large) k. I don't know if such results are provable in PA, I guess there is a lot of analytic number theory involved, but we don't know if that is essential. If provable in PA, then G_k would be provable in Heyting's Aritmetic (= PA - LEM) as well.