3 ms·
I was under the impression that even verification is Turing undecidable in general - ie http://en.wikipedia.org/wiki/Entscheidungsproblem http://en.wikipedia.or
by byerley 13y ago
I was under the impression that even verification is Turing undecidable in general - ie http://en.wikipedia.org/wiki/Entscheidungsproblem http://en.wikipedia.org/wiki/Entscheidungsproblem
- joe_the_user 13y agoIt's easy for impressions of undecidability to get out of hand. But actually, verification is computable. Verification has to be computable for things like Godel's theorem to work. If you read your link carefully, you'll notice it's about provability via axioms, not verification. Peace
- jonahx 13y agojoe, what is the difference between verification and provability?
- tel 13y agoVerification is saying that a given proof does substantiate a theorem—it's easy as it's "just" a special kind of type-checking algorithm. Provability is saying that given some theorem it's possible to find a proof in a particular axiomatic system.
- lisper 13y agoIt's the difference between showing that a candidate proof is correct, and coming up with a correct proof in the first place. Once you have a proof, showing it is correct is (easily) computable. But coming up with a correct proof in the first place is not computable in general. (More generally, deciding whether a given proposition is true -- i.e. whether a proof exists or not -- is not computable. That is the "entsheidungsproblem".)
- jonahx 13y agothanks. after reading your explanation it's clear that the verification is verification of the proof, whereas i was interpreting it as verification of the statement to be proved, hence my confusion.
- joe_the_user 13y agoWow, Until I read your post, it never occurred to me you were confused by the ambiguous implications of "verification". You remind me how easy it is, once you get the jargon and the concepts, to not actually write out everything into a form someone from the outside can understand.
- jonahx 13y agoYeah, I personally file that under "Lessons You Never Learn Enough Times." Glad my slowness could be of service :) In retrospect, it seems like something I should have been able to deduce, since it's kind of the only thing makes sense.
- Chattered 13y agoIt's standard to use a verifier to check the correctness of a computer program, by encoding the program and then doing proofs about it. As per Goedel, a verifier can't check the correctness of its own program. So they'll always be incomplete there. Missing such a theorem isn't exactly a deal-breaker though.