The Coq mailing list

[roconnor AT theorem.ca]

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