The Coq mailing list

[José Manuel Rodriguez Caballero <josephcmac AT gmail.com>]

Emilio said
I am not sure what do you mean, the paper is very clear in that every
strategy is a winning strategy (Thm. 2.(i))

Read page 291 in the paper

Kirby, Laurie, and Jeff Paris. "Accessible independence results for Peano arithmetic." Bulletin of the London Mathematical Society 14.4 (1982): 285-293. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.107.3303&rep=rep1&type=pdf

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.

I'm just focus on CategoryTheory from UniMath in order to formalize in Coq my favorite model of arithmetic: 

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.

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.

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