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 10:05:52 -0700 (PDT)
- Authentication-results: mail2-smtp-roc.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:2zYftxIHDtNgTYX9Q9mcpTZWNBhigK39O0sv0rFitYgRKv3xwZ3uMQTl6Ol3ixeRBMOHs6kC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwtFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhikHOTAn7W/YiM9+jKxVrx2uuxNy2IvUbJ2POfdkYq/QZ9cXSGxcVchRTSxBBYa8YpMVD+oGIelYqI/9p10JrRukHgSsGOPvxSFPhn/sw6I61v4tHh3c0wEmAtkAvnPUrNDvO6cTV+C41KfJzTTAb/NXwTfy9pXHchE7rv2WWrJwa8XRxVEgFwPEklWQqZHlMCiP2usRtGib6vJsVfiuhmI9tw5+uD6izdovhInRno8Z1EzI+CFjzIsxJ9C0UlB3bcC6HJdKqi2XOJd6T8U/SG9yoik60KcJuZujcSgK1psnwxnfZuSbc4iI/B3jU/yRLil9hH5/ZL2wnQ6+8UmmyuLiSsm5yEhGojZBn9XWsn0A1Qbf5taZRvdj5EutxDmC2xzL5uFBO080lK7bK5A7wr43k5oeqV7DHijql0Xxiq+WcEIk+vKz5uT7YrXpuJicN5VqhQH7KKghhtawDfwiMgcSR2ib5fi81Lr78ELlR7VKl+Q6nbXdsJDHPssWvbW5Ag9Q0oY78RmzFTam0NICnXkGNl1JYhyHj5K6c23Jdfv/FLK0h0mmuDZt3fHPeLP7UbvXKX2WirDqerB77FR01Ao+yspS4tRfA+JSaMnvU1P84YSLRiQyNBa5lr6+WYdNk7gGUGfKOZe3dabbsFuG/OUqerPeeI8YvyzwLr4u7qyw1CNrqRomZaCsmKAvRjWgBP0/eReFYXfrmNoEV2wD7FJnEb7azWaaWDsWXE6cGqIx4jZiUtC6DYrEXI2oxreIjnm2
** 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.''
- 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), Jose Manuel Rodriguez Caballero, 05/03/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Pierre Courtieu, 05/03/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/03/2018
- RE: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Soegtrop, Michael, 05/03/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/03/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Pierre Courtieu, 05/03/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Dominique Larchey-Wendling, 05/03/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/03/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Andrej Bauer, 05/03/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/03/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), roconnor, 05/03/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), roconnor, 05/03/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Andrej Bauer, 05/03/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Ken Kubota, 05/03/2018
- Message not available
- Message not available
- Message not available
- Message not available
- Re: [Coq-Club] [Metamath] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Ken Kubota, 05/03/2018
- Re: [Coq-Club] [Metamath] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/04/2018
- Re: [Coq-Club] [Metamath] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Emilio Jesús Gallego Arias, 05/04/2018
- Re: [Coq-Club] [Metamath] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/04/2018
- Re: [Coq-Club] [Metamath] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Emilio Jesús Gallego Arias, 05/05/2018
- Re: [Coq-Club] [Metamath] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), roconnor, 05/05/2018
- Re: [Coq-Club] [Metamath] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/05/2018
Archive powered by MHonArc 2.6.18.