Skip to Content.
Sympa Menu

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

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: roconnor AT theorem.ca
  • 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: Thu, 3 May 2018 11:20:01 -0700 (PDT)
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=roconnor AT theorem.ca; spf=PermError smtp.mailfrom=roconnor AT theorem.ca; spf=PermError smtp.helo=postmaster AT theorem.ca
  • Ironport-phdr: 9a23:69qzGR9sN485g/9uRHKM819IXTAuvvDOBiVQ1KB51OMcTK2v8tzYMVDF4r011RmVBd6ds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55Pebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRhHohikZKjA28mLZisJ+g61UvB2svAB/z5LObY2JKPZzZL3RcNUHTmRBRMZRUClBD5umb4sIE+UBOuBYr4/6p1sUtha+GQmsC/3oyj9SmHD22Lc23Pg7HgzAwQcuEdUOsHHOo9X0MqcfSe60zKjLzTXCd/NZxyry6InSfRw7pvGMR71wfdLLyUQuDQ/Kkk+fpIr4ND2WzuQAq3aX4/ZkWO61j2MqqRt9riaxyssykIXFm40YxkzC+C5k2og6P8e4R1R+YdO8EJtfqSWaN4xuT8M+Q2FnpiE6yqcYtp6+ZiQF1I4oywbea/yBbYeI/gruWPiNLTp8nn5ofLCyiwys/US+1OHwTNS43VlWoiZdl9nDrHEN1xjd6sidTft9+1+s2SyI1w/P7eFEJ0Y0la3BK5M63r4wloQcsUPZHiDonUX6lrOZeV889uiy9+vneqnmpoObN4Jslg7+Nb0ultWjDuQ8LwgBRHOW+f+81b3m5U32Wq9GjvwwkqnDsZDVP94XpqCjA1wd7oF24BGmSjyizd4wnH8dLVsDdgjUoZLuPgTUJ/v/C/G4mXywkDps3f3DeLboUcaFFWTKjLq0JeU10EVb0gdmlYkOtaIRMakIJbfIYmG0sdXZChEjNAntmbT7CNh6zI4bH2mGUPHAbPHi9GSQ7+dqGNGiIZcPsW+neeQl6vn0gHp/klZPJfD0j6tSU2ixG7FdG2vcYXfohY5bQ3sKsw0kQemsg1TQDzM=

On Thu, 3 May 2018,
roconnor AT theorem.ca
wrote:

But if PA were really inconsistent then this is probably what we expect to happen. If PA were really inconsistent, then from standard results in logic we know that it would be that case that epsilon_0 is not really an ordinal. In particular, there would exist an infinitely long decending chain of ordinal notations in Cantor normal form (https://en.wikipedia.org/wiki/Ordinal_arithmetic#Cantor_normal_form), and similarly there would exist a particular instance of Kirby and Paris's Hydra that is impossible to slay. So in a similar form, I expect there would be an infinitely descending sequence of substructures of a term of one of the inductive types used in defining PAconsistent. This would allow our structural recursion to go on forever.

Personally speaking I don't think that PA is inconsistent. I'm about as confident that there is no infinitely long descending chain of orndinal notations in Cantor normal form as I am that there is no infinitely long descening chain of natural numbers. And while I'm perhaps less confident that every function definable in Coq resulting in an inductive type is terminating, I have few doubts that the functions definable in the fragment of Coq used to define PAConsistent are all terminating.

I should add that the upshot of all this is that if CIC turns out to be unsound or inconsistent, it isn't going to be due to some hanywavy argument about presupposing the natural numbers exist. It's probably going to be due to presupposing some complex form of structural recursion is well-founded that isn't. (And, IMHO, that complex form of structural recursion is likley to involve the impredicativity of Prop somewhere.)

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



Archive powered by MHonArc 2.6.18.

Top of Page