How is the Gödel's Completeness Theorem not a tautology? As a physicist trying to understand the foundations of modern mathematics (in particular Model Theory) $-$ I have a hard time coping with the border between syntax and semantics. I believe a lot would become clearer for me, if I stated what I think the Gödel's Completeness Theorem is about (after studying various materials including Wikipedia it seems redundant for me) and someone knowledgeable would clarify my misconceptions. So here it goes:
As I understand, if we have a set $U$ with a particular structure (functions, relations etc.) we can interpret it (through a particular signature, e.g. group signature $\{ e,\cdot \}$ ), as a model $\mathfrak{A}$ for a certain mathematical theory $\mathcal{T}$ (a theory being a set of axioms and its consequences). The theory is satisfied by $\mathfrak{A}$ only if $U$'s structure satisfies the axioms.
Enter Gödel's theorem: For every first order theory $\mathcal{T}$ :
$$\left( \exists \textrm{model } \mathfrak{A}:
\mathfrak{A} \models \mathcal{T} \right) \iff \mathcal{T} \textrm{ is consistent}$$
So I'm confused. Isn't $\mathcal{T}$ being consistent a natural requirement which implicates that a set $U$ with a corresponding structure  always exists (because of the ZFC's set theory freedom in constructing sets as we please without any concerns regarding what constitutes the set)? And that in turn always allows us to create a model $\mathfrak{A}$ with an interpretation of the signature of the theory $\mathcal{T}$ in terms of $U$'s structure?
Where am I making mistakes? What concepts do I need to understand better in order to be able to properly comprehend this theorem and what model theory is and is not about? Please help!
 A: Even today the connection between all this and computability is not sufficiently emphasized.
What does "consistent" mean?  It means you can't deduce a contradiction.  Your means of deducing must be (1) sound and (2) effective, but we'd also like it to be (3) complete.
"Sound" means if you can deduce $\alpha$ from $\mathcal T$, then $\alpha$ is true in every structure in which all the members of $\mathcal T$ are true.
"Effective" means there's an algorithm for checking the validity of your deductions.  That's the aforementioned connection with computability.
"Complete" means you can deduce everything you ought to be able to deduce.  If $\alpha$ is true in every structure in which all the members of $\mathcal T$ are true, then you ought to be able to deduce $\alpha$.  "Incomplete" would mean for some $\alpha$ and $\mathcal{T}$, it would be the case that $\alpha$ is true in every structure in which all the members of $\mathcal T$ are true, but your means of deducing are insufficient to prove that.  That means $\mathcal{T}\cup\{\sim\alpha\}$ would be consistent!  That's what "consistent" means.  It means you can't deduce a contradiction.  But there would be no structure in which everything in $\mathcal{T}\cup\{\sim\alpha\}$ is true.  It would be a consistent theory with no model.  "Complete" means your method of deducing things is enough to deduce $\alpha$ from $\mathcal{T}$ if $\alpha$ is true in every structure in which all the members of $\mathcal T$ are true.  But that's the same as saying that if your method of deducing is not enough to show that $\alpha$ is true in every structure in which all the members of $\mathcal T$ are true, then $\alpha$ is false in some structure in which all the members of $\mathcal{T}$.  "Some structure" means there exists a structure.  So completeness means there exists a structure satisfying a theory, if the theory is consistent.
It is a consequence of Gödel's incompleteness theorem that there can be no completeness theorem for second-order logic.  That means every method of deduction for second-order logic that is sound and effective is incomplete: you cannot deduce everything that you ought to be able to deduce.  What consistency means then depends on which system of deducing you use, but no matter which one it is, there will be some consistent theories with no model.  But they will be "consistent" only because they are not powerful enough to find the contradiction.
A: $T$ is consistent means that there is no way in which you can obtain a contradiction from it with syntactical manipulations. It is a syntactical notion and means that as long as you stick to the proper rules about writing proofs there is no way get a conclusion of the form $\alpha\wedge\neg\alpha$. Is it immediately clear that just because there is no way to write a proof of a contradiction, we can come up with a structure that "makes $T$ true" inside of it ($T$ is satisfiable means that you can come up with such a structure)? If it is then there should be an "obvious choice" for such a structure. What would it be?
I think if you think about the above questions you'll see that Godel's completeness theorem  isn't as obvious as you first thought.
A: I want to suggest you some additional reflections on this topic.
You can see this post for an "historical" overview, aimed to show that the current "mainstream" reading of Gödel's Completeness Theorem as :


for f-o theory, satisfiability is equivalent to consistency


was not the "driver" to Gödel's discovery.
The original context was :

the 2nd of famous Hilbert's problems regarding the consistency of arithmetic

and the "call for a solution" contained into the first mathematical logic textbook : David Hilbert & Wilhelm Ackermann, Principles of Mathematical Logic (1st german ed - 1928).
In the second edition (1938) [citation from the english translation (1950), page 95] :

we may ask whether we have completeness in the other sense [see page 42 : The completeness of an axiom system may be defined in two ways. First, it may be taken to mean that all the true formulas of a certain domain which is characterized by content can be proved from 
  the set of axioms.]  The question here is whether all universally valid formulas of the predicate calculus, as defined at the beginning of this chapter, can be proved in the axiom system. We actually do have completeness in this sense. The proof is due to K.Gödel [Die Vollstandigkeit der Axiome des logischen Funktionen-kalkuls, Mh.Math.Physik, Vol.37 (1930).]

Recall also the comment [page 88] about the (proven) consistency of the axiomatization of f-o calculus :

We must not, by the way, overestimate the significance of this consistency proof [of f-o logic]. It amounts to saying that we assume the domain of individuals underlying the axioms to consist of only a single element, and thus to be finite. We have absolutely no assurance that the formal introduction of postulates unobjectionable as regards content leaves the system of theorems consistent.
For example, the question remains unanswered whether the addition of mathematical axioms would not, in our calculus, make any arbitrary formula provable. This problem, whose solution is of fundamental importance for mathematics, is incomparably more difficult than the question dealt with here. The mathematical axioms actually assume an infinite domain of individuals, and there are connected with the concept of infinity the difficulties and paradoxes which play a role in the discussion of the foundations of mathematics. 

Now we have on the scene the three "actors" of the play :


*

*the adequacy of axioms and rules of "restricted predicate calculus" (i.e.f-o logic) regarding the notion of (universally) valid formula (solved in the positive by Gödel's Completeness Th)

*the paramount relevance of consistency proofs for "fundamental" mathematical theories, like arithmetic and set theory (see 2nd Hilbert's problem), as a "solution" to the foundational problem (Frege, Russell's paradox, Intuitionism)

*the search for a proof of "another kind" of completeness. 
In this context, we can read again the above passage from H&A :


The completeness of an axiom system [...] may be taken to mean that all the true formulas of a certain domain which is characterized by content can be proved from the set of axioms


as regarding also arithmetic. In this case, it amount to the question if [first-order version of] Peano's axioms are sufficient [or adequate, i.e.complete] to prove all arithmetical truth expressible in f-o language.
And again Gödel gave us the answer : NO, with his Incompleteness Theorems.
A: Look at it this way: 


*

*Semantics & model theory is reasoning about some hypothetical reality.

*Syntax & proof theory is just making marks on a piece of paper by mindlessly following certain rules.


The Completeness Theorem is the remarkable claim that these two very different things are in some sense equivalent to each other.
Take a simple example where T is just one sentence ∃a:a=a ("Something exists that equals itself").


*

*The semantic approach: Can I find a meaning for a for which the sentence ∃a:a=a is true? Hmm, lets try a=0. Ooh yes, that works, QED.

*The syntactic approach: Can I derive the formula ∃a:a=a in my proof theory calculus? 


*

*The detail here will depend on which calculus you use, but your proof will just be a series of sentences–meaningless lines of symbols–which the rules of the calculus allow you to write down and of which the last line is ∃a:a=a. None of the symbols ∃ or a or = mean anything. They're just marks on paper.

*[So a proof theory calculus always has two things: Rules for sentences you are always allowed to just write down. These are called axioms. And rules for "given you have already written down some sentences, you are now allowed to write down this new sentence." These are often called derivation rules.]



It feels tautologous perhaps because when you look at some actual rules in a propositional calculus (e.g. "from P and P→Q derive Q") you instinctively 'see' them as more than marks on a piece of paper. You 'see' that they could have a meaning. And this is partly because, the proof calculi you most often meet were specifically crafted to imitate the rules we use in logical reasoning. They are designed to look as if they mean something.
The Completeness Theorem is the proof of what you have instinctively 'seen'. It bridges the gap between obvious and proven.
Foundations of Mathematics is very much about proving the obvious. Or rather, checking whether the obvious really is true after all.
A: Gödel's completeness theorem is far from being a tautology. But it can appear so if you don't correctly apprehend the different notions in play. This answer will remain highly informal on purpose.
Gödel and its predecessors have tried to capture the essence of a mathematician's daily work. They looked at what we do when we prove things and made it formal : this is what we call syntax. So syntax is a kind of modelization (in the applied science sense) of the wild principle of proof. But the modelization could have failed, and capture only a portion of what is a proof. Gödel's theorem tells you this is not the case. So, in a very informal way, Gödel's theorem can be stated as :

The attemp to modelize the principle of proof by syntax is successful !

Of course, in order to prove such a statement, one has to translate it in mathematical term. 
First, what people call soundness : if one can write a syntactic proof from some axioms, then every mathematical model satisfying those axioms must satisfy the conclusion of the proof. It is just saying that we can carry a known proof in any mathematical world where it makes sense. In short, it is checking that we did not make stupid rules when defining the syntax.
Secondly, the much harder problem of completeness : if a sentence is satisfied in any model of some fixed axioms, I must be able to construct a syntactic proof. This is where you know that the attempt of modelization is successful, and that you have not just modelize a small portion of what is a proof.
A: It may help to look at things from a more general perspective. Presentations that focus on just first-order logic may obscure the fact that specific choices are implicit in the definitions of first-order logic; the general perspective highlights these choices. I want to write this up in detail, as a reference.
General "logics"
We define a particular type of general "logic" with negation. This definition is intended to be very general. In particular, it accommodates much broader types of "syntax" and "semantics" than first-order logic.  
A general "logic" will consist of:


*

*A set of "sentences" $L$. These do not have to be sentences in the sense of first-order logic, they can be any set of objects.

*A function $N: L \to L$ that assigns to each $x \in L$ a "negation" or "denial" $N(x)$.

*A set of "deductive rules", which are given as a closure operation on the powerset of $L$. So we have a function $c: 2^L \to 2^L$ such that


*

*$S \subseteq c(S)$ for each $S \subseteq L$

*$c(c(S)) = c(S)$ for each $S \subseteq L$

*If $S \subseteq S'$ then $c(S) \subseteq c(S')$. 


*A set of "models" $M$. These do not have to be structures in the sense of first-order logic. The only assumption is that each $m \in M$ comes with a set $v_m \subseteq L$ of sentences that are "satisfied" (in some sense) by $M$: 


*

*If $S \subseteq L$ and $x \in v_m$ for each $x \in S$ then $y \in v_m $ for each $y \in c(S)$

*There is no $m \in M$ and $x \in L$ with $x \in v_m$ and $N(x) \in v_m$
The exact nature of the "sentences", "deductive rules", and "models", and the definition of a model "satisfying" a sentence are irrelevant, as long as they satisfy the axioms listed above. These axioms are compatible with both classical and intuitionistic logic. They are also compatible with infinitary logics such as $L_{\omega_1, \omega}$, with modal logics, and other logical systems.
The main restriction in a general "logic" is that we have included a notion of negation or denial in the definition of a general "logic" so that we can talk about consistency.


*

*We say that a set $S \subseteq L$ is syntactically consistent if there is no $x \in L$ such that $x$ and $N(x)$ are both in $c(S)$.

*We say $S$ is semantically consistent if there is an $m \in M$ such that $x \in v_m$ for all $x \in S$. 
The definition of a general "logic" is designed to imply that each semantically consistent theory is syntactically consistent. 
First-order logic as a general logic
To see how the definition of a general "logic" works, here is how to view first-order logic in any fixed signature as a general "logic". Fix a signature $\sigma$.


*

*$L$ will be the set of all $\sigma$-sentences. 

*$N$ will take a sentence $x$ and return $\lnot x$, the canonical negation of $x$. 

*$c$ will take $S \subseteq L$ and return the set of all $\sigma$-sentences provable from $S$. 

*$M$ will be the set of all $\sigma$-structures. For each $m \in M$, $v_m$ is given by the usual Tarski definition of truth.
With these definitions, syntactic consistency and semantic consistency in the general sense match up with syntactic consistency and semantic consistency as usually defined for first-order logic.
The completeness theorem
Gödel's completeness theorem simply says that, if we treat first-order logic in a fixed signature as a general "logic" (as above) then syntactic consistency is equivalent to semantic consistency. 
The benefit of the general perspective is that we can see how things could go wrong if we change just one part of the interpretation of first-order logic with signature $\sigma$ as a general "logic":


*

*If we were to replace $c$ with a weaker operator, syntactic consistency may not imply semantic consistency. For example, we could take $c(S) = S$ for all $S$. Then there would be syntactically consistent theories that have no model. In practical terms, making $c$ weaker means removing deduction rules.

*If we were to replace $M$ with a smaller class of models, syntactic consistency may not imply semantic consistency. For example, if we we take $M$ to be just the set of finite $\sigma$-structures, there are syntactically consistent theories that have no model. In practical terms, making $M$ smaller means excluding some structures from consideration.

*If we were to replace $c$ with a stronger closure operator, semantic consistency may not imply syntactic consistency. For example, we could take $c(S) = L$ for all $S$. Then there would be semantically consistent theories that are syntactically inconsistent. In practical terms, making $c$ stronger means adding new deduction rules.
On the other hand, some changes would preserve the equivalence of syntactic and semantic consistency. For example, if we take $M$ to be just the set of finite or countable $\sigma$-structures, we can still prove the corresponding completeness theorem for first-order logic. In this sense, the choice of $M$ to be the set of all $\sigma$-structures is arbitrary.
Other completeness theorems
We say that the "completeness theorem" for a general "logic" is the theorem that syntactic consistency is equivalent to semantic consistency in that logic.


*

*There is a natural completeness theorem for intuitionistic first-order logic. Here we let $c$ be the closure operator derived from any of the usual deductive systems for intuitionistic logic, and let $M$ be the set of Kripke models.  

*There is a completeness theorem for second-order logic (in a fixed signature) with Henkin semantics. Here we let $c$ be the closure operator derived from the usual deductive system for second-order logic, and let $M$ be the set of Henkin models.  On the other hand, if we let $M$ be the set of all "full" models, the corresponding completeness theorem fails, because this class of models is too small.

*There are similar completeness theorems for propositional and first-order modal logics using Kripke frames.
In each of those three cases, the historical development began with a deductive system, and the corresponding set of models was identified later. But, in other cases, we may begin with a set of models and look for a deductive system (including, in this sense, a set of axioms) that leads to a generalized completeness theorem. This is related to a common problem in model theory, which is to determine whether a given class of structures is "axiomatizable".
A: The usual form of the completeness theorem is this: $ T \models \phi \implies T \vdash\phi$, or that if $\phi$ is true in all models $\mathcal{M} \models T$, then there is a proof of $\phi$ from $T$. This is a non-trivial statement, structures and models are about sets with operations and relations that satisfy sentences. Proofs ignore the sets with structure and just gives rules for deriving new sentences from old. 
If you go to second order logic, this is no longer true. We can have a theory $PA$, which only has one model $\mathbb N \models PA$, but there are sentences $PA \models \phi$ with $PA \not\vdash \phi$ ("true but not provable" sentences). This follows from the incompleteness theorem which says that truth in the particular model $\mathbb N$ cannot be pinned down by proofs. The way first order logic avoids this is by the fact that a first order theory can't pin down only one model $\mathbb N \models PA$. It has to also admit non-standard models (this follows from Lowenheim-Skolem).
This theorem, along with the soundness theorem $T\vdash \phi \implies T\models \phi$ give a strong correspondence between syntax and semantics of first order logic.
Your main confusion is that consistency here is a syntactic notion, so it doesn't directly have anything to do with models. The correspondence between the usual form of the completeness theorem, and your form is by using a contradiction in place of $\phi$, and taking the contrapositive. So if $T \not \vdash \bot$ ($T$ is consistent), then $T \not \models \bot$. That is, if $T$ is consistent, then there exists a model $\mathcal M \models T$ such that $\mathcal M \not \models \bot \iff \mathcal M \models \top$, but that's a tautology, so we just get that there exists a model of $T$. 
A: You can think of this as a proof that set theoretic constructions truly are powerful enough to construct models of theories that are consistent. And conversely, that the method of deductive proof truly is powerful enough to prove the statements about a theory that must be true in all models.
A priori, this might not have been true. Here is an example that might demonstrate this. Let's assume that the first-order theory of real numbers is consistent (more precisely, the "theory of real closed fields"). We can construct a new theory by adding to the theory of real numbers:


*

*A new constant symbol $W$

*An axiom $1 < W$

*An axiom $1 + 1 < W$

*An axiom $1 + 1 + 1 < W$

*... and so forth


This theory is consistent! It's actually very easy to prove: as follows.


*

*The theory formed by only taking the first $N$ of these new axioms rather than all of the axioms is obviously consistent: we can simply interpret $W$ as $N + 2$, and we get a model of this theory.

*If the theory formed by taking all of these new axioms were inconsistent, then we could use the axioms to prove a contradiction. However, proofs have only finitely many steps, and so such a proof can only use finitely many of the new axioms. But we've already proven you can't derive a contradiction using only finitely many of the axioms.
However, it's not at all obvious how to go about constructing a set that could be a model of such a theory. (at least, not until you've seen the idea of ultrapowers)

It may be useful to know that second-order logic is not complete in this sense, if we require models of a second-order theories to have the property that the (second-order) type of all subtypes of $X$ be interpreted as the power set of the interpretation of $X$. 
This can be interpreted as saying that the rules for doing proofs in second-order logic are not powerful enough to prove all things that must be true in all ZFC-set-theoretic models of a second-order theory.
