The Coq mailing list

[Vincent Semeria <vincent.semeria AT gmail.com>]

Hi Pierre-Marie,

> More generally, by Gödel's theorem Π01 formulae are the worm in the apple, since they can encode the soundness of an arbitrarily complex problem.

Yes, this is what I am trying to understand about Coq. I am looking for a Π01 formula satisfied by nat (because from inside Coq all n:nat look standard) but not provable inside Coq (because there must be models of Coq with non standard numbers). I wonder whether Coq's consistency Con_Coq is such a formula. As you said, its InterpBool is a stuck term, so it cannot be proved equal true inside Coq. And by InterpBoolPropEquiv, its InterpProp cannot be proved inside Coq either.

I now think my mistake was trying to define truth, i.e. satisfaction by nat, inside Coq. This rather seems a meta-property, estalished by a meta-theory that observes Coq from the outside. Assuming the consistency of Coq from this meta-theory seems like assuming Con_Coq is satisfied by nat, is that correct ?

On Sat, Jun 19, 2021 at 2:25 PM Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

pOn 19/06/2021 10:22, Vincent Semeria wrote:
> Assuming LPO, I defined interpretations of arithmetical formulas in Coq,
> both in bool and in Prop, as shown below. I imagine that Coq's
> consistency is an arithmetical formula that would be interpreted to true
> by InterpBool.

No. Since you use a non-computable axiom you'll get a stuck term which
is neither true nor false. And you won't be able to prove that it is
indeed one of true or false, with the disjunction in the meta, i.e.
there is neither a proof of "InterpBool Φ = true" nor a proof of
"InterpBool Φ = false".

More generally, by Gödel's theorem Π01 formulae are the worm in the
apple, since they can encode the soundness of an arbitrarily complex
problem. Identifying Prop with bool is just moving the problem in
another place.

There are deep reasons why Gödel went into the study of constructive
logic after the discovery of incompleteness. Being able to compute is a
very good way to trust some statements.

PMP