>If a proof can not be found isn't that like not halting, since the space of all theorems can never be exhaustively checked? That's correct, and the consequenc

>If a proof can not be found isn't that like not halting, since the space of all theorems can never be exhaustively checked? That's correct, and the consequence is that Coq will reject some valid recursive functions that always terminate. You can't describe the Collatz function in Coq and then ask the compiler if it terminates or not, for example. The compiler will reject the function, but it may still terminate - we don't know. The general reason for this is that Coq allows you to write recursive proofs (such as the induction in the article), and these recursive proofs need to have limited power - otherwise the proof system becomes inconsistent and it's possible to prove any statement. Since Coq proofs are just programs, if you could write a recursive non-terminating function, you could write such a function that lets you construct ill-founded proofs e.g. (* Non-terminating Coq function *) fix : (A -> A) -> A fix f := f (fix f) (* Use of that function as a Coq proof building tool *) my_false_statement : ⊥ my_false_statement := fix (fun x => x)