Comment on Theories on Theories
pfried@reddthat.com 2 weeks agoThe 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 2 weeks 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.
pfried@reddthat.com 2 weeks ago
It certainly is about those specific proofs and anything that has been rigorously proven in Lean. We’re discussing techniques that show something is correct forever, and those proofs show that something is correct forever. Philosophical arguments don’t even show that something is correct today.
Only to a point, just like human language proofs require the reviewers brains to be bug free to a point. The repeated verification makes proofs as correct as anything can get.
lemonwood@lemmy.ml 2 weeks ago
Exactly, I’m glad you understand. There’s no epistemological certainty in math, just like in normal language. We have to make do with being pretty certain, as good as it gets. I like lean for it’s intended purpose: advancing math. No one involved in lean is seriously claiming it produces some kind of religious absolute certainty. Neither is anyone trying to replace philosophy.
Math can’t elevate anything above philosophy, because in a sense, it is part of philosophy, one of the parts using specialized language, specifically the part that is concerned with tautologies.
Have you clicked on the links to the philosophy wiki I provided? Maybe read about what a brilliant mathematician and philosopher has written on the philosophy of mathematics to convince yourself, that philosophy of mathematics is valuable and necessary (wether you agree or not). You’re already engaging in philosophical debate yourself. Your claims about the nature of philosophical arguments and mathematical proofs are themselves philosophical in nature.
pfried@reddthat.com 2 weeks ago
That’s my point. Mathematical proofs aren’t generally agreed. Philosophical arguments are generally agreed upon until the tools to take them out of philosophy are developed, and then the philosophical arguments are discarded entirely.