4 ms·
Hilbert's program was about whether every statement could be proved ab nihilo either true or false. The question remains: given a proof, can we verify it? Argua
by Twisol 5y ago
Hilbert's program was about whether every statement could be proved ab nihilo either true or false. The question remains: given a proof, can we verify it? Arguably, any proof conceived by a human mind should be verifiable in principle. So the Incompleteness Theorem doesn't really apply, either formally or morally.
A more interesting argument could be made on the basis of Rice's Theorem: for a Turing-complete language, the only non-trivial properties provable about a program are fundamentally syntactic. (Type systems can be seen as a way of elaborating your syntax to capture finer-grained details of your semantics). Here we have a richer and nearer-to-hand collection of programs whose properties are inaccessible -- take, for instance, whether the 3n+1 algorithm halts on all inputs. Again, though, if we have a proof of some property, we still ought to be able to verify it.
- tshaddox 5y agoIsn’t verifying a proof equivalent to determining whether a certain computer program halts?
- Twisol 5y agoNo, but it would be equivalent to verifying that a given computer program halts on a specified N steps. This is the same distinction between (among other things) P and NP problems. For any problem in P, given an instance of the problem I can produce a solution in polynomial time. For any problem in NP, given an instance of the problem and a candidate solution, I can determine whether the solution is valid in polynomial time. Determining whether a certain computer program halts would be equivalent to producing a proof, not verifying an existing one. Verifying a proof is, in principle, only a matter of making sure that each step of the proof is valid. Coming up with the right steps is a creative endeavor. Certainly, coming up with the right set of allowable steps is a creative endeavor, and proving that your system is expressive enough for interesting proofs is a creative endeavor. But once given a proof, verifying that it legally applies legal steeps is a purely mechanical endeavor.
- chadcmulligan 5y ago> But once given a proof, verifying that it legally applies legal steps is a purely mechanical endeavor. But isn't this the same as once having a program then executing it? which then has the problem of does it finish? so back to the halting problem?
- Twisol 5y agoNo, because a proof (especially a human-constructed proof) is a finite object built out of basic pieces. The only question as to the validity of a proof is whether the basic pieces have been fit together according to the established rules of the game. We don't have to have any notion of "execution" of a proof to verify that its construction is valid. Let me put it this way. I tell you that I can make apple juice if you give me an apple and a juicer. Do you have to give me anything to believe me? Several researchers have indeed put together a theory of "execution" of a proof; see for instance Prof. Frank Pfenning's research program on logic-based process calculi. These theories tend to have the common theme of execution as normalization -- the chosen mode of execution actively changes and evolves the proof structure until it reaches a terminal form, usually one with a particularly simple logical structure. Cut elimination is a central theme: any logical system worth calling "computational" (one argues) will support cut elimination, allowing you to replace a proof with steps like `A -> B, B -> C |- A -> C` with a direct proof of `A -> C` that does not use the intermediate hypothesis `B`. But we're not doing that when we're verifying a proof. We're looking at the finite, static structure of a proof term, and checking that it was put together legally.
- deleted 5y ago[deleted]
- deleted 5y ago[deleted]