The Coq mailing list

[roconnor AT theorem.ca]

> ** How is this useful? **

Since others on this list seem to be interested in this thread, let's talk 
about what having proved the "consistency of PA" in Coq entails. 
Hopefully I've established by now that proving the "consitency of PA" in 
Coq does not directly preclude the possiblity of also proving the 
"inconsistency of PA" in Coq.  That can only be concluded if we 
additionally assume Coq is consistent.

Let's ask the question, what if PA were really inconsistent?  What would 
the consequences of that be?  As a former student of logic, I've spend my 
fair share of time thinking about this question.

What would it mean for PA to really be inconsistent?  It would mean we 
could write down a deduction, using a classical Hilbert style deduction 
system, from the logical axioms and the axioms of PA, and conclude with 
"0=1".  In principle we should be able, literally, to write this deduction 
on a scroll of paper.  It might be long, but it must have a finite 
representation.  Of course having a deduction of "0=1" means we can extend 
this deduction to conclude any formula we want.  In particular, we can 
conclude "¬x_0=x_0" in our Hilbert deduction system, and again this entire 
deduction would be finitely reprsentable; we could write it out on a 
scroll or type it into a computer as a document.

Since we would be able to literally type this deduction into a computer 
then we might as well write the deduction in Coq as a closed, normal term 
of the inductive family Prf @ 
https://github.com/coq-contribs/goedel/blob/a232fade79805c9339aaa4ec2c641723095e2c4e/folProof.v#L68-L100. 
Since we would have a real honest deduction, I see no reason why Coq would 
refuse to type check this particular method encoding of our deduction.

With this value of the Prf family in hand, we could construct a value of 
type (SysPrf PA (notH (equalH (var 0) (var 0))) (see 
https://github.com/coq-contribs/goedel/blob/a232fade79805c9339aaa4ec2c641723095e2c4e/folProof.v#L102-L105) 
by creating a suitable list of the particular instances of the non-logical 
axioms that were required for our proof of (notH (equalH (var 0) (var 
0))), call this list of axioms required "Axm", and establish that every 
such non-logical axiom is an axiom of PA.  This is established by building 
a function of type (forall g : Formula, In g Axm -> mem _ PA g) which is 
required by our definition of SysPrf.  This function whould be easy to 
build as a finite case analysis over the argument of (In g Axm) type and 
deducing that each element of Axm sasitifies the requirements needed to be 
an axiom of PA (the requirements to be an axiom of PA are defined @ 
https://github.com/coq-contribs/goedel/blob/a232fade79805c9339aaa4ec2c641723095e2c4e/PA.v#L12-L40).

(It's notable that only a finite number of instances of PA's axiom schema 
of induction are ever required for any single particular deduction, 
including the deduction of a contradtion.  This is the compactness theorem 
of first-order logic (https://en.wikipedia.org/wiki/Compactness_theorem).)

Having our hypothetial value of type (SysPrf PA (notH (equalH (var 0) (var 
0))) in hand, let's turn to our existing and very much non-hypothetical 
value PAconsistent of type (Consistent LNT PA) from 
https://github.com/coq-contribs/goedel/blob/master/PAconsistent.v#L18

Looking at the defintion of (Consistent) from 
https://github.com/coq-contribs/goedel/blob/master/folProof.v#L109, we see 
that PAconsistent is a pair of value f of type Formula, paired with a 
function from type (SysPrf T f) to the type False.  If we compute, or 
inspect, the defintiion of PAconsistent, we see that the first component 
of this pair is the formula (notH (equalH (var 0) (var 0))).  This means 
the second compontent of this pair is a funtion from the type (SysPrf T 
(notH (equalH (var 0) (var 0)))) to the type False.

Let me reiterate that this function is very much not hypothetical.  It has 
been very rigorously defined and it really exists in as much as any 
software exists.

If PA were really inconsistent then we could create an equally real 
argument to this function of type (SysPrf T (notH (equalH (var 0) (var 
0)))) as I described above.  If that is the case then we can apply our 
really existing function to this hypothetically existing argument and we 
get a value whose type is False.

Okay, so we would have just proven the inconsitency of Coq.  What's the 
big deal?  Everyone expects that if PA is inconsistent, then Coq would be 
as well.  If we were working in classical set theory, such as ZFC, this 
would appear to be the end of the story.  But with type theory, the story 
isn't over yet, and the following is one of the things that I find most 
exciting and compelling about type theory over traditional classical set 
theory.

We have a value of type False, and this value is a function applied to an 
argument.  We have a beta-redex!!  So we can apply beta reduction to it, 
which will produce further redexes and we can keep reducing those, and so 
on.  Let's turn the crank on this!

Coq is supposed to satisify a normalization property which states that 
there always exists a path of reductions that will terminate with a term 
that has no more redexes, a so-called normal form.  This property in turn 
entails a canonicity property whereby in the empty context a term in 
normal form must begin with a constructor of its type.

If PA were inconsistent then we have seen that we can construct a term of 
type False in the empty context.  If Coq were normalizing then this term 
must reduce to a normal form that begins with a constructor.  But the type 
False has no constructors, so that would be impossible!  If this situation 
occurs, it must be the case that something goes wrong when we try to 
normalize our term of type False.  What are the things that could possibly 
go wrong?

Perhaps, somehow the reduction process ends without being in canonical 
form.  This can easily happen in Coq when Axioms are used (such as 
functional extensionality), but I'm fairly certain I avoid any use of 
extra Axioms in my construction of PAconsistent (this fact can be verified 
by using the coqchk program).  And we don't require using any Axioms to 
construct our hypothetical value of type (SysPrf PA (notH (equalH (var 0) 
(var 0))), so Axioms are out.

Well-typed terms in Coq are designed so that it is only possible to match 
up eliminators with values of the corresponing type.  As long as 
well-typedness is maintained by reductions, it shouldn't be possible to 
get stuck trying to do case analysis over a value of the wrong type. 
There are some sticky issues related to CoInductive types and the above 
"subject-reduction" property not being maintained.  But, my construction 
of PAconsistent doesn't use CoInductive types anywhere and neither does 
our hypothetical value of type (SysPrf PA (notH (equalH (var 0) (var 0))).

The type theory of Coq has been carefully crafted to avoid reductions 
getting stuck, so I think it is very unlikely that that will be the 
problem.  What is far more likely is that, if this situation were to 
occur, as we evaluate, more and more redexes always pop up, and no matter 
what strategy we try we always find that ever more redexes that appear.

One might say that this would be like trying to fight a Hydra, where every 
time you cut off one head (evaluate a redex), a whole new group of heads 
(redexs) grow back.

Coq's type theory is supposed to be designed such that this sort of 
infinite evaluation to never happens under a suitable strategy.  All fixed 
point recurion is structural.  Every recursive call is made on a term that 
is smaller than the orignal call by virtue of being required to be a 
substructure of the orignal argument to the fixed point.  One would think 
this would ensure the eventual termination of evaluation of any fixed 
point.  It's as if when a Hydra regrows a group of heads, they only regrow 
at a somewhat lower level.

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.

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