Editing Compactness theorem (section)

==Proofs==

One can prove the compactness theorem using [[Gödel's completeness theorem]], which establishes that a set of sentences is satisfiable if and only if no contradiction can be proven from it.  Since [[mathematical proof|proof]]s are always finite and therefore involve only finitely many of the given sentences, the compactness theorem follows.  In fact, the compactness theorem is equivalent to Gödel's completeness theorem, and both are equivalent to the [[Boolean prime ideal theorem]], a weak form of the [[axiom of choice]].<ref>See Hodges (1993).</ref>

Gödel originally proved the compactness theorem in just this way, but later some "purely semantic" proofs of the compactness theorem were found; that is, proofs that refer to {{em|truth}} but not to {{em|provability}}.  One of those proofs relies on [[ultraproduct]]s hinging on the axiom of choice as follows:

'''Proof''': 
Fix a first-order language <math>L,</math> and let <math>\Sigma</math>  be a collection of <math>L</math>-sentences such that every finite subcollection of <math>L</math>-sentences, <math>i \subseteq \Sigma</math> of it has a model <math>\mathcal{M}_i.</math>  Also let <math display=inline>\prod_{i \subseteq \Sigma}\mathcal{M}_i</math> be the direct product of the structures and <math>I</math> be the collection of finite subsets of <math>\Sigma.</math> For each <math>i \in I,</math> let <math>A_i = \{j \in I : j \supseteq i\}.</math> 
The family of all of these sets <math>A_i</math> generates a proper [[Filter (set theory)|filter]], so there is an [[Ultrafilter (set theory)|ultrafilter]] <math>U</math> containing all sets of the form <math>A_i.</math>

Now for any sentence <math>\varphi</math> in <math>\Sigma:</math>
* the set <math>A_{\{\varphi\}}</math> is in <math>U</math>
* whenever <math>j \in A_{\{\varphi\}},</math> then <math>\varphi \in j,</math> hence <math>\varphi</math> holds in <math>\mathcal M_j</math>
* the set of all <math>j</math> with the property that <math>\varphi</math> holds in  <math>\mathcal M_j</math> is a superset of <math>A_{\{\varphi\}},</math> hence also in <math>U</math>
[[Ultraproduct#Łoś's theorem|Łoś's theorem]] now implies that <math>\varphi</math> holds in the [[ultraproduct]] <math display=inline>\prod_{i \subseteq \Sigma} \mathcal{M}_i/U.</math>  So this ultraproduct satisfies all formulas in <math>\Sigma.</math>