I don't understand Gödel's incompleteness theorem anymore Here's the picture I have in my head of Model Theory:

*

*a theory is an axiomatic system, so it allows proving some statements that apply to all models consistent with the theory

*a model is a particular -- consistent! -- function that assigns every statement to its truth value, it is to be thought of as a "concrete" object, the kind of thing we actually usually think about. It's only when it comes to models that we have the law of the excluded middle.

My understanding of Gödel's first incompleteness theorem is that no theory that satisfies some finiteness condition can uniquely pin down a model.
So I am not really surprised by it. The idea of theories being incomplete -- of not completely pinning down a particular model -- is quite normal. The fact that no theory is complete seems analogous to how no Turing machine can compute every function.
But then I read this thread and there were two claims there in the answers which made no sense to me:

*

*Self-referential statements as examples of unprovable statements -- Like "there is no number whose ASCII representation proves this statement".

A statement like this cannot be constructed in propositional logic. I'm guessing this has to do with the concept of a "language", but why would anyone use a language that permits self-reference?
Wouldn't that be completely defeat the purpose of using classical logic as the system for syntactic implications?
If we permit this as a valid sentence, wouldn't we also have to permit the liar paradox (and then the system would be inconsistent)?


*Unprovable statements being "intuitively true/false" -- According to this answer, if we found that the Goldbach conjecture was unprovable, then in particular that means we cannot produce a counter-example, so we'd "intuitively" know that the conjecture is true.

How is this only intuitive? If there exist $\sf PA$-compatible models $M_1$, $M_2$ where Goldbach is true in $M_1$ but not $M_2$, then $\exists n, p, q$ such that $n= p+q$ in $M_1$ but not in $M_2$. But whether $n=p+q$ is decidable from $\sf PA$, so either "$\sf{PA}+\sf{Goldbach}$" or "$\sf{PA}+\lnot\sf{Goldbach}$" must be inconsistent, and Goldbach cannot be unprovable. Right?
In any case, I don't know what it means for the extension to be "intuitively correct". Do we know something about the consistency of each extension or do we not?
Further adding to my confusion, the answer claims that the irrationality of $e+\pi$ is not such a statement, that it can truly be unprovable. I don't see how this can be -- surely the same argument applies; if $e+\pi$'s rationality is unprovable, there does not exist $p/q$ that it equals, thus it is irrational. Right?
 A: The proof of Gödel's first incompleteness theorem relies on inventing a proposition-to-integer mapping. The theories it considers are able to describe this, as a function from strings of symbols to integers. It turns out that, even without direct self-reference, propositions can even talk about their own Gödel numbers. (There's no way to prohibit this in the theories of interest.) And some are equivalent to their own unprovability. Such statements are either true but unprovable, or false but provable.
If Goldbach's conjecture is false, it has a counterexample, so is decidable. Therefore, if a theory $T$ proves the conjecture is undecidable in $T^\prime$, $T$ also proves the conjecture true.
A: This answer only addresses the second part of your question, but you asked many questions so hopefully it's okay.
First, there is in the comments a statement: "If Goldbach is unprovable in PA then it is necessarily true in all models." This is incorrect. If Goldbach were true in all models of PA then PA would prove Goldbach by Godel's Completeness Theorem (less popular, still important).
What is true is:
Lemma 1: Any $\Sigma_1$ statement true in $\mathbb{N}$ (the "standard model" of PA) is provable from PA.
These notes (see Lemma 3) have some explanation: http://journalpsyche.org/files/0xaa23.pdf
So the correct statement is:
Corollary 2: If PA does not decide Goldbach's conjecture then it is true in $\mathbb{N}$.
Proof: The negation of Goldbach's conjecture is $\Sigma_1$. So if PA does not prove the negation, then the negation of Goldbach is not true in $\mathbb{N}$ by Lemma 1.
Remember that $\mathbb{N}$ is a model so any statement is either true or false in it (in our logic). But PA is an incomplete theory (assuming it's consistent), so we don't get the same dichotomy for things it can prove.
Now, it could be the case that PA does prove Goldbach (so its true in all models of PA including $\mathbb{N}$). But if we are in the situation of Corollary 2 (PA does not prove Goldbach or its negation) then Goldbach is true in $\mathbb{N}$ but false in some other model of PA. (This would be good enough for the number theorists I imagine.) This is also where the problem in your reasoning is. It is NOT true that if Goldbach fails in some model $M$ of PA then there is a standard $n$ in $\mathbb{N}$ that is not the sum of two primes. Rather the witness to the failure of Goldbach is just some element that $M$ believes is a natural number. In some random model, this element need not be in the successor chain of $0$.
On the other hand, the rationality of $\pi+e$ is not known to be expressible by a $\Sigma_1$ statement. So we can't use Lemma 1 in the same way.
Edited later: I don't have much to say about the question on self-referential statements beyond what others have said. But I'll just say that one should be careful to distinguish propositional logic and predicate logic. This also goes for your "general picture of Model Theory". Part of the interesting thing with the incompleteness theorems is that they permit self-reference without being so obvious about it. In PA there is enough expressive power to code statements and formal proofs, and so the self-referential statements about proofs and so forth are fully rigorous and uncontroversial.
A: Let me try to get at the heart of your misunderstanding as concise as possible:
1. We are not deliberately choosing to use a language that permits self-reference, we are forced to do so.
The only choice we made is that of a logic that is sufficiently strong to include integer arithmetic. What Gödel then proves is that access to the integers automatically allows us to construct somewhat self-referential statements. If we want integers, then we have to accept self-referentiality. The same is true in the theory of computability. Turing machines are not chosen because they can emulate themselves, they are chosen because they allow all operations we expect a general computer to do, which just happens to include emulating turing machines.
2. We are self-referential with respect to the theory, not the model.
The kind of sentences that Gödels procedure allows us to construct are of the form "X can not be infered from Y", as the integers are only used to build a copy of logical reasoning. If we pick the set of axioms of a given theory as Y, then we can construct sentences like "X is not provable in the theory" which is what leads to the incompleteness theorem if X is the sentence itself. There is no way to access a specific model of the theory and thus no way of constructing sentences like "X is false", which would be needed for the liar's paradoxon.
A: Allow me to start by pointing out that Gödel's theorems are usually studied in the context of first-order logic, whereas you are describing propositional logic in your understanding of theory and model.
While a theory is roughly the same idea of a collection of sentences and inference rules (although some people define a theory as also being closed under deductions), a model is very different. It is not just an assignment of truth values. So while propositional logic deals with a lot of "switches" that have true and false, first-order logic deals with collections of objects, some relations, some functions, and some named constants, and what statements a collection of objects interpreting these syntactic ideas will satisfy.
The two things, models and theories, are connected by Gödel's completeness theorem which states the first-order logic is complete (which is not the same as a theory being complete). So a statement is provable from a theory if and only if it is true in every model of the theory. And it is important to stress, "most theories" have a lot of different models, either by reasons like cardinality (if a theory has an infinite model, it has one of every infinite cardinality) or incompleteness (if a theory is not complete it has completely different models even in the same cardinality), or by other reasons (e.g. maybe the theory is complete, but there are things beyond the scope of the language that are not decided).
And while we utilise this deep connection all the time in mathematics, without even thinking about it most of the time, syntax and semantics are separate. Theories are not models, and models are not theories.
When you get to analyse these definitions, you will see that a first-order language cannot be self-referential. It cannot talk about its own model, because the tools to do so are simply not syntactic.
But, and here is the importance of the conditions of Gödel's incompleteness theorem, some languages are sufficient for internalising the whole of first-order logic, and under some basic assumptions a theory can provably do so.
In other words, if $T$ is a theory in a language which is "rich enough" (where "rich enough" is really quite poor: a binary relation or a binary function would suffice), and $T$ can internalise first-order logic, then it is not complete.
The key idea is that once we have formulas which we can prove to be an interpretation of first-order logic, we can make all sort of weird constructions. This is not self-referential as much as it is "self-aware". But even that is a misnomer.
The subtle point of the incompleteness theorem is that in different models of the same theory, the internalisation may be very different. It will always include a faithful copy of the actual first-order logic used "outside" the theory, but it may include new bits and pieces which may or may not be "reasonable".
Moreover, since the notion of "finiteness" is not captured internally by first-order logic, once we interpreted first-order logic, and found a predicate to represent the interpretation of a theory $T'$, if $T'$ had infinitely many axioms, if the internalisation process adds "new bits", it will invariably add new sentences to its own interpretation of $T'$.
So between different models of the theory $T$, we may get very different copies of first-order logic and different copies of $T'$. Gödel utilises this to construct a sentence which is not provable from $T$ itself.
But this is not the liar's paradox. At no point a sentence really refers to itself. It simply talks about an interpretation of itself. Because "true/false" is not the same as "provable/unprovable", unless you can quantify over all models, which you can't, since they are not part of your language.
Gödel wanted to avoid people looking at all of this and saying "Oh, those crazy logicians... good things we actually care about the natural numbers and not all of this formalism around it". So in the process he showed that all of this coding can be done in an extremely robust way by using the natural numbers and some very basic number theoretic results. Now mathematicians had to pay attention, this can no longer be ignored.
Finally, as to the remarks on the Goldbach Conjecture, I will direct your attention to Decidability of the Riemann Hypothesis vs. the Goldbach Conjecture.
A: 

*

*Self-referential statements as examples of unprovable statements -- Like "[there is no number whose ASCII representation proves this statement][1]".

A statement like this cannot be constructed in propositional logic. I'm guessing this has to do with the concept of a "language", but why would anyone use a language that permits self-reference?

Here's the crux of the issue. Actually, such a statement can be constructed. (Or, at least, a statement which acts like such a statement can be constructed.)
As you know, it's not possible to take the sentence "This sentence cannot be proved in ZFC" and simply translate it directly into the language of ZFC. This is because, as you know, there is nothing in the language of ZFC that means "this sentence".
What we can do, however, is create a sentence G that is true if and only if G cannot be proved in ZFC. How can we do this?
Well, take a look at the following English sentence:

If you write down the following, and then write it again in between quotation marks, then the resulting statement cannot be proved in ZFC: "If you write down the following, and then write it again in between quotation marks, then the resulting statement cannot be proved in ZFC:"

Notice that the part within quotation marks is identical to the part outside of quotation marks, and so "the resulting statement" is identical to the original statement. This statement refers to itself without ever using the phrase "this statement"!
It is possible to do something similar to the above "tricky sentence" in the language of ZFC. The desired sentence is "The sentence with Gödel number $N$ cannot be proved in ZFC", where $N$ is a particular number which is chosen in a way similar to the above "tricky sentence", so that $N$ is the Gödel number for a sentence which is logically equivalent to "The sentence with Gödel number [$N$] cannot be proved in ZFC".
The reason that this can't be extended to form the liar paradox is that the predicate "the statement $p$ cannot be proved in ZFC" can be defined in the language of ZFC, whereas the predicate "the statement $p$ is false" cannot. (In fact, the liar paradox you mention is the proof that the predicate "the statement $p$ is false" cannot be defined in the language of ZFC.)
