coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)
Chronological Thread
- From: José Manuel Rodriguez Caballero <josephcmac AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)
- Date: Wed, 2 May 2018 12:38:53 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=josephcmac AT gmail.com; spf=Pass smtp.mailfrom=josephcmac AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f179.google.com
- Ironport-phdr: 9a23:Ti9x4BHnSMfVfXHyMKWRwJ1GYnF86YWxBRYc798ds5kLTJ78osiwAkXT6L1XgUPTWs2DsrQY07GQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDSwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KODw38G/XhMJ+j79Vrgy9qBFk2YHYfJuYOeBicq/Bf94XQ3dKUMZLVyxGB4Oxd48BD+0aPeFCt4bzoEEBrR2jBQayAOPg0iNGhnjr0q0g0uQhHhzG0xIhHt0Wrnnbts76O70WUeCx0qbI1zLDZO5R1Df/74jIaQ4uoemMXb1sdMre01UgGhjKjlWVs4PlPjeV2v4RvGic6uptTOSigHMkpQFpujWj2Nsgh43Tio8Wyl3I7zh1zYcoKdGiVUJ2Y9qpHZ1NvC+ALYR2WNktQ2RwtSY61LIGvZm7cTAPyJs9xh7fb+WLcoiG4x7/TeqRLyp0iXBhdb6liBay9k+gyuL4VsaqylpFsi1FktzUunAM0Rzc9NSHR+Nj8ku93TuDzQPe5+FeLUwplKfXNoQtzqMym5cXqUjDGzX5mETyjK+YbEUk/e2o5vzlYrXhvZ+TKZd0igHiPaQrgMOwHf81MgcLX2eB+OS80Kfv8lH+QLVPlvE2iLXWsIjGJcQHoa60GxNa0oE66xqmEzim1MkYkmIcIVJeeBOHipDpNEvULPD5C/e/mVWsny1xy/DIJL2ySqnKe3PEifLqeat3w09a0gs6i95FtLxODbRUAvXo23jUvdrFAxsOCQu42efoFdhv4agXU2uLBqKDN+uGs1iT6/ovKOyFb6cavT/8L74u4Pu43ixxokMUYaT8hchfU3u/BPkzexzIM0qpuc8IFCIxhiR7SeXrjFOYVjsKPiS9Wqs94ncwD4f0VN6fFLDou6SI2WKAJrMTfnpPUwneHnLhdoHCUPAJOnrLf51R1wccXL3kcLcPkBGjsAiglehiJ+vQvzwH7dftjYckoeLUkh42+Hp/CMHPi2w=
Dear Emilio,
Thank you very much by the information that Voevodsky retracted its conjecture that PA is inconsistent (it would be wonderful to find a video or a manuscript of him in order to know the context). Nevertheless, as far as I know, he didn't retracted his second claim: "CIC is not cleaned defined, because it is an initial model of a theory which itself requires natural numbers to be specified".
Concerning you claim that "consistency of PA is a well-established fact", according to your two arguments I only can deduce that "consistency of PA is a well-established belief". First, "the termination of the finitary Hydra game" is not true for certain initial segment of PA (this is precisely the theorem that I'm trying to mechanize in Coq right now). You can prove "the termination of the finitary Hydra game" in ZFC as well as in CiC, but that is more, not less. Second, the argument "if you had to bet all your current and future state to either..." can be used to "prove" any conjecture, for example the 3x+1 conjecture.
With respect to you question
"About 'proving in Coq' assumptions from CiC in a fancy way, well, that's
what logic is, isn't it?"
My answer is that in foundation of mathematics you go from weak assumptions to strong assumptions. To do it the other way around is Begging the Question. For example, Riemann "proved" Prime Number Theorem, but he just assumed Riemann Hypothesis.
CiC is wonderful for many branches of mathematics, but there are some foundational problems when it is applied as an autonomous foundation of mathematics.
Best Regards,
José M.
Emilio says:It is my understanding that his views were influenced by Edward Nelson
which were quite radical AFAICT. IIRC, at some point Nelson wrote a
"theorem prover" and claimed to have found a proof of "PA ⊢ ⊥", but it
seems it was not correct.Nelson was not as nutty as this might suggest. He took the view that natural number induction is not predicative, because one quantifies over all natural numbers. In his classic monograph "Predicative Arithmetic" he discusses formal systems that are predicative in his sense. IIRC such systems do not prove totality of exponentiation, so Godel's Theorem may be unprovable.--Randy
- [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Jose Manuel Rodriguez Caballero, 05/01/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Andrej Bauer, 05/01/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Matej Košík, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Pierre-Yves Strub, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Emilio Jesús Gallego Arias, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Emilio Jesús Gallego Arias, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), R. Pollack, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Arthur Azevedo de Amorim, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Emilio Jesús Gallego Arias, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Emilio Jesús Gallego Arias, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Siddharth Bhat, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Emilio Jesús Gallego Arias, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Siddharth Bhat, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), R. Pollack, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Andrej Bauer, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Adam Chlipala, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Jose Manuel Rodriguez Caballero, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Adam Chlipala, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Pierre Courtieu, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Jose Manuel Rodriguez Caballero, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Pierre-Yves Strub, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
Archive powered by MHonArc 2.6.18.