The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

To add to the question of the possible impact of classical axioms,
when a double-negation translation is possible, Dragalin-Friedman's
trick (*) shows that classical logic does not prove more functions
total than intuitionistic logic.

There are however cases where classical reasoning raises the
consistency strength. For instance, with an axiom of choice (with
"exists" in Prop) on top of a predicative system, classical logic
allows to lift the quantification over functions into a quantification
over predicates, hence providing impredicativity of Prop, which in
turn gives the totality of all functions of at least System F (even if
you started from, say, a system proving only the totality of functions
in System T). (Actually, what matters in choice here is only the
ability it gives to reify a predicate into a function to bool, so
unique choice is enough.)

Hoping it contributes to the discussion,

Hugo

(*) I don't know how much details to give as this is well-known from
many people on the list, but for the record, totality is a statement
of the form "forall m, exists p, T(e,m,p)" for T the Turing predicate
mentioned by Yannick and e the code of the function. A double-negation
translation (that is a continuation-passing-style translation when
seen from the programming point of view), gives
"forall m, ~~ exists p, T(e,m,p)" but then, for fixed m, one can
equally take "exists p, (e,n,m)" instead of False as return type, then
apply the identity continuation to go from
"(exists p, T(e,m,p) -> exists p, T(e,m,p)) -> exists p, T(e,m,p)"
to "exists p, T(e,m,p)".

On Fri, May 19, 2023 at 01:52:12PM -0400, Mario Carneiro wrote:
> 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
> 
>