On the intuitionism page at Stanford Encyclopedia of Philosophy (SEP), it's said in Section 3.3 that

Because of the finiteness of a natural number in contrast to, for example, a real number, many arithmetical statements of a finite nature that are true in classical mathematics are so in intuitionism as well. For example, in intuitionism every natural number has a prime factorization; there exist computably enumerable sets that are not computable...

This uncomputability result must necessarily use the halting problem, whose uncomputability is proved unconstructively, as it relies on the law of the excluded middle: TM $M$ of input $\langle M\rangle$ either halts or not. This is not constructive because it might be impossible to know whether the TM runs forever. If you can prove for every case that the TM runs forever when it indeed does, then the collection of such proofs results in an algorithm that decides haltingness. So this proof is not constructive. But SEP says that intuitionists accept it! Isn't intuitionism a constructive theory? Or are there other constructive proofs of the halting problem that I don't know?

  • $\begingroup$ @LukeMathieson Thanks for the link and your answer there. OK, I admit that I didn’t read the quote carefully enough. But what I have in mind is to exhibit a specific language that’s undecidable. Do intuitionists accept that one can define a specific language that’s undecidable? Thanks for the chance to clarify my question. $\endgroup$ – Zirui Wang Oct 30 '19 at 12:28
  • $\begingroup$ To mash some of the information from the other question together, constructivist logic is okay with proofs along the lines of "assuming $\phi$ gives a contradiction, so $\neg \phi$" (we still have $\neg(\phi \wedge \neg \phi)$, even if we don't have $\phi \vee \neg \phi$). So the basic diagonalisation structure is fine. Then the link in the first answer gives an example of a specific language: mail.haskell.org/pipermail/haskell-cafe/2003-May/004343.html $\endgroup$ – Luke Mathieson Oct 30 '19 at 12:54
  • $\begingroup$ The language of codes for halting Turing machines is a specific language that's undecidable. Also, by the way 'assuming $\phi$ gives a contradiction' is essentially the definition of $¬\phi$ intuitionistically. The fancier principle (non-contradiction) is derived from that and other rules. $\endgroup$ – Dan Doel Oct 30 '19 at 12:55
  • 2
    $\begingroup$ You are making a few assumption here. You claim that we have to use the halting problem, but one could use something else. You claim that any proof must use the fact that a TM halts or not, you provide no support for that: even if the proof you know uses the excluded middle, there might be an alternative proof which does not. Indeed, to constructively prove $\lnot p$, we can assume $p$ and reach a contradiction. Assuming that there is a TM solving some problem H and then reaching a contradiction (constructively), would constructively prove that H is undecidable. No excluded middle required. $\endgroup$ – chi Oct 30 '19 at 17:50
  • 3
    $\begingroup$ I would just like to say that THE USUAL PROOF THAT THE HALTING ORACLE DOES NOT EXIST IS CONSTRUCTIVELY VALID. THERE IS NO APPLICATION OF EXCLUDED MIDDLE IN IT. $\endgroup$ – Andrej Bauer Oct 31 '19 at 16:33