creating an infinite model

From the syntactic compactness theorem for first order logic, we get this nice (and useful) result:

Let T be a theory of first-order logic. If T has finite models of unboundedly large sizes, then T also has an infinite model.

Proof.

Define the propositions

$${\mathrm{\Phi }}_n\equiv \underset{¯}{\exists x_1\mathrm{\cdots }\exists x_n.(x_1\ne x_2)\wedge \mathrm{\cdots }\wedge (x_1\ne x_n)\wedge (x_2\ne x_3)\wedge \mathrm{\cdots }\wedge (x_{n-1}\ne x_n)}$$

(${\mathrm{\Phi }}_n$ says “there exist (at least) $n$ different elements in the world”). Note that

$$\mathrm{\cdots }⊢{\mathrm{\Phi }}_n⊢\mathrm{\cdots }⊢{\mathrm{\Phi }}_2⊢{\mathrm{\Phi }}_1.$$

Define a new theory

$${\text{𝐓}}_{\mathrm{\infty }}=\text{𝐓}\cup \{{\mathrm{\Phi }}_1,{\mathrm{\Phi }}_2,\mathrm{\dots }\}.$$

For any finite subset ${\text{𝐓}}^{\prime }\subset {\text{𝐓}}_{\mathrm{\infty }}$, we claim that ${\text{𝐓}}^{\prime }$ is consistent: Indeed, ${\text{𝐓}}^{\prime }$ contains axioms of T, along with finitely many of ${\left\{{\mathrm{\Phi }}_n\right\}}_{n\ge 1}$. Let ${\mathrm{\Phi }}_m$ correspond to the largest index appearing in ${\text{𝐓}}^{\prime }$. If ${ℳ}_m\vDash \text{𝐓}$ is a model of T with at least $m$ elements (and by hypothesis, such as model exists), then ${ℳ}_m\vDash \text{𝐓}\cup \{{\mathrm{\Phi }}_m\}⊢{\text{𝐓}}^{\prime }$.

So every finite subset of ${\text{𝐓}}_{\mathrm{\infty }}$ is consistent; by the compactness theorem for first-order logic, ${\text{𝐓}}_{\mathrm{\infty }}$ is consistent, and by Gödel’s completeness theorem for first-order logic it has a model $ℳ$. Then $ℳ\vDash {\text{𝐓}}_{\mathrm{\infty }}⊢\text{𝐓}$, so $ℳ$ is a model of T with infinitely many elements ($ℳ\vDash {\mathrm{\Phi }}_n$ for any $n$, so $ℳ$ has at least $\ge n$ elements for all $n$). ∎

Title	creating an infinite model
Canonical name	CreatingAnInfiniteModel
Date of creation	2013-03-22 12:44:29
Last modified on	2013-03-22 12:44:29
Owner	CWoo (3771)
Last modified by	CWoo (3771)
Numerical id	9
Author	CWoo (3771)
Entry type	Example
Classification	msc 03B10
Classification	msc 03C07
Related topic	CompactnessTheoremForFirstOrderLogic
Related topic	GettingModelsIModelsConstructedFromConstants