= 27d567bc2d48d9f40e9ccc20ea370b15)
Sewing-Machine comments on Edward Nelson claims proof of inconsistency in Peano Arithmetic - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (115)
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.