The Coq mailing list

[Ken Kubota <mail AT kenkubota.de>]

This is exactly my position!

(I read this after writing the other email.)

All presentations of Goedel's theorems tacitly (implicitly) convey a specific philosophical approach without being conscious of the relativity of the approach as a whole when relying on a metatheory.

Philosophically, relying on a metatheory is even self-contradictory.

Kind regards,

Ken Kubota

____________________________________________________

Ken Kubota
https://doi.org/10.4444/100

Am 22.06.2021 um 11:11 schrieb Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>:

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.