Qea. If this were normal science, the proof that P is inconsistent could be written up rather quickly. But since this work calls for a paradigm shift in mathematics, it is essential that all details be developed fully. At present, I have written just over 100 pages beginning this. The current version is posted as a work in progress at http://www.math.princeton.edu/~nelson/books.html, and the book will be updated from time to time. The proofs are automatically checked by a program I devised called qea (for quod est absurdum, since all the proofs are indirect). Most proof checkers require one to trust that the program is correct, something that is notoriously difficult to verify. But qea, from a very concise input, prints out full proofs that a mathematician can quickly check simply by inspection. To date there are 733 axioms, definitions, and theorems, and qea checked the work in 93 seconds of user time, writing to files 23 megabytes of full proofs that are available from hyperlinks in the book.
It looks like Qea does verify the proof and generates human-readable text. In that case, my trust in it or Coq would be based on their relative size adjusted for amount of testing these tools received. Coq uses a non-trivially unique proof system (calclulus of coinductive constructions, if I remember correctly), which counts against it. Did anything look what proof system Qea uses?
Yeah, I’ve heard about this “notorious difficulty” in verifying proof checkers before, and I don’t understand what it could mean. Humans are way more unverifiable.
I bet the real purpose of qea is that it allowed its author to avoid learning to use something else. But I find it interesting that he recognizes the importance of computer verification for something like this, and maybe it indicates that this has been in the works for a while. It doesn’t have to be half-baked to be wrong, though.
Yeah, I’ve heard about this “notorious difficulty” in verifying proof checkers before, and I don’t understand what it could mean. Humans are way more unverifiable.
I think the idea is that for a point this controversial he is well aware that mathematicians may actually object to his trustworthiness (they’ve objected to less questionable things in the past), and want to verify the proof for themselves. I think he may well be right in this. However, I don’t see why he can’t give a full explanation (his current paper isn’t) for humans as well, since this would probably be finished sooner and would probably save a lot of his own time if there is a mistake.
Actually, I would be more interested in the size of checking core of Qea. Quickly inspecting 23 megabytes of proofs sounds like a bad idea. A converter to TSTP first-order proof format (for example) would allow me to use a few different bug-for-bug-independent well-tested checkers for this format that are already out there; that I would trust more than both human inspection and any single-implementation prover.
Strictly speaking, PA uses infinitely many axioms—the induction axiom is actually an axiom schema, one axiom for each predicate you can plug into it. If you actually had it as one axiom quantifying over predicates, that would be second-order.
This aspect is very interesting:
It seems easier to me to simply trust Coq than to read through 23 megabytes of proofs by eye. But I’m not entirely certain what the purpose of qea is.
It looks like Qea does verify the proof and generates human-readable text. In that case, my trust in it or Coq would be based on their relative size adjusted for amount of testing these tools received. Coq uses a non-trivially unique proof system (calclulus of coinductive constructions, if I remember correctly), which counts against it. Did anything look what proof system Qea uses?
Yeah, I’ve heard about this “notorious difficulty” in verifying proof checkers before, and I don’t understand what it could mean. Humans are way more unverifiable.
I bet the real purpose of qea is that it allowed its author to avoid learning to use something else. But I find it interesting that he recognizes the importance of computer verification for something like this, and maybe it indicates that this has been in the works for a while. It doesn’t have to be half-baked to be wrong, though.
I think the idea is that for a point this controversial he is well aware that mathematicians may actually object to his trustworthiness (they’ve objected to less questionable things in the past), and want to verify the proof for themselves. I think he may well be right in this. However, I don’t see why he can’t give a full explanation (his current paper isn’t) for humans as well, since this would probably be finished sooner and would probably save a lot of his own time if there is a mistake.
Actually, I would be more interested in the size of checking core of Qea. Quickly inspecting 23 megabytes of proofs sounds like a bad idea. A converter to TSTP first-order proof format (for example) would allow me to use a few different bug-for-bug-independent well-tested checkers for this format that are already out there; that I would trust more than both human inspection and any single-implementation prover.
How do you get to 733 axioms? Maybe I’m being stupid, but doesn’t PA run on just 5?
Strictly speaking, PA uses infinitely many axioms—the induction axiom is actually an axiom schema, one axiom for each predicate you can plug into it. If you actually had it as one axiom quantifying over predicates, that would be second-order.
I think that Nelson denies that there is a completed infinity of predicates that you can plug into the schema.
Well, you’d certainly only need finitely many to prove inconsistency.
I think 733 is counting axioms, definitions, and theorems all.
That would explain it.
It said “733 axioms, definitions, and theorems”
I’m guessing 733 is the sum of the axioms, definitions and theorems, not just the axioms alone.