The Coq mailing list

[Andrei Popescu <andrei.h.popescu AT gmail.com>]

Greetings,

I think a main problem with the formulations of Gödel's incompleteness
theorems from the literature is that they are either too concrete
(focussing on a particular setting, e.g., extensions of Peano
arithmetic within classic FOL) or too abstract (e.g., at the level of
provability logic). I've recently written a paper with Dmitriy Traytel
https://www.andreipopescu.uk/pdf/Goedel_JAR_2021.pdf
where we "distill" the amount of structure and properties needed for
being able to formulate these theorems. Particular attention is paid
to the notion of truth in a standard model and to the avoidance of
unnecessary assumptions (e.g., classical reasoning) about the object
logics.

Best wishes,
Andrei

On Tue, Jun 22, 2021 at 10:46 AM Vincent Semeria
<vincent.semeria AT gmail.com> wrote:
>
> > Truth is always relative to your meta-theory
> Thanks, that is clearer to me now.
>
> > I don't understand your insistence on non-standard numbers.
> Σ01 propositions are absolute, whereas Π01 propositions are not. In other 
> words, if a Σ01 proposition is satisfied by nat, then it is provable by 
> Robinson arithmetic, but this lemma does not hold for Π01 propositions. How 
> do we explain this failure for a Π01 proposition, (forall n:nat, P n), for 
> a decidable predicate P ? The way I see it, P would be true on all standard 
> numbers, and false on some non-standard numbers in some non-standard model.
>
> > I personally really hate the phrasing of Gödel's incompleteness theorem
> Quit hating or loving theorems, they do not deserve it :-)
>
> On Tue, Jun 22, 2021 at 11:11 AM Pierre-Marie Pédrot 
> <pierre-marie.pedrot AT inria.fr> wrote:
>>
>>
>>
>> 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
>>