Return to Answer

There are indeed many proofs of the Compactness theorem. As I mention in this MO answer, when I was a graduate student Leo Harrington told me that he used a different proof method for Compactness each time he taught the introductory graduate logic course in Berkeley. I am not sure for how many semesters he was able to keep this up, but when I had him, it was time for the Boolean-valued models proof.

There are indeed many proofs of the Compactness theorem. As I mention in this MO answer, when I was a graduate student Leo Harrington told me that he used a different proof method for Compactness each time he taught the introductory graduate logic course in Berkeley. I am not sure for how many semesters he was able to keep this up, but when I had him, it was time for the Boolean-valued models proof.

• Goedel's original proof was via the Completeness theorem, deducing it as a trivial corollary. If $T$ is inconsistent, then the proof of a contradiction is finite, so there is an inconsistent finite subtheory. This proof is deprecated by contemporary logicians, because the Compactness theorem lies completely on the semantic side of the syntax/semantic divide, and it seems beside the point to have to develop the entire syntactic theory of formal proofs and derivations in order to make a conclusion purely about the semantic notions of models and satisfiability.

• The Henkin proof. The point is that the usual Henkin proof of the Completeness theorem also serves directly to prove the Compactness theorem. Suppose that every finite subset of $T$ is satisfiable. By the usual details of the Henkin argument, we may extend $T$ to a finitely-satisfiable complete Henkin theory $T^+$, in a language with new constant symbols (using the theorem on constants). That is, the new theory contains the Henkin assertions $\exists x\varphi(x)\to \varphi(c)$, where $c$ is a new constant symbol added for this purpose with $\varphi$. Now, from $T^+$ we may build a model out of the Henkin constants in the usual manner. The reduct of this model to the original language satisfies $T$, as desired.

• The proof via Skolem functions (as you requested). This amounts basically just to a more complicated version of the Henkin proof. I recall Henkin giving a talk at the Berkeley Logic Colloquium in which he explained that the idea for his proof of the Completeness theorem arose to him in a dream, after considering the (at that time standard) Skolem function proof of Completeness. The point was that in that proof, one adds Skolem functions to the language to tie the formula $\varphi(x)$ to the witness $f_\varphi(x)$, so that one adds the formulas $\forall \vec y, x[\varphi(x)\to \varphi(f_\varphi(\vec y))]$, instead of the Henkin assertion (this amounts to the quantifer-reducing idea mentioned by Andreas). But otherwise, it works out similarly---one proves the analogue of the theorem on constants that allows one to add the Skolem function assertions, and then builds the model out of formal term expressions. Henkin said that he realized in his dream that there was no need to tie the witness so closely to the formula with the Skolem function, and that merely having the presence of a constant to serve as a witness sufficed. Thus was born the Henkin proof.

• The ultrapower proof. Pete has an explanation of this proof in his answer. If $T$ is finitely satisfiable, then consider the set of finite subsets $t\subset T$, each of which has a model $M_t\models t$. Let $F$ be an ultrafilter containing for each $\varphi\in T$ the set of finite $t\subset T$ with $\varphi\in t$, a collection with the finite intersection property. The ultrapower of $\Pi_t M_t/F$ satisfies every $\varphi\in T$ by \L os's theorem.

• The reduced product proof. In this proof, one first develops the concept of a reduced product $\Pi_t M_t/F_0$, where $F_0$ is only a filter instead of an ultrafilter (the filter generated by the collection with FIP above). And then you can finish the job by considering a quotient of this structure, which essentially amounts to the ultraproduct.

• The Boolean-valued model proof. It is similar to the ultrapower proof and the reduced power proof (they are all essentially the same), but there is no need to quotient out by $F$ in advance. Instead, one builds a $\mathbb{B}$-valued model out of the product ${\cal M}=\Pi_t M_t$, where $\mathbb{B}$ is the Boolean algebra of all subsets of finite subsets of $T$, so that the truth-value of a statement $\varphi$ in $\cal M$ is the set of $t$ for which $M_t\models \varphi$. Then, one develops the general theory allowing one to quotient a Boolean-valued model by a filter, and the conclusion amounts to \L os in the ultrapower proof.

• Goedel's original proof was via the Completeness theorem, deducing it as a trivial corollary. If $T$ is inconsistent, then the proof of a contradiction is finite, so there is an inconsistent finite subtheory. This proof is deprecated by contemporary logicians, because the Compactness theorem lies completely on the semantic side of the syntax/semantic divide, and it seems beside the point to have to develop the entire syntactic theory of formal proofs and derivations in order to make a conclusion purely about the semantic notions of models and satisfiability.

• The Henkin proof. The point is that the usual Henkin proof of the Completeness theorem also serves directly to prove the Compactness theorem. Suppose that every finite subset of $T$ is satisfiable. By the usual details of the Henkin argument, we may extend $T$ to a finitely-satisfiable complete Henkin theory $T^+$, in a language with new constant symbols (using the theorem on constants). That is, the new theory contains the Henkin assertions $\exists x\varphi(x)\to \varphi(c)$, where $c$ is a new constant symbol added for this purpose with $\varphi$. Now, from $T^+$ we may build a model out of the Henkin constants in the usual manner. The reduct of this model to the original language satisfies $T$, as desired.

• The proof via Skolem functions (as you requested). This amounts basically just to a more complicated version of the Henkin proof. I recall Henkin giving a talk at the Berkeley Logic Colloquium in which he explained that the idea for his proof of the Completeness theorem arose to him in a dream, after considering the (at that time standard) Skolem function proof of Completeness. The point was that in that proof, one adds Skolem functions to the language to tie the formula $\varphi(x)$ to the witness $f_\varphi(x)$, so that one adds the formulas $\forall \vec y, x[\varphi(x)\to \varphi(f_\varphi(\vec y))]$, instead of the Henkin assertion (this amounts to the quantifer-reducing idea mentioned by Andreas). But otherwise, it works out similarly---one proves the analogue of the theorem on constants that allows one to add the Skolem function assertions, and then builds the model out of formal term expressions. Henkin said that he realized in his dream that there was no need to tie the witness so closely to the formula with the Skolem function, and that merely having the presence of a constant to serve as a witness sufficed. Thus was born the Henkin proof.

• The ultraproduct proof. Pete has an explanation of this proof in his answer. If $T$ is finitely satisfiable, then consider the set of finite subsets $t\subset T$, each of which has a model $M_t\models t$. Let $F$ be an ultrafilter containing for each $\varphi\in T$ the set of finite $t\subset T$ with $\varphi\in t$, a collection with the finite intersection property. The ultraproduct $\Pi_t M_t/F$ satisfies every $\varphi\in T$ by \L os's theorem.

• The reduced product proof. In this proof, one first develops the concept of a reduced product $\Pi_t M_t/F_0$, where $F_0$ is only a filter instead of an ultrafilter (the filter generated by the collection with FIP above). And then you can finish the job by considering a quotient of this structure, which essentially amounts to the ultraproduct.

• The Boolean-valued model proof. It is similar to the ultraproduct proof and the reduced product proof (they are all essentially the same), but there is no need to quotient out by $F$ in advance. Instead, one builds a $\mathbb{B}$-valued model out of the product ${\cal M}=\Pi_t M_t$, where $\mathbb{B}$ is the Boolean algebra of all subsets of finite subsets of $T$, so that the truth-value of a statement $\varphi$ in $\cal M$ is the set of $t$ for which $M_t\models \varphi$. Then, one develops the general theory allowing one to quotient a Boolean-valued model by a filter, and the conclusion amounts to \L os in the ultraproduct proof.

There are indeed many proofs of the Compactness theorem. As I mention in this MO answer, my graduate experience was with Leo Harrington, who announced to the class that he used a different proof method for Compactness each time he taught the introductory graduate logic course in Berkeley. I am not sure for how many semesters he was able to keep this up, but when I had him, it was time for the Boolean-valued models proof.

• Goedel's original proof was via the Completeness theorem, deducing it as a trivial corollary. If $T$ is inconsistent, then the proof of a contradiction is finite, so there is an inconsistent finite subtheory. This proof is deprecated by contemporary logicians, because the Compactness theorem lies completely on the semantic side of the syntax/semantic divide, and it seems beside the point to have to develop the entire syntactic theory of formal proofs and derivations in order to make a conclusion purely about the semantic notions of models and satisfiability.

• The Henkin proof. The point is that the usual Henkin proof of the Completeness theorem also serves directly to prove the Compactness theorem. Suppose that every finite subset of $T$ is satisfiable. By the usual details of the Henkin argument, we may extend $T$ to a finitely-satisfiable complete consistent Henkin theory $T^+$, in a language with new constant symbols (using the theorem on constants). That is, the new theory contains the Henkin assertions $\exists x\varphi(x)\to \varphi(c)$, where $c$ is a new constant symbol added for this purpose with $\varphi$. Now, from $T^+$ we may build a model out of the Henkin constants in the usual manner. The reduct of this model to the original language satisfies $T$, as desired.

• The proof via Skolem functions (as you requested). This amounts basically just to a more complicated version of the Henkin proof. I recall Henkin giving a talk at the Berkeley Logic Colloquium in which he explained that the idea for his proof of the Completeness theorem arose to him in a dream, after considering the (at that time standard) Skolem function proof of Completeness. The point was that in that proof, one adds Skolem functions to the language to tie the formula $\varphi(x)$ to the witness $f_\varphi(x)$, so that one adds the formulas $\forall \vec y, x[\varphi(x)\to \varphi(f_\varphi(\vec y))]$, instead of the Henkin assertion (this amounts to the quantifer-reducing idea mentioned by Andreas). But otherwise, it works out similarly---one proves the analogue of the theorem on constants that allows one to add the Skolem function assertions, and then builds the model out of formal term expressions. Henkin said that he realized in his dream that there was no need to tie the witness so closely to the formula with the Skolem function, and that merely having the presence of a constant to serve as a witness sufficed. Thus was born the Henkin proof.

• The ultrapower proof. Pete has an explanation of this proof in his answer. If $T$ is finitely satisfiable, then consider the set of finite subsets $t\subset T$, each of which has a model $M_t\models t$. Let $F$ be an ultrafilter containing for each $\varphi\in T$ the set of finite $t\subset T$ with $\varphi\in t$, a collection with the finite intersection property. The ultrapower of $\Pi_t M_t/F$ satisfies every $\varphi\in T$ by \L os's theorem.

• The reduced product proof. In this proof, one first develops the concept of a reduced product $\Pi_t M_t/F_0$, where $F_0$ is only a filter instead of an ultrafilter (the filter generated by the collection with FIP above). And then you can finish the job by considering a quotient of this structure, which essentially amounts to the ultraproduct.

• The Boolean-valued model proof. It is similar to the ultrapower proof and the reduced power proof (they are all essentially the same), but there is no need to quotient out by $F$ in advance. Instead, one builds a $\mathbb{B}$-valued model out of the product ${\cal M}=\Pi_t M_t$, where $\mathbb{B}$ is the Boolean algebra of all subsets of finite subsets of $T$, so that the truth-value of a statement $\varphi$ in $\cal M$ is the set of $t$ for which $M_t\models \varphi$. Then, one develops the general theory allowing one to quotient a Boolean-valued model by a filter, and the conclusion amounts to \L os in the ultrapower proof.

There are indeed many proofs of the Compactness theorem. As I mention in this MO answer, when I was a graduate student Leo Harrington told me that he used a different proof method for Compactness each time he taught the introductory graduate logic course in Berkeley. I am not sure for how many semesters he was able to keep this up, but when I had him, it was time for the Boolean-valued models proof.

• Goedel's original proof was via the Completeness theorem, deducing it as a trivial corollary. If $T$ is inconsistent, then the proof of a contradiction is finite, so there is an inconsistent finite subtheory. This proof is deprecated by contemporary logicians, because the Compactness theorem lies completely on the semantic side of the syntax/semantic divide, and it seems beside the point to have to develop the entire syntactic theory of formal proofs and derivations in order to make a conclusion purely about the semantic notions of models and satisfiability.

• The Henkin proof. The point is that the usual Henkin proof of the Completeness theorem also serves directly to prove the Compactness theorem. Suppose that every finite subset of $T$ is satisfiable. By the usual details of the Henkin argument, we may extend $T$ to a finitely-satisfiable complete Henkin theory $T^+$, in a language with new constant symbols (using the theorem on constants). That is, the new theory contains the Henkin assertions $\exists x\varphi(x)\to \varphi(c)$, where $c$ is a new constant symbol added for this purpose with $\varphi$. Now, from $T^+$ we may build a model out of the Henkin constants in the usual manner. The reduct of this model to the original language satisfies $T$, as desired.

• The proof via Skolem functions (as you requested). This amounts basically just to a more complicated version of the Henkin proof. I recall Henkin giving a talk at the Berkeley Logic Colloquium in which he explained that the idea for his proof of the Completeness theorem arose to him in a dream, after considering the (at that time standard) Skolem function proof of Completeness. The point was that in that proof, one adds Skolem functions to the language to tie the formula $\varphi(x)$ to the witness $f_\varphi(x)$, so that one adds the formulas $\forall \vec y, x[\varphi(x)\to \varphi(f_\varphi(\vec y))]$, instead of the Henkin assertion (this amounts to the quantifer-reducing idea mentioned by Andreas). But otherwise, it works out similarly---one proves the analogue of the theorem on constants that allows one to add the Skolem function assertions, and then builds the model out of formal term expressions. Henkin said that he realized in his dream that there was no need to tie the witness so closely to the formula with the Skolem function, and that merely having the presence of a constant to serve as a witness sufficed. Thus was born the Henkin proof.

• The ultrapower proof. Pete has an explanation of this proof in his answer. If $T$ is finitely satisfiable, then consider the set of finite subsets $t\subset T$, each of which has a model $M_t\models t$. Let $F$ be an ultrafilter containing for each $\varphi\in T$ the set of finite $t\subset T$ with $\varphi\in t$, a collection with the finite intersection property. The ultrapower of $\Pi_t M_t/F$ satisfies every $\varphi\in T$ by \L os's theorem.

• The reduced product proof. In this proof, one first develops the concept of a reduced product $\Pi_t M_t/F_0$, where $F_0$ is only a filter instead of an ultrafilter (the filter generated by the collection with FIP above). And then you can finish the job by considering a quotient of this structure, which essentially amounts to the ultraproduct.

• The Boolean-valued model proof. It is similar to the ultrapower proof and the reduced power proof (they are all essentially the same), but there is no need to quotient out by $F$ in advance. Instead, one builds a $\mathbb{B}$-valued model out of the product ${\cal M}=\Pi_t M_t$, where $\mathbb{B}$ is the Boolean algebra of all subsets of finite subsets of $T$, so that the truth-value of a statement $\varphi$ in $\cal M$ is the set of $t$ for which $M_t\models \varphi$. Then, one develops the general theory allowing one to quotient a Boolean-valued model by a filter, and the conclusion amounts to \L os in the ultrapower proof.