I see philosophy as a place to make nonrigorous arguments.
It’s the other way around: math is where you just ignore questions about what makes sense, what knowledge is, what truth is, what a proof is, how scientific consensus is reached, what the scientific method should be, and so on. Instead, you just handwave and assume it will all work out somehow.
You’re just covering my third paragraph. Yes, everybody is a philosopher because we don’t have the tools to do away with philosophical arguments entirely yet.
Once a mathematical proof has been verified by computer, there is no arguing that it is wrong. The definitions and axioms directly lead to the proved result. There is no such thing as verifying a philosophical argument, so we develop tools to lift philosophical arguments into more rigorous systems. As I’ve shown earlier, and as another commenter added to with incompleteness, this is a common pattern in the history of philosophy.
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.
The fact that C++ is Turing complete does not prevent it from computing that 1+1=2. Similarly, the fact that C++ is Turing complete does not prevent programs created from it from verifying the proofs that they have verified. The proof of the halting problem (and incompleteness proofs based on the halting problem) itself halts. https://leanprover-community.github.io/mathlib_docs/computability/halting.html
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.
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. This is why the examples I gave earlier are now not explained by philosophy but by other systems. Once the tooling exists to lift a discussion out of philosophy, that is the end of philosophical debate for that topic.
Furthermore, the kernel still relies on CPU, memory and OS behavior to be bug free.
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.
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.
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 with his specific point of view 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.
Also, though you haven’t clearly articulated your philosophical position, it seems to be close to the one of the famous Vienna Circle
, which was inspired by Wittgenstein, but later rejected by him. It’s generally agreed today, that their project of logical empiricism has failed. You can find the critiques of the various points in the article above.
It’s the other way around: math is where you just ignore questions about what makes sense, what knowledge is, what truth is, what a proof is, how scientific consensus is reached, what the scientific method should be, and so on. Instead, you just handwave and assume it will all work out somehow.
Philosophy of mathematics is were these questions are treated rigorously.
Of course, serious mathematicians are often philosophers at the same time.
You’re just covering my third paragraph. Yes, everybody is a philosopher because we don’t have the tools to do away with philosophical arguments entirely yet.
Once a mathematical proof has been verified by computer, there is no arguing that it is wrong. The definitions and axioms directly lead to the proved result. There is no such thing as verifying a philosophical argument, so we develop tools to lift philosophical arguments into more rigorous systems. As I’ve shown earlier, and as another commenter added to with incompleteness, this is a common pattern in the history of philosophy.
I explicitly refer to your second paragraph.
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.
It is not necessary to solve the halting problem to show that a particular lean proof is correct.
Lean runs on C++. C++ is a turning complete, compiled language. It and it’s compiler are subject to the halting problem.
The fact that C++ is Turing complete does not prevent it from computing that 1+1=2. Similarly, the fact that C++ is Turing complete does not prevent programs created from it from verifying the proofs that they have verified. The proof of the halting problem (and incompleteness proofs based on the halting problem) itself halts. https://leanprover-community.github.io/mathlib_docs/computability/halting.html
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.
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. This is why the examples I gave earlier are now not explained by philosophy but by other systems. Once the tooling exists to lift a discussion out of philosophy, that is the end of philosophical debate for that topic.
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.
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 with his specific point of view 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.
Also, though you haven’t clearly articulated your philosophical position, it seems to be close to the one of the famous Vienna Circle , which was inspired by Wittgenstein, but later rejected by him. It’s generally agreed today, that their project of logical empiricism has failed. You can find the critiques of the various points in the article above.