[proofplan] We enlarge $T$ by adding, for each natural number $n$, a first-order sentence asserting that the universe has at least $n$ distinct elements. Every finite part of this enlarged theory mentions only finitely many such lower-bound sentences, so the hypothesis of arbitrarily large finite models provides a model for that finite part. By the [compactness theorem for first-order logic](/theorems/4290), the entire enlarged theory has a model. Since that model satisfies the sentence “there are at least $n$ elements” for every $n \in \mathbb{N}$, its universe cannot be finite. [/proofplan] [step:Add first-order lower-bound sentences to the theory] For each $n \in \mathbb{N}$, define the $\mathcal{L}$-sentence $\varphi_n$ by \begin{align*} \varphi_n := \exists x_1 \cdots \exists x_n \bigwedge_{1 \leq i < j \leq n} x_i \neq x_j . \end{align*} Thus an $\mathcal{L}$-structure $\mathcal{A}$ satisfies $\varphi_n$ exactly when $|\mathcal{A}| \geq n$. Define the enlarged $\mathcal{L}$-theory $T^*$ by \begin{align*} T^* := T \cup \{\varphi_n : n \in \mathbb{N}\}. \end{align*} [guided] We want to force a model of $T$ to be infinite using only first-order sentences. First-order logic cannot express “the universe is infinite” by a single sentence, but it can express every finite lower bound on the size of the universe. For each $n \in \mathbb{N}$, define the $\mathcal{L}$-sentence \begin{align*} \varphi_n := \exists x_1 \cdots \exists x_n \bigwedge_{1 \leq i < j \leq n} x_i \neq x_j . \end{align*} The variables $x_1,\dots,x_n$ are required to be pairwise distinct, so an $\mathcal{L}$-structure $\mathcal{A}$ satisfies $\varphi_n$ exactly when its universe has at least $n$ elements. Now define \begin{align*} T^* := T \cup \{\varphi_n : n \in \mathbb{N}\}. \end{align*} A model of $T^*$ is therefore a model of $T$ whose universe has at least $n$ elements for every $n \in \mathbb{N}$. [/guided] [/step] [step:Verify finite satisfiability of the enlarged theory] Let $\Delta \subset T^*$ be finite. Since $\Delta$ contains only finitely many of the sentences $\varphi_n$, define \begin{align*} N := \max\bigl(\{1\} \cup \{n \in \mathbb{N} : \varphi_n \in \Delta\}\bigr). \end{align*} By hypothesis, there exists a finite $\mathcal{L}$-structure $\mathcal{M}_N$ such that $\mathcal{M}_N \models T$ and $|\mathcal{M}_N| \geq N$. Since $\Delta \cap T \subseteq T$, we have $\mathcal{M}_N \models \Delta \cap T$. Also, if $\varphi_n \in \Delta$, then $n \leq N$, so $|\mathcal{M}_N| \geq N \geq n$, and hence $\mathcal{M}_N \models \varphi_n$. Therefore $\mathcal{M}_N \models \Delta$. Thus every finite subset of $T^*$ is satisfiable. [guided] To apply compactness, we must prove that every finite subset of $T^*$ has a model. Let $\Delta \subset T^*$ be finite. The set $\Delta$ may contain some sentences from $T$ and some lower-bound sentences $\varphi_n$, but only finitely many of the latter. Define \begin{align*} N := \max\bigl(\{1\} \cup \{n \in \mathbb{N} : \varphi_n \in \Delta\}\bigr). \end{align*} The extra $\{1\}$ ensures that $N$ is defined even if $\Delta$ contains no sentence of the form $\varphi_n$. By the hypothesis of arbitrarily large finite models, there exists a finite $\mathcal{L}$-structure $\mathcal{M}_N$ such that \begin{align*} \mathcal{M}_N \models T \quad\text{and}\quad |\mathcal{M}_N| \geq N. \end{align*} Since every sentence of $\Delta \cap T$ belongs to $T$, the relation $\mathcal{M}_N \models T$ implies $\mathcal{M}_N \models \Delta \cap T$. Now take any lower-bound sentence $\varphi_n \in \Delta$. By the definition of $N$, we have $n \leq N$. Since $|\mathcal{M}_N| \geq N$, it follows that $|\mathcal{M}_N| \geq n$, so $\mathcal{M}_N \models \varphi_n$. Hence $\mathcal{M}_N$ satisfies every sentence in $\Delta$. Therefore every finite subset $\Delta \subset T^*$ is satisfiable. [/guided] [/step] [step:Apply compactness to obtain a model satisfying all finite lower bounds] Since every finite subset of $T^*$ is satisfiable, the [compactness theorem](/theorems/2748) for first-order logic applies to $T^*$ and yields an $\mathcal{L}$-structure $\mathcal{M}$ such that $\mathcal{M} \models T^*$ (citing a result not yet in the wiki: Compactness Theorem for First-Order Logic). Because $T \subseteq T^*$, we have $\mathcal{M} \models T$. [guided] The compactness theorem for first-order logic says that if every finite subset of a first-order theory is satisfiable, then the whole theory is satisfiable. We verified the hypothesis in the previous step: every finite subset of $T^*$ has a model. Applying compactness to the $\mathcal{L}$-theory $T^*$ gives an $\mathcal{L}$-structure $\mathcal{M}$ such that \begin{align*} \mathcal{M} \models T^* . \end{align*} This invocation uses the compactness theorem itself as the external model-theoretic ingredient (citing a result not yet in the wiki: Compactness Theorem for First-Order Logic). Since $T \subseteq T^*$, every model of $T^*$ is automatically a model of $T$. Therefore \begin{align*} \mathcal{M} \models T . \end{align*} [/guided] [/step] [step:Show that the compactness model is infinite] For every $n \in \mathbb{N}$, the sentence $\varphi_n$ belongs to $T^*$, so $\mathcal{M} \models \varphi_n$. Hence $|\mathcal{M}| \geq n$ for every $n \in \mathbb{N}$. If $\mathcal{M}$ were finite, say $|\mathcal{M}| = m$ for some $m \in \mathbb{N}$, then $\mathcal{M} \not\models \varphi_{m+1}$, contradicting $\mathcal{M} \models T^*$. Therefore $\mathcal{M}$ is infinite. Thus $T$ has an infinite model. [/step]