2

In general when trying to solve an excersise, or construct a proof, I always find myself looking at what strategy should I take to complete the proof. Many times I try to solve the excercise with a constructive proof, and since it is not working out, I end up trying with an absurd-type argument. A couple of days ago, I read a question asking if there was any way to exhibit a constructive proof for a certain theorem regarding continuity, and someone answered that there was no way to give such a proof if working in ZFC.

My question is, how can you know, if you can give a constructive proof or not? Is there any way to give a constructive proof of this question?

Joaquin Liniado
  • 3,840
  • Please tell us what that particular theorem is, or we won't be able to tell you. Start with the specific before looking for a general rule. – Thomas Andrews Jun 08 '15 at 22:31
  • (There's an interesting theorem in strong constructive mathematics that all functions are continuous, so it is impossible without using non-constructive means to define a function that is not continuous.) (Note that $x<0$ is a non-constructive test, since there are real numbers in constructive mathematics for which this decision is undecidable.) – Thomas Andrews Jun 08 '15 at 22:36
  • http://math.stackexchange.com/questions/1312873/show-constructively-that-the-sequence-definition-of-continuity-implies-the-epsil. That's the question I was reffering to. However my question is in general. Given a theorem, (no one in particular), is there any way to know (not necessairily constructively) if there is a constructive proof for the theorem? – Joaquin Liniado Jun 08 '15 at 22:41

1 Answers1

2

Given a theorem, (no one in particular), is there any way to know (not necessarily constructively) if there is a constructive proof for the theorem?

No, there is no such method.

First, there is no formal notion of "constructive proof" in general - there are just particular constructive proof systems. So the best you could hope for is a way to tell if a statement is provable in some particular constructive system.

But even that is impossible, because of the undecidability of the halting problem. This asks for an algorithm to determine, given a Turing machine, whether the Turing machine will eventually halt after it is started. Now, a Turing machine halts if and only if there is a constructive proof that the machine halts. If it halts, we can list out the execution step by step to prove that it halts -- and the converse also holds. This proof method will work in any sufficiently strong constructive proof system.

So, if there was a way to tell whether a given theorem had a constructive proof, in a sufficiently strong constructive system, then there would be a way to tell whether a given Turing machine halts. We know that is not the case.

Carl Mummert
  • 81,604
  • Surely that argujment doesn't work? Given the proof system, there is a Turing machine that enumerates the proofs of the system and halts if it finds a proof of $x \neq x$. This machine halts iff the system is inconsistent. By the incompleteness theorem, if it is sufficiently strong and consistent, the machine does not halt, but as the system can't prove its own consistency, it can't prove that. – Rob Arthan Jun 09 '15 at 16:53
  • Exactly - the machine does not halt, and the system does not prove that the machine halts. My claim was that for a sufficiently strong (and sound) constructive system, the system will prove that the machine halts if and only if the machine really does halt (call this property H). So if we could decide which sentences are provable in the system, we could decide which machines halt. For my purposes, it is irrelevant if the system can prove that any machine does not halt. Many consistent systems do have property (H), for example Heyting arithmetic or Peano arithmetic. – Carl Mummert Jun 09 '15 at 18:30
  • This part of your answer is extremely unclear: "a Turing machine halts if and only if there is a constructive proof that the machine halts. If it halts, we can list out the execution step by step to prove that it halts -- and the converse also holds." Constructive proof in what system?? Converse of what?? Please clarify. – Rob Arthan Jun 09 '15 at 20:11
  • As the next sentence says: this proof method will work in any sufficiently strong constructive proof system. As for the converse that also holds, the converse of "if it halts, we can list out the execution step by step to prove it halts" also holds: "if we can list out the execution step by step to prove a machine halts, then the machine halts". – Carl Mummert Jun 09 '15 at 20:34