The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 22/06/2021 10:25, Vincent Semeria wrote:
> I am looking for a Π01 formula satisfied by nat (because from inside 
> Coq all n:nat look standard)

What does that mean? Truth is always relative to your meta-theory so you
can't say much about "satisfaction in the meta" without explicitly
specifying the rules of your meta.

I personally really hate the phrasing of Gödel's incompleteness theorem
as "there are unprovable true statements" because it's implicitly
referring to the meta and confusing the reader about some grand and
transcendental notion of "truth" when this does not exist. Except maybe
when you're a Girard fan and / or some neo-Popperian believer, in which
case you may claim that Π01 formulae are falsifiable in the only
standard model we have, a.k.a. our local universe, and thus there is
some well-behaved notion of truth for these (but not above).

Incompleteness is really a boring theorem that can be phrased purely in
terms of provability without any irrelevant references to truth,
anchovies or hairy Schwarzschild black holes.

> but not provable inside Coq (because there must be models of Coq with
> non standard numbers).

I don't understand your insistence on non-standard numbers. You can have
perfectly standard numbers and weird properties about them, this happens
for presheaf models for instance. Since you have dependent elimination
you're outside of first-order logic and you're pretty much bound to have
numbers that behave at least internally like actual numbers.

But yes, Con_Coq is never going to be provable from within Coq, and if
your meta is strong enough to prove the consistency of the Coq theory
Con_Coq is going to be "true" in it. But this is begging the question,
by definition you're meta-assuming something stronger than "Coq is
consistent" for that.

PMP

Attachment: OpenPGP_signature
Description: OpenPGP digital signature