[lmm]

But we wouldn't want to just leave such a theorem prover running indefinitely. Far more practical to have it check all possible proofs of length up to n (trivial to do in a total language), or at most run it for a particular number of days, months or years. At some point you do end the experiment.

[tom_mellior]

Sure. You usually run the prover with a timeout. The point is, this is a practical example of running a program where you cannot predict whether it will "work" or not. Additionally, when you reach the timeout, you will not have gained any information, i.e., the process is not "productive" in the sense discussed above.

Edit: Can't reply to your reply. Interesting. Yes, true, "there is no proof of length < N" is some information, but it's not information that tells you anything about the provability of your formula. It's not productive information. You can keep trying, but you won't be able to overturn the semidecidability of first-order logic in a Hacker News comment thread.

[lmm]

If the prover simply went into an infinite loop while checking the first proof candidate and never got as far as checking the second one, would it be working correctly? I would consider such a prover not useful, and a useful prover would be one that told me something when reaching the timeout, such as that there were no proofs for the given theorem shorter than a certain length.

[thamster]

This is handled in university CS algorithms courses. In such a case, dovetailing or interleaving the execution of the TM on the input would be used. Sipser pp. 150–152 https://courses.engr.illinois.edu/cs373/sp2009/lectures/old/...