coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [Metamath] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)

From: Emilio Jesús Gallego Arias <e AT x80.org>
To: José Manuel Rodriguez Caballero <josephcmac AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] [Metamath] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)
Date: Fri, 04 May 2018 22:17:58 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:NPegqhWYnvCPXrtEjQqOKGO3A/7V8LGtZVwlr6E/grcLSJyIuqrYYxaEt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/XlMJ+kaVboByvqRN9wIDbbo6aO+ZxcK7GYdMaXHBMUtpNWyFbAI6xaZYEAeobPeZfqonwv1QArR6/BQmoBePvzSdHiHvo0q0hyfwhChnJ0g06ENIKtHTbstr1NKAKXu2p1qnIzC/Mb+hL0jr69ofFaR8grPKQUb5qdsrR00YvGhrDg16NqoLlJyuY2vkOvmWY9eZsS/yjhm89pw1soDWj290ghpTHi44L0lzJ9iR0zJw0KNC6UkJ2ZcSoHIZMuy2GMYZ9X9ksTHtyuCkgz70LoZ67czYOyJQg3xPeZP+Kf5SS7hLkTuaRLi90hHNjeL2hmxa/6VWsx+7/W8WuzlpGsCtInsPRun0PyhDf8NWLR/Vj8ku53DaAzQHT6uVKIUAukqrbLoYszaArm5scsknPAjX6mELsjK+Zbkkk4PSn6/z7YrX6oZ+RL5N7igbnMqg3hsO/Bfk4PRMVUmiA+eW80aXj8lfjTLVLiP02iKjZv4rAKcQVvK7qSzNSh6Qk8Jf3Kj6gzdkc1UMAIEhEdw+KncDCMlvHJPT1F/D311arizpzx/vDN7bJDZDEL3yFm7DkK+VT8UlZnSc2zNRe4KV2B6qTO8XcU0v1udPfOTYjMgWvi7LqIMUtjsUZQ23ZUfzRC7/brVLdvrFnGOKLfoJA4G+sechg3ObniDoCoXFYeKCo2ZUNb3XpTOQ2ewOee3W+245dQ1dPhRI3SanRsHPHSSRaNiSiD/p64Ss0Wtr/UNXzA7u1ibnE5x+VW51bYmcXWEDcSTHvbYrWAvo=
Organization: X80 Heavy Industries

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

> There is such a losing strategy, but you need to take a certain initial
> segment of non-standard model of first-order Peano arithmetic, this is how
> Kirby and Paris proved the unprovability of Goodstein theorem in PA (page
> 291 of Accessible Independence Results for Peano Arithmetic).

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

The fact that you cannot prove it in P it doesn't mean that there exists
a losing strategy, but only that you can assume it.

E.

Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), (continued)
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), roconnor, 05/03/2018