I'm trying to make sense of Gödel's incompleteness theorems. I feel like the existential crisis that these theorems cause is overblown.
First, these theorems don't prove that it's impossible to prove that a theory is consistent. Gentzen proved the consistency of Peano arithmetic in arithmetic, using an principle to do recursion up to ε₀. You can give a model of ZFC is set theory by assuming the existence of an inaccessible cardinal. People in the MetaRocq project are proving the consistency of the Rocq prover, they are only assuming strong reduction (that implies the consistency of Rocq).
Sure these proofs are not 100% self-contained, but they are still fruitful.
I feel that this theorems prove an inherent limitation of axiomatic reasoning. Whenever you have system T, by a diagonal construct, there are unprovable statements.
My interpretation would be that mathematics cannot be reduced to a single axiomatic system. One day or another, you'll need an extra principle. And this is not much of a problem when you think of it.
I'm sorry, I'm talking about a topic I don't 100% understand, don't hesitate to add something if you studied this more than me.
