= 27d567bc2d48d9f40e9ccc20ea370b15)
cousin_it comments on AI cooperation in practice - 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 (157)
The proof checker checks proofs within some formal theory. The Godel sentence for the checker is certainly true and provable by us, given the consistency of that formal theory. (If the theory were inconsistent, the checker would be able to prove any sentence.) But this doesn't work as a proof within the theory! The theory cannot believe its own consistency (Godel's second incompleteness theorem), so the checker cannot assume it when checking proofs. So your argument doesn't actually give an example of a valid proof rejected by the checker.
I think you mean that there would be some proof (that checks) for any sentence.
Yes. Thanks.
Let's say we are trying to prove statements within ZFC.
"ZFC can never prove this statement to be true"
...is one thing and...
"This proof checker can never prove this statement to be true"
...is another.
Neither can be proved by the specified proof checker - but the second statement can be proved by another, better proof checker - still working within ZFC - so it can be seen that it is true.
"proved by a proof checker" - huh?
"Asserted", "approved" - whatever.
Worse, it's only "true" that a consistent theory is consistent in some unclear sense, because you can extend the theory with a statement that asserts inconsistency of the original theory, and the resulting theory will remain consistent.
What you're saying is certainly true (onlookers, see pages 5-6 of this pdf for as especially clear explanation), but I like to think that you can't actually exhibit a proof string that shows the inconsistency of PA. If you could, we'd all be screwed!
Proof in what theory, "can't" by what definition of truth? In the extension of PA with inconsistency-of-PA axiom, it's both provable and true that PA is inconsistent.
A proof in PA that 1+1=3 would suffice. Or, if you will, the Goedel number of this proof: an integer that satisfies some equations expressible in ordinary arithmetic. I agree that there's something Platonic about the belief that a system of equations either has or doesn't have an integer solution, but I'm not willing to give up that small degree of Platonism, I guess.
You would demand that particular proof, but why? PA+~Con(PA) doesn't need such eccentricities. You already believe Con(PA), so you can't start from ~Con(PA) as an axiom. Something in your mind makes that choice.