[dwohnitmok]

Godel's incompleteness theorems are really syntactic results rather than semantic results. The main consequence they have for modern mathematics is that there is no "one axiom system to rule them all," since you can always extend many systems with a new axiom, which doesn't change much, since mathematics since time immemorial has been engaged in the practice of tweaking various axioms and seeing what consequences emerge.

Indeed Godel's completeness (not incompleteness) theorem (which applies to most mathematical settings such as anything that uses ZFC) is a strong indication that everything mathematicians would care to prove is in fact provable.

[n4r9]

It's been a long time since I studied this stuff properly, but is it true to say that you can tell that a statement is provable (or otherwise) if it can be couched in the language of first order logic?

[dwohnitmok]

Not quite. One way of thinking about Godel's Completeness Theorem is to couch in the language of abstractions. Every formal theory is an abstraction that seeks to abstract over many different concrete use cases. In the process we know that we give up some specificity for this generality, that is we know that there are aspects of these concrete use cases that are "forgotten" by the abstract formal theory. In return we get greater reusability of our formal theory and the consequences we can prove using it.

However, the question arises whether the abstract formal theory "forgets too much." That is, we know we must trade some specificity for increased generality, but is it possible we've traded too much? Are there attributes shared in common by all the concrete use cases to which our formal theory is applicable to but to which our abstract formal theory is blind to?

That is perhaps our formal theory is applicable to humans, cows, mathematical sets, etc., and so it necessary forgets about e.g. human-specific features, but there may nonetheless be some statement A that is true about all these things which our formal theory is unable to prove?

Godel's Completeness Theorem states that the answer is negative. Our formal theory and that which we can prove using it are exactly the attributes that are held in common across all its use cases, no more no less. That is our abstraction "leaks" no more than is strictly necessary.

So if we cannot prove or disprove a given statement in our formal theory, that is because there is at least one concrete use case to which our formal theory applies but the statement is false and one concrete use case to which our formal theory applies but the statement is true. That is unprovability is exactly synonymous with independence.

Many first-order theories, such as the theory that consists entirely of the sentence "there exists an element which is Special" can have sentences which cannot be proved or disproved in the theory (e.g. "all elements are Special."). But by the Completeness Theorem that just means there are use cases where sometimes the sentence is true and sometimes it isn't (the theory could be equally applied to a set of elements only one of which is marked as "Special" or where all the elements are marked "Special").

Godel's Completeness Theorem and Incompleteness Theorems are independent phenomena. Not only is it possible for both to hold, only one to hold, or for none to hold, they also apply to different domains of discourse. The Completeness Theorem applies to entire logical systems (such as first-order logic), while the Incompleteness Theorems refer to specific theories (such as a single given theory in first-order logic).

The two taken together mean that e.g. for any first-order theory capable of expressing arithmetic there is always more than one concrete mathematical object that satisfies that theory. That is the abstract theory is incapable of uniquely specifying a single mathematical object. Stated equivalently any abstract theory containing arithmetic can always be indefinitely extended by new axioms.

This is a common theme of first-order logic and there are related results that show in other ways how first-order logic sometimes has problems pinning down unique objects (e.g. the Downward and Upward Lowenheim-Skolem Theorems).