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.
That’s my point. Mathematical proofs aren’t generally agreed. They are agreed by everyone to logically follow from the definitions and axioms started with. Every single statement in a mathematical proof evaluates to true or false, and if you don’t believe a mathematical proof, you can directly point to a statement that is false. 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.
Your same argument that mathematics can be discussed under philosophy can be used to argue that mathematics can be discussed under the framework of wild untethered speculation. Neither one is a convincing argument that philosophy or wild untethered speculation is useful.
This is why ethics has failed. It has been built on the unstable foundation of philosophy instead of on the solid foundation of mathematics.
Yes, they are. Have you seen the controversies around many recent proofs? Proofs are getting so long and topics so specialized, that simply just reading them takes for ever. Some important ones have only been checked by one or two people. Some have been out for years and are still controversial, because no one claims to have some the immense work to actually checked them. That’s one of the reasons why proof assistants are used in the first place. They help, but they come with their own problems and challenges.
This is why ethics has failed. It has been built on the unstable foundation of philosophy instead of on the solid foundation of mathematics.
This is such a very old idea and you’re not the first one to have it. Just try it yourself as an exercise. Is like to see how you get an ought from an is with pure math. Every one who tried to build ethics on math only failed. Please, just google it or read some of the links I shared. Philosophers are totally familiar with very advanced math and use it. Again read some articles on like set theory or quantum mechanics on plato.stanford.edu to verify yourself. It’s already being used and always has. Even the antique philosophers were mathematicians. They invented logic and geometry. Every philosophy student through antiquity and the middle ages up to the Renaissance was forced to learn them before getting to the more advanced topics.
No matter how smart you are, other smart people probably had very similar ideas before you, tried to formalize them, got challenged, responded, tried again and so on. The history of their work is the history of philosophy. Trying to do better without even reading any of it would fit the definition of being naive.
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.
That’s my point. Mathematical proofs aren’t generally agreed. They are agreed by everyone to logically follow from the definitions and axioms started with. Every single statement in a mathematical proof evaluates to true or false, and if you don’t believe a mathematical proof, you can directly point to a statement that is false. 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.
Your same argument that mathematics can be discussed under philosophy can be used to argue that mathematics can be discussed under the framework of wild untethered speculation. Neither one is a convincing argument that philosophy or wild untethered speculation is useful.
This is why ethics has failed. It has been built on the unstable foundation of philosophy instead of on the solid foundation of mathematics.
Yes, they are. Have you seen the controversies around many recent proofs? Proofs are getting so long and topics so specialized, that simply just reading them takes for ever. Some important ones have only been checked by one or two people. Some have been out for years and are still controversial, because no one claims to have some the immense work to actually checked them. That’s one of the reasons why proof assistants are used in the first place. They help, but they come with their own problems and challenges.
This is such a very old idea and you’re not the first one to have it. Just try it yourself as an exercise. Is like to see how you get an ought from an is with pure math. Every one who tried to build ethics on math only failed. Please, just google it or read some of the links I shared. Philosophers are totally familiar with very advanced math and use it. Again read some articles on like set theory or quantum mechanics on plato.stanford.edu to verify yourself. It’s already being used and always has. Even the antique philosophers were mathematicians. They invented logic and geometry. Every philosophy student through antiquity and the middle ages up to the Renaissance was forced to learn them before getting to the more advanced topics.
No matter how smart you are, other smart people probably had very similar ideas before you, tried to formalize them, got challenged, responded, tried again and so on. The history of their work is the history of philosophy. Trying to do better without even reading any of it would fit the definition of being naive.