3 ms·
The quote pretty obviously is referring to checking a proof (series of logical statements) not an arbitrary logical statement. Compared to most reporting on te
by shasta 12y ago
The quote pretty obviously is referring to checking a proof (series of logical statements) not an arbitrary logical statement. Compared to most reporting on technical subjects, this reporting was wonderful.
- lutusp 12y ago> The quote pretty obviously is referring to checking a proof (series of logical statements) not an arbitrary logical statement. Checking a series of logical statements, and generating a series of logical statements, are not fundamentally different with respect to the issue of undecidability. > Compared to most reporting on technical subjects, this reporting was wonderful. Until I got to the passage I quoted, I agreed completely, and I agree in general in spite of it. It's one of those often-heard statements that make more experienced readers say, "Umm, wait, you really don't want to say it that way."
- gohrt 12y agoChecking a series of logical statements is just arithmetic. Generating a series of logical statements is only hard because the formal statements are not generated axiomatically, they are sourced from ill-understood human creativity. Once a formalism is defined it is trivial O(e^n) algorithm to generate all proofs of size n. http://math.stackexchange.com/questions/324867/automated-proof-checking-machine http://math.stackexchange.com/questions/324867/automated-pro...
- colanderman 12y agoTo be fair, n may be arbitrarily large, hence the undecidability of logics in general. (Not disagreeing with you, just clarifying.)