I feel like some weird hawk that swoops in for a lot of these Godel comments.
No Godel's incompleteness theorems prove nothing about truth by themselves. They are only statements about proofs and can be independently paired with other statements (as well as their negation), both philosophical and mathematical, about truth. That is the incompleteness theorems are silent on the matter of truth as a direct consequence, but require other theorems or philosophies to further mold statements on truth (the incompleteness theorems do have important indirect impact on those statements).
For example there is Godel's Completeness Theorem , which in a vague sense proves that "all true things are provable" (I can explain in greater detail if so desired). Godel's Completeness Theorem holds independently of Godel's Incompleteness Theorems (that is all four possible pairings of holding/not holding can apply to different formal systems). Notably Godel's Completeness Theorem holds for first order logic, the most common formalization of mathematical foundations (which includes ZFC and Peano Arithmetic).
> Can you give an example of a statement that is independent of ZFC yet useful/often-used?
Very briefly, the proof of Fermat's Last Theorem used an axiom that is independent of ZFC (it used a large cardinal axiom). It was later found that the proof did not require this axiom and could be fully formalized within ZFC.
There are separately simple-sounding and useful-sounding, but not actually used, statements which are independent of ZFC (such as if the set X is smaller than the set Y by cardinality then X has fewer subsets than Y).
But almost all of mainstream mathematics is perfectly happy to remain in ZFC.
There is separately an interesting empirical/philosophical question of whether there might still be a "practically complete" set of axioms to do mathematics which is not definitively settled by Godel's Incompleteness Theorems.
> And are you saying formal proof assistants like coq and isabelle are fools errands, in the sense that mathematics is in principal beyond formalization? If not, then why not?
Ugh this is why associating Godel's Incompleteness Theorems with truth can be so misleading. Godel's Incompleteness Theorems, in contexts where Godel's Completeness Theorem holds, has little overall consequence for formal proof assistants. Whether the conception of abstraction in a human mind in principle is beyond formalization is a deep philosophical question (but this is not specific to mathematics, this is really just the age old philosophical question of whether qualia and the human consciousness are reducible). However mathematics as practiced by working mathematicians and laid out in theorems and proofs is formalizable essentially by definition.
No Godel's incompleteness theorems prove nothing about truth by themselves. They are only statements about proofs and can be independently paired with other statements (as well as their negation), both philosophical and mathematical, about truth. That is the incompleteness theorems are silent on the matter of truth as a direct consequence, but require other theorems or philosophies to further mold statements on truth (the incompleteness theorems do have important indirect impact on those statements).
For example there is Godel's Completeness Theorem , which in a vague sense proves that "all true things are provable" (I can explain in greater detail if so desired). Godel's Completeness Theorem holds independently of Godel's Incompleteness Theorems (that is all four possible pairings of holding/not holding can apply to different formal systems). Notably Godel's Completeness Theorem holds for first order logic, the most common formalization of mathematical foundations (which includes ZFC and Peano Arithmetic).
> Can you give an example of a statement that is independent of ZFC yet useful/often-used?
Very briefly, the proof of Fermat's Last Theorem used an axiom that is independent of ZFC (it used a large cardinal axiom). It was later found that the proof did not require this axiom and could be fully formalized within ZFC.
There are separately simple-sounding and useful-sounding, but not actually used, statements which are independent of ZFC (such as if the set X is smaller than the set Y by cardinality then X has fewer subsets than Y).
But almost all of mainstream mathematics is perfectly happy to remain in ZFC.
There is separately an interesting empirical/philosophical question of whether there might still be a "practically complete" set of axioms to do mathematics which is not definitively settled by Godel's Incompleteness Theorems.
> And are you saying formal proof assistants like coq and isabelle are fools errands, in the sense that mathematics is in principal beyond formalization? If not, then why not?
Ugh this is why associating Godel's Incompleteness Theorems with truth can be so misleading. Godel's Incompleteness Theorems, in contexts where Godel's Completeness Theorem holds, has little overall consequence for formal proof assistants. Whether the conception of abstraction in a human mind in principle is beyond formalization is a deep philosophical question (but this is not specific to mathematics, this is really just the age old philosophical question of whether qualia and the human consciousness are reducible). However mathematics as practiced by working mathematicians and laid out in theorems and proofs is formalizable essentially by definition.