Comment on Theories on Theories
lemonwood@lemmy.ml 19 hours agoI explicitly refer to your second paragraph.
I covered those other arguments in another top level comment in this same thread. Yes, you absolutely can argue computer verified proofs. They are very likely to be true (same as truth in biology or sociology: a social construct), but to be certain, you would need to solve the halting problem to proof the program and it’s compiler, which is impossible. Proofing incompleteness with computers isn’t relevant, because it wasn’t in question and it doesn’t do away with it’s epistemological implications.
pfried@reddthat.com 19 hours ago
It is not necessary to solve the halting problem to show that a particular proof is correct.
lemonwood@lemmy.ml 18 hours ago
Lean runs on C++. C++ is a turning complete, compiled language. It and it’s compiler are subject to the halting problem.
pfried@reddthat.com 18 hours ago
The fact that C++ is Turing complete does not prevent it from computing that 1+1=2. Similarly, the fact that Lean is Turing complete does not prevent it from verifying the proofs that it has verified.
lemonwood@lemmy.ml 12 minutes ago
It’s not about those specific proofs. You’re claiming, that every possible proof stated in lean will always halt. Lean tries to evade the halting problem best as possible, by requiring functions to terminate before it runs a proof. But it’s not able to determine for every lean program it halts or not. That would solve the halting problem. Furthermore, the kernel still relies on CPU, memory and OS behavior to be bug free. Can you be sure enough in practice, yeah probably. But you’re claiming absolute metaphysical certainty that abolishes the need for philosophy and sorry, but no software will ever achieve that.