The Coq mailing list

[Peter LeFanu Lumsdaine <p.l.lumsdaine AT gmail.com>]

On Sun, Jun 20, 2021 at 10:36 PM Marco Servetto <marco.servetto AT gmail.com> wrote:

I'm quite ignorant and confused too.
In particular, what does it mean for a statement to be true without being provable?

Any time you’re talking about provability, you’re implicitly talking about provability in some object theory/formal system.

Any time you’re talking about truth of a statement of a formal language L, you’re implicitly talking about truth in some model M of L.

And any time you’re doing *anything* mathematical, you’re implicitly working in some meta-theory — which isn’t usually important to think about explicitly, but in contexts like this, it’s helpful.  And it’s *in that meta-theory* that we’re talking about provability in the object language, and truth in some model.

So when people say e.g. “the statement G is true without being provable”, it’s usually shorthand for something like: Working informally in our usual foundational system (e.g. ZFC or some form of type theory), we’ve shown that the statement G in the language of arithmetic holds in the natural numbers (the “standard model” of arithmetic), but is not provable in Peano arithmetic”.

The version relevant to this thread is talking about less clearly-established systems, so it’s a little ambiguous on how one might fill in the details.  One way would be: Write T_Coq for (some fragment of) the type theory of Coq. We’ve sketched a definition of some statement G in T_Coq.  Then, working in some foundational system (e.g. T_Coq plus enough stronger universe assumptions to model T_Coq), we claim that G holds in the standard model of T_Coq, but is not provable in T_Coq.

Another slightly different way to unpack it might be: We’ve sketched a definition of a statement G in L_arith, the language of arithmetic.  Then, working in some foundational system sufficient to discuss the model of L_arith in the natural numbers and provability in T_Coq, we claim: G holds in the natural numbers, but assuming T_Coq is consistent, the translation of G into T_Coq is not provable in T_Coq.

–p.