I must say, be careful with "reasoning". For example, once a philosophy PhD minimized mathematics eloquently by saying all mathematical results are "tautological", hence uninteresting. Hence, why bother studying it, and in your case, why bother thinking Gödel did anything special.
Why bother about anything at all... there's the rub.
This seems quite circular, where the (claims mine) contrived statements enabling godel 2 incompletude theorem, make it unable to prove a non-contrived statement?
Thanks for the reference though, I'll admit that is a topic I'm not familiar enough with to fully challenge it.
> I must say, be careful with "reasoning". For example, once a philosophy PhD minimized mathematics eloquently by saying all mathematical results are "tautological", hence uninteresting. Hence, why bother studying it, and in your case, why bother thinking Gödel did anything special.
Yeah that's a classic, it's a good thought experiment but that only prove that one must not be careful with the pruning that can enable high level reasoning but more with being careful of fallacious or misleading reasonings. Yes in theory, mathematical chain proofs are only tautologies derived from ZFC/higher order logic, so yes mathematics doesn't say anything new. However in practice, the task of unfolding reasoning chains and being able to refer to past lemnas as abtractions/objects, enable the reader to optimize for cognition, and hence the more proofs advances, the more we can discover, retain, understand and refer, useful tautological yet transitive knowledge.
Also, I am aware there are non-contrived statements that are can't be proven in ZFC such as https://en.wikipedia.org/wiki/List_of_statements_independent.... I'm only claiming that the incompleteness theorems only find contrived ones, and that for the non-contrived ones humanity has found, it is NOT that they are mathematically unproveable, it is that ZFC is not enough.
There are plenty of people who find ZFC + ¬CH a reasonable axiomatic system.
EDIT: I misread samth's statement (https://news.ycombinator.com/item?id=31424581), which I think is proveable in ZFC; I thought their statement was ¬CH.
Your second paragraph is confused. Given an axiom system like ZFC, there are (a) statements that can be proved true or false using it, (b) statements that can't be proved that are true in a particular model, (c) statements that can't be proved that are false in that model. It's set (b) that the incompleteness theorem tells us must exist. The theorem doesn't "find" statements, it proves that (b) exists by constructing a particular one, which is necessarily meta because it applies to every formal system.
However, we do not have access to a model which tells us the answers for things like the CH. So all you can do is decide on the axiom scheme you like, and then some things are provable. You can always add more axioms, like CH, but you can add their negation instead, if you want. So there's no sense in which there's really a right answer for CH but we haven't found it yet.
Nothing especially contrived there. Less so for a professional logician.