Comment by empath75
3 days ago
> the vast vast majority of statements in any axiomatic system are going to be decidable
This is just flatly untrue, in the strictest possible sense, and even in the generous definition of "statements that mathematicians care about", that is going to be very heavily biased towards questions that are decidable, because the questions that are likely to be decidable are the ones that they can even reason about to begin with.
If you're a computer programmer, the CS shadow of Godel comes up _all the time_ in practice, and undecidable situations are quite common and don't really need to be carefully constructed.
This is just the drunk-in-the-streetlight situation. Things seem to be decidable everywhere we look because we look where things are likely to be decidable.
To be fair, in the most literal sense, the vast majority of syntactically-valid statements in a typical FOL encoding will be trivial. One of my side-projects has been trying to find the shortest statements independent of ZF and some of its fragments. In fact, for every slightly nontrivial statement that requires actually building a construction, there are billions more that can be instantly solved via a few simplifications, and statically pruning the search tree a bit is the best we can do.
To actually get independence, we need very rigid statements that don't allow any simple way to fudge a solution or counterexample. If anything, statements that mathematicians (and programmers) care about are biased toward undecidability, simply because they're extremely biased toward nontriviality. We put in the hard work of building towers of rigid definitions to that effect.