Comment on Theories on Theories
lemonwood@lemmy.ml 18 hours agoI see philosophy as a place to make nonrigorous arguments.
It’s the other way around: math is where your 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 three questions are treated rigorously.
Of course, serious mathematicians are often philosophers at the same time.
pfried@reddthat.com 17 hours ago
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.
lemonwood@lemmy.ml 15 hours ago
I 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 15 hours ago
It is not necessary to solve the halting problem to show that a particular proof is correct.
lemonwood@lemmy.ml 14 hours ago
Lean runs on C++. C++ is a turning complete, compiled language. It and it’s compiler are subject to the halting problem.