The Coq mailing list

[Emilio Jesús Gallego Arias <e AT x80.org>]

José Manuel Rodriguez Caballero 
<josephcmac AT gmail.com>
 writes:

> In other words, he used the type "nat" as a model of PA. So, in order to
> prove that natural numbers satisfy the principle of complete induction from
> PA, he used the above-mentioned induction definition scheme which allows
> you to do things parametrized by natural numbers from the beginning.

> I do not say that "mechanization" of theorems from Model Theory is not
> possible in Coq. What I say is that, from the point of view of foundation
> of mathematics, we need to be open to the possibility that maybe some
> people are just "proving in Coq" assumptions from CiC in a fancy way. I use
> the example of O'Connor, because I tried to do a similar project in Model
> Theory, but I'm not convinced of the efficacy of this approach from a
> mathematical point of view.

As far as I can see this is just way a remove the assumption, in a sense
the proof is:

"Assume M a model of PA, then Theorem"

Of course, if you can provide a model M inside the logic of Coq your
theorem is "stronger" as you have removed an assumption.

About "proving in Coq" assumptions from CiC in a fancy way, well, that's
what logic is, isn't it?

It is good practice in theory to try to remove assumptions when possible
(*), as we assume the logical theory of Coq to be consistent, but of
course you can prove your lemmas abstractly if that's what you want.

E.

p.d: I sometimes see students writing { Pre } Prog { Post } where
actually Pre won't be ever satisfied so indeed building a model for your
assumptions is a good sanity check.