3 ms·
I don't think it's too surprising. Mathematicians aren't in the business of searching around for all true theorems. They work on problems of interest. It seems
by 6gvONxR4sf7o 7y ago
I don't think it's too surprising. Mathematicians aren't in the business of searching around for all true theorems. They work on problems of interest. It seems much more likely that you fail to progress for all the usual reasons (it's hard) rather than because it's undecidable.
It's like the halting problem. It doesn't prevent programmers from automating stuff and reasoning about programs.
- libraryofbabel 7y agoYes and no. The analogy with the halting problem is a good one, and I completely agree that mathematicians are guided by what's interesting, not just by enumerating propositions. But they also advance many conjectures that are considered interesting open propositions to prove or disprove. Very very few of these interesting conjectures have turned out to be undecidable (the Continuum Hypothesis being, again, a notable special exception). And I guess that's my point: it's a curious fact that undecidability and "interestingness" don't seem to intersect very much, as far as we can tell. I don't think that's something that self-evidently had to be the case, but it's where we are after close on 100 years of living with what Gödel showed us.
- ProfHewitt 7y agoIn strongly-typed higher-order theories, the Continuum Hypothesis has _not_ been proved to be inferentially undecidable because Cohen's results do not apply to strongly-typed higher-order theories.