3 ms·
Simply because there are some propositions that are unprovable in a consistent system with finite axioms. Having an algorithm that solves any proposition would
by krichman 14y ago
Simply because there are some propositions that are unprovable in a consistent system with finite axioms. Having an algorithm that solves any proposition would be equivalent to having an algorithm that solves the halting problem.
- hackinthebochs 14y ago>There is no algorithm that can determine the truth of any proposition in arithmetic (for example). It is impossible, in principle, to construct such an algorithm. But given any proposition in arithmetic, the mind can decide its truth value. These two statements seem to contradict, unless you grant that the mind either fudges the proof or constructs new axioms such that the proof can be valid. Why do you assume a program can never do this?
- leephillips 14y agoBecause the program that does it would itself be an algorithm with its own finite set of axioms. There would be undecidable propositions unreachable by the program.
- DanWaterworth 14y agoSolving the halting problem wouldn't be sufficient to tell you whether a proposition was true, but it could tell you whether a proposition is independent and if it wasn't whether it was true or false.