On independency of ZFC of statements in math problem solving

axiomslogicprovability

To be honest, this is a question that has been bothering me (provided that I understand this correctly), which probably means I'm not quite sure about what I ask, but I'm looking for some clarification.

I am a graduated mathematician who mostly work on graph theory. I admit I have to learn more about mathematical logic, but when I started to dig deeper, I found (and read) something about statements that are independent of some systems of axioms (not just ZFC: it's just what I heard most, more than PA or others). I read that formally some statements cannot be deduced from a selected system.

I found some independent statements (of ZFC) listed in Wikipedia page, and questions similar to this in Math SE too, but I seem to not get the answer I am wondering about. Some said that when you are trying to prove/deduce a statement, you don't necessarily need to care about its independency or something.

I mean, within my simple, curious mind, which currently might not get the idea of independency at all, isn't it natural to ask:

"Does this mean that if we face a math statement and want to know it is TRUE or FALSE, instead of (usually) only conjecturing that this statement is TRUE or FALSE and providing the reasoning (by this I mean I can try to prove it without any knowledge about axiomatic systems that I use at all), we actually need to also consider the possibility that this statement is independent (of something?) or anything like that?"

I hope anyone gets what I am saying and what my struggles are. This is because when I found some statements that are independent of ZFC or something, I was like "Wait, so does this mean that mathematicians every time must realize that when facing a statement, they must either:
a) show it is true,
b) show it is false, OR
c) show it is axiomatic (can't be proven true or false, relative to a system)?"

I am pretty sure I've never considered option c when doing math (or maybe I have, but I did not care and simply accept that I need AC to show each vector space has a basis). Is that such a normal, and preferable approach? Should we just accept that my above concern will rarely happen?
Is mine even a valid concern (since if I read it right, I (generally) should always consider doing additional work when trying to verify a statement)???

Maybe future (and more) researches will lead me to have to consider option c one day, though.

*feel free to criticize this question, if any
*some of my tags possibly are wrong ones

Best Answer

In a purely formal sense, you are right that if we have a set of axioms and a goal proposition in mind, we could show that the proposition is provable from the axioms, disprovable from the axioms, or independent (neither provable nor disprovable) from the axioms.

However, the phenomenon of independence is much less common when we look at "natural" mathematical statements, and work in strong systems such as ZFC. It is hard to make this formally precise, but if you look a a list of statements independent of ZFC you will see that they tend to have a "set theoretic" flavor. Only the Whitehead problem and the normal Moore space conjecture are sufficiently well known to have an actual name as a conjecture. On the other hand, essentially then entire body of published mathematics is provable in ZFC or small extensions of ZFC.

So, in practice, there's not a good reason for mathematicians working in less set theoretic areas (e.g. finite or countable combinatorics) to worry about whether their conjectures are independent of ZFC. Independence does not happen that often for statements that are encountered "naturally" in practice, but we know that it often happens that a particular result takes a long time and a lot of effort to prove or disprove.

Related Question