The Coq mailing list

[Mario Carneiro <di.gama AT gmail.com>]

Well, I think you need to distinguish between the computation of the bounding function fuel : N -> N and the constructiveness of the proof that forall x, f' (fuel x) x = S (f x) (borrowing the variables from Yannick's statement). If the termination proof relies on classical axioms, then of course there is no free lunch when transforming to this setting, those axioms have to be used somewhere. But it can well be the case that the upper bound on the computation "fuel" is reasonable but the proof that it terminates within that bound is hard or relies on additional axioms. (I would give an example at this point, but I can't think of any good examples of functions which require classical logic for their termination proof.)

Because classical axioms don't raise the consistency strength of the system, I would not expect it to be able to prove the existence of even faster growing functions, hence I would doubt you need classical axioms to construct the bounding function.

On Fri, May 19, 2023 at 1:34 PM Stefan Monnier <monnier AT iro.umontreal.ca> wrote:

> This doesn't sound quite correct. While Kleene's T tells you that for any
> terminating computation there is *some* bound for the fuel you need to
> compute the value, the bound itself might be quite large, and so you are

Side question: is it the case that such a (conservative) bound is always
computable, even for those functions whose termination proof relies on
classical axioms?


        Stefan