The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Le jeu. 24 juin 2021 à 04:49, Marco Servetto
<marco.servetto AT gmail.com> a écrit :
>
> I'm more and more confused, but now I have an example that may help to
> clarify (and ends up hitting non-standard numbers too)
> -One of the typical examples for Propositions that may not be provable
> is termination of programs:
> -lets have "halt(p) = n" a partial function from program->nat, that returns 
> the
> number of steps the program p takes to terminate.
> - For all terminating programs, their execution trace is a valid and
> finite 'proof of termination'
> - For some programs, there is no proof of neither
>     Exists n: halt(p)=n       nor       not Exists n: halt(p)=n
> -Those programs do not terminate, otherwise we would have a
> termination proof using their execution trace.
>
> -Question1:  Where is the 'model' that defines 'truth' in my reasoning 
> above?

I can't tell but it is for sure the one you are in when you write
sentences like: "For some programs, there is no proof of bla". This
english statement corresponds to some formula (en existential one
here) to be interpreted in some theory, where there is a notion of "X
being a proof of Y" in ANOTHER (less expressive) theory.

My two cents.

P.