3 ms·
Ehhh what you are describing is an algorithm for evaluating the truth of a statement. Which is not the same thing as a proof at all.
by apalmer 10y ago
Ehhh what you are describing is an algorithm for evaluating the truth of a statement. Which is not the same thing as a proof at all.
- RGamma 10y agoIn classical logic your statement entails that there is a proof that cannot be checked (marked "true") by an algorithm (note, that the proof itself cannot be checked, not a fact, for which there is no proof) or that there is an algorithm marking something "true" that doesn't constitute a proof (trivially the thing that is marked "true" is proven). I doubt you'll find counterexamples to either of them, as an infinite, yet valid, proof is hardly believable (nobody of us could ever finish reading it) and a terminating ("marking true") algorithm always computes something.