3 ms·
> An algorithm which verifies "reliability" is applied to the constructed solution (e.g a proof). If this algorithm terminates then we know that we have a g
by fao_ 11y ago
> An algorithm which verifies "reliability" is applied
to the constructed solution (e.g a proof). If this
algorithm terminates then we know that we have a
good solution of the original problem. If it does not
then we may have to start looking for another
solution.
I might be misunderstanding things here, but doesn't that mean that there would exist proofs that are impossible to know the answer to, since there exist algorithms that are finite but will not terminate in human time? My brain is throwing up the Halting Problem, but I'm not entirely sure if that has any concrete relation to this.
- Ericson2314 11y agoFirst of all, know that the Halting problem and incompleteness are very related, so you are on the right track :). Here the idea is that to type-check our proofs, if the proof language is sufficiently expressive, we need to run a program which may not terminate. But if it does terminate, we know the proof is good. From Gödel's perspective, the proof-checker is written in an inconsistent language, because infinite loops themselves prove anything! But us humans are only finite-time-patient, and we have Ctrl-C, so such technicalities are irrelevant :)