models constructed from constants
The definition of a structure^{} and of the satisfaction relation is nice, but it raises the following question : how do we get models in the first place? The most basic construction for models of firstorder theory is the construction that uses constants. Throughout this entry, $L$ is a fixed firstorder language.
Let $C$ be a set of constant symbols of $L$, and $T$ be a theory in $L$. Then we say $C$ is a set of witnesses for $T$ if and only if for every formula $\phi $ with at most one free variable^{} $x$, we have $T\u22a2\exists x(\phi )\Rightarrow \phi (c)$ for some $c\in C$.
Lemma. Let $T$ is any consistent set of sentences^{} of $L$, and $C$ is a set of new symbols such that $C=L$. Let ${L}^{\prime}=L\cup C$. Then there is a consistent set ${T}^{\prime}\subseteq {L}^{\prime}$ extending $T$ and which has $C$ as set of witnesses.
Lemma. If $T$ is a consistent^{} theory in $L$, and $C$ is a set of witnesses for $T$ in $L$, then $T$ has a model whose elements are the constants in $C$.
Proof: Let $\mathrm{\Sigma}$ be the signature^{} for $L$. If $T$ is a consistent set of sentences of $L$, then there is a maximal consistent ${T}^{\prime}\supseteq T$. Note that ${T}^{\prime}$ and $T$ have the same sets of witnesses. As every model of ${T}^{\prime}$ is also a model of $T$, we may assume $T$ is maximal consistent.
We let the universe^{} of $\U0001d510$ be the set of equivalence classes^{} $C/\sim $, where $a\sim b$ if and only if $\text{\u201c}a=b\text{\u201d}\in T$. As $T$ is maximal consistent, this is an equivalence relation. We interpret the nonlogical symbols as follows :

1.
$[a]{=}^{\U0001d510}[b]$ if and only if $a\sim b$;

2.
Constant symbols are interpreted in the obvious way, i.e. if $c\in \mathrm{\Sigma}$ is a constant symbol, then ${c}^{\U0001d510}=[c]$;

3.
If $R\in \mathrm{\Sigma}$ is an $n$ary relation symbol, then $([{a}_{1}],\mathrm{\dots},[{a}_{n}])\in {R}^{\U0001d510}$ if and only if $R({a}_{1},\mathrm{\dots},{a}_{n})\in T$;

4.
If $F\in \mathrm{\Sigma}$ is an $n$any function symbol, then ${F}^{\U0001d510}([{a}_{0}],\mathrm{\dots},[{a}_{n}])=[b]$ if and only if $\text{\u201c}F({a}_{1},\mathrm{\dots},{a}_{n})=b\text{\u201d}\in T$.
From the fact that $T$ is maximal consistent, and $\sim $ is an equivalence relation, we get that the operations^{} are welldefined (it is not so simple, i’ll write it out later). The proof that $\U0001d510\vDash T$ is a straightforward induction^{} on the complexity of the formulas of $T$. $\mathrm{\u2662}$
Corollary. (The extended completeness theorem) A set $T$ of formulas of $L$ is consistent if and only if it has a model (regardless of whether or not $L$ has witnesses for $T$).
Proof: First add a set $C$ of new constants to $L$, and expand $T$ to ${T}^{\prime}$ in such a way that $C$ is a set of witnesses for ${T}^{\prime}$. Then expand ${T}^{\prime}$ to a maximal consistent set ${T}^{\prime \prime}$. This set has a model $\U0001d510$ consisting of the constants in $C$, and $\U0001d510$ is also a model of $T$. $\mathrm{\u2662}$
Corollary. (Compactness theorem) A set $T$ of sentences of $L$ has a model if and only if every finite subset of $T$ has a model.
Proof: Replace “has a model” by “is consistent”, and apply the syntactic compactness theorem. $\mathrm{\u2662}$
Corollary. (Gödel’s completeness theorem) Let $T$ be a consistent set of formulas of $L$. Then A sentence $\phi $ is a theorem of $T$ if and only if it is true in every model of $T$.
Proof: If $\phi $ is not a theorem of $T$, then $\mathrm{\neg}\phi $ is consistent with $T$, so $T\cup \{\mathrm{\neg}\phi \}$ has a model $\U0001d510$, in which $\phi $ cannot be true. $\mathrm{\u2662}$
Corollary. (Downward LöwenheimSkolem theorem) If $T\subseteq L$ has a model, then it has a model of power at most $L$.
Proof: If $T$ has a model, then it is consistent. The model constructed from constants has power at most $L$ (because we must add at most $L$ many new constants). $\mathrm{\u2662}$
Most of the treatment found in this entry can be read in more details in Chang and Keisler’s book Model Theory^{}.
Title  models constructed from constants 

Canonical name  ModelsConstructedFromConstants 
Date of creation  20130322 12:44:42 
Last modified on  20130322 12:44:42 
Owner  ratboy (4018) 
Last modified by  ratboy (4018) 
Numerical id  17 
Author  ratboy (4018) 
Entry type  Definition 
Classification  msc 03C07 
Synonym  completeness theorem 
Synonym  Gödel completeness theorem 
Related topic  UpwardsSkolemLowenheimTheorem 
Defines  set of witnesses 