The Coq mailing list

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

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

Theorem 2 (i) in Kirby & Paris' "Accessible independence results for Peano arithmetic" implicitly assumes that the hydra is an standard object (in the sense of Nelson's Set Theory).

Emilio said
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)

Here, we are again in the same problem as in the "proof of consistency of arithmetic". The natural numbers from ZFC, identified as ordinals, correspond to the standard model of first-order Peano arithmetic. 

There should be a justification for the privilege of the standard model over the non-standard models of PA. To say that the memory of a computer is a standard natural number is a valid argument in some cases, but maybe this number is so huge that it is better to think about is as non-standard. 

One argument against the standard model of PA is that non-standard models can be used in a more natural way to formalize applied mathematics, in particular Probability Theory, as Nelson did: https://web.math.princeton.edu/~nelson/books/rept.pdf 

I think that losing strategies for the Hydra game should be studied from of point of view of Nelson's Probability Theory. Maybe there are some interesting theorems about infinite Hydra games, with physical applications as approximations of physical phenomena. So this possibility should not be excluded.  

2018-05-05 6:14 GMT+02:00 <roconnor AT theorem.ca>:

On Fri, 4 May 2018, José Manuel Rodriguez Caballero wrote:

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...

The theorem is about the /essetial/ incompletness of theories, proving the essential incompleteness of a weaker theory is a logically stronger result.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''