The struggle is that the symbolic graphs we construct to explain facts become logical beasts of their own, prone to generating sentences paradoxical under our desired interpretation.
Of course, the proofs are first constructed in the context of meaning, but the entire process seems to be a struggle to context-switch between the realms of meaning and symbology, which do not necessarily mirror one another.
But Godel has somehow proved that symbols cannot always provide both a consistent and complete system of meaning.
Gödel seems very much related to this, but I'm still lost.
No, this is more about the philosophy of mathematics -- the question of "to which degree is mathematics 'real'?" Gödel did have an impact on this, with formalism no longer being a particularly viable viewpoint. But this is less of a strict mathematical question and more of a philosophical one.
No, the incompleteness theorem only examines how formal systems relate to themselves, not to reality. It shows that no significantly expressive system can be designed that won't allow paradoxical statements.
Unprovable statements. Not paradoxical statements. Paradoxes confound the reader, but can be explained as either being true or false due to rules that were implicitly used to construct the statement. Once all the steps are explicitly shown, with each rule that applies at each step, there is no more paradox.
On the other hand, unprovable statements never make it to the "but can be explained" stage: either the formal system is consistent, and these expressions by definition cannot have an answer, or they can be answered but the formal system is demonstrably inconsistent.
The formal system also needs to be a little more precise than "significantly expressive": it needs to allow for self-referential expressions. In effect, it must be possible to create an expression that can be mapped to the natural language sentence "This statement has no proof in this formal system".
While in natural language puzzles that might be a fun paradox to try to figure out, where the challenge is to determine whether, given the rules of the context, the answer is actually "true" or "false", when it comes to Godel sentences for formal systems there is never a paradox. Either they are undecidable, or the formal system is inconsistent. And we don't get an "out" by saying "but in reality, the answer is ..." because the whole point of formal systems is to be self-contained. There is nothing "outside" of them that we can use to make claims about expressions within that formal system. We only get the axioms of the formal system itself.
> It shows that no significantly expressive system can be designed that won't allow paradoxical statements.
The above is a complete misrepresentation of Gödel’s second incompleteness theorem.
The theorem holds for any sufficiently expressive system, where the term ‘sufficiently expressive’ has a precise formal meaning[1]. Moreover, it is not the case that any sufficiently expressive system must be inconsistent! The theorem could perhaps be paraphrased as ‘no sufficiently expressive consistent system can prove its own consistency’[2], as long as we are prepared to explain what ‘its own’ really means.
Importantly, there are systems that do not allow paradoxical statements, and are nevertheless quite expressive, in an informal sense. For example, any dependently typed[3] total functional programming language[4], such as Agda[5], Coq[6], Idris[7], or Lean[8].
All of these languages are designed to be consistent. Of course, implementation bugs do happen[9].
If you would like to learn more about dependent types, ‘The Little Typer’[10] is newly out and a lot of fun to read. For an accessible introduction to the concept of total functional programming, see Turner 2004[11].
I like your paraphrase but I think it muddies the water. We really want to prove that axioms of a system cannot be contradicted if the system is inconsistent.
To be even more precise, the system or theory T proves that there is no number n which provides a proof of contradiction for the axioms of T.
So its the axioms of the systems which all formal systems assume and hold to be true. Basically its impossible to prove that axioms are true with the same system.
In short, no formal system can define its own consistency because in order for its axioms to be true, the system must be inconsistent.
Of course, the proofs are first constructed in the context of meaning, but the entire process seems to be a struggle to context-switch between the realms of meaning and symbology, which do not necessarily mirror one another.
But Godel has somehow proved that symbols cannot always provide both a consistent and complete system of meaning.
Gödel seems very much related to this, but I'm still lost.