Comment by hnfong
2 years ago
> inevitable difference between "true" and "provable" (ie Godel's incompleteness). Now that part is pretty much solved, we are fairly confident that the foundations of mathematics are consistent.
Your assertion about the inevitability is true only under specific axioms. If you are willing to drop the notion that infinity exists, or the law of excluded middle (and maybe others), the problems that arise from Gödel's incompleteness theorems don't necessarily apply.
I'm very far from mathematician circles so I don't know how they actually interpret Gödel, but the idea of being "fairly confident" that math foundations are consistent while knowing that either there are true statements that we can't prove, or that the foundations aren't consistent, feels like a pretty weird thing to me.
I always thought most mathematicians just looked at Gödel like he discovered an interesting novelty, then ignored him and went back to doing whatever math they were already doing, instead of losing sleep over what his theorem implied.
That there are statements which might be true but we don't know how to prove was always the reality in mathematics. That this is not a temporary reality but something we're doomed to was thus not a huge revelation. Definitely not something I would expect anyone to lose sleep over.
Also, is it true that constructive mathamtics actually escapes Godel's theorems? My understanding was that any system strong enough to contain regular arithmetic is subject to it. Either way, constructive math is more limited in what it accepts as proofs, so there will be more, not fewer statements that are true but unprovable with such a system.
Classical logic embeds in intuitionistic logic by Gödel–Gentzen see https://en.m.wikipedia.org/wiki/Double-negation_translation