The Coq mailing list

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

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

> Read page 291 in the paper
>
> There is an initial segment M of first-order Peano Arithmetic (denoted just
> P in this paper) such that no interval [1, y] is omega_c-large.
> Furthermore, it says how to define such a model, formalizing in Peano
> arithmetic a certain theorem about rapidly increasing functions due to
> Ketonen and Solovay  (it can be done in O'Connor simulation of first-order
> Peano arithmetic). You suppose that every Goodstein sequence terminates and
> you deduce from this fact that there is an interval [1, y] which is omega_c
> - large. Because we are in classical logic, it follows that there exists a
> Goodstein sequence which does not terminate.

Sorry if I am bit obstruse as I barely got out of a day-long meeting and
have to do some urgent stuff so I write in a hurry, but doesn't this
just show that "P + ¬Con(P)" has a model?

What problem do you have with Theorem 2.(i) in the paper you cite?

You claimed "there is such a losing strategy" and indeed there exists
one due to oddities of non-standard models (which is sometimes a high
price to pay, as others have said, for keeping compactness)

But this doesn't mean you can prove that there exists a losing strategy,
in fact, quite the contrary it is possible to prove in ZFC that all
strategies are winning strategies.

Let me remark that I explicitly asked to interpreted the Hydra game as a
computational, or psychical device.

Let's take it this way, should you be able to prove that the following
program terminates:                [example due to Michael J. O'Donnell]

while(a > 0) a--;

Well, if is interpreted in a non-standard model you may find trouble,
won't you?

> Moerdijk, Ieke. "A model for intuitionistic non-standard arithmetic."
> (1995). http://repository.ubn.ru.nl/bitstream/handle/2066/
> 129065/129065.pdf?sequence=1
>
> I'm trying to formalize in UniMath (using Coq) the unprovability of
> Goodstein's theorem in higher-order Heyting arithmetic, following a topos
> theoretic approach. My motivation to read Russell's paper was to try to do
> it in his first-order system, but I think that the first-order logic is not
> essential in Moerdijk's approach. Of course, it will be not the original
> Kirby & Paris theorem, but a free version in Coq.

That's very interesting, but may not be pain-free. You are totally right
that CIC is a very syntactic system and thus it may not map well to some
key notions on categorical logic. And also you are right about the
different trade-offs involved in the formalization of model theory and
logic. Coq in a sense gives you a "model" for free. So you can trivially
prove the consistency of PA in Coq just by building nat and a few
trivial proofs.

> By the way, Emilio, do you think that the incompleteness of arithmetic can
> be mechanized in Coq without simulating first-order logic? I think that you
> can repeat the Gödel-Rosser argument by coding CiC by Gödel numbers. I do
> not see why first-order logic is essential here.

That's a very good point, but somehow you need to reflect the syntax of
Coq terms; I am not sure what the best choice would be here, I guess
that Russell can say more as I vaguely recall reading on some paper of
his "I would pick a different syntax representation would I start again".

In terms of embedding to Coq, FOL or System-T may be fine; however
binders turn out to be a pain and Paulson recently used Hereditarily
Finite Sets plus Nominal Isabelle which seems like very cool stuff.

> If higher-order arithmetic is incomplete, then in particular first-order
> arithmetic is incomplete too. I wonder if there could be some
> simplifications...

I have no idea, but looks like a very interesting question; maybe
someone more expert knows more?.

For consistency, it is very easy to take advantage of the
meta-theoretical property, as Coq is a quite strong system, but for
incompleteness...

E.