Hi all, I am interested in proofs without using Goedel's completeness theorem.
Thanks.
There's a proof of compactness using Skolem functions in the book "Elements of Mathematical Logic. Model Theory" by Kreisel and Krivine. (I'm assuming here that the English version matches the French, because the latter is the one I checked.) It presupposes the compactness theorem for propositional logic.
The proof runs as follows: Given a finitely satisfiable set $S$ of formulas, Skolemize them to get a set $S'$ of universal formulas that is satisfiable if and only if $S$ is. (Technical detail: If the vocabulary has no constant symbols, adjoin one, so that there are some closed terms for use in the next step.) Let $S''$ be the set of all the formulas you get from those in $S'$ by deleting the universal quantifiers and replacing the variables by closed terms in all possible ways. The formulas in $S''$ are propositional combinations of atomic sentences; by regarding the atomic sentences as propositional variables, we can view $S''$ as a set of formulas of propositional logic. Finite satisfiability of $S$ (in the sense of first-order logic) implies finite satisfiability of $S''$ (in the sense of propositional logic). By propositional compactness, there is a truth assignment satisfying $S''$. That truth assignment amounts to a description of a structure (in the first-order sense) in which every element is the value of some closed term. This structure satisfies $S'$ and therefore $S$.
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.
The Compactness Theorem is the assertion that if a first order theory $T$ is finitely satisfiable (all finite subtheories have a model), then $T$ itself is satisfiable.
Let me describe a number of proofs.
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.
One standard modern approach is to prove the Compactness Theorem using ultraproducts. I did so at the end of a short summer course on model theory: see
There is a nice recent book by Richard Kaye, The mathematics of logic (Cambridge, 2007).
The book is centered around the completeness theorem, and treats different versions, while developing the required set theoretic and logical background along the way. It begins with a treatment of König's lemma. Then develops a "toy version" of a proof calculus, that introduces the idea of completeness of a proof system. This toy version is designed to require only König's lemma. Additional choice is added to the picture as the proof system grows (so we see Boolean algebras and then propositional calculus, Tychonov's theorem and then first-order logic). Compactness is presented topologically but not in terms of ultraproducts.
Some of the exercises (from the very beginning) are challenging. I found it a very nice introduction to the topic.
For some reason I like stating the ultraproduct proof of the compactness theorem in measure-theoretic language, as follows. A filter $F$ on the index set $I$ corresponds to a "finitely additive measure", like this: $$ m(A) = \begin{cases} 1 & \text{if }A \in F, \\ 0 & \text{if }I \setminus A \in F \\ \text{undefined} & \text{otherwise} \end{cases} $$ A filter is an ultrafilter if the "otherwise" case is vacuous. Then \Los's theorem says a first-order statement in the language of the model is true in the ultraproduct if and only if it's true in "almost all" of the factors. (Then as others noted above, let $I$ be the set of finite subsets of the set of statements you're trying to satisfy; let $F$ be an ultrafilter that contains every co-finite set (one exists if you believe in Zorn's lemma); then for each $i \in I$ let the $i$th factor be a model that satisfies that finite set of statements; then prove by induction on the formation of first-order formulas that the ultraproduct satisfies all of the statements. As far as I know you have to include formulas with free variables in the proof to make the induction work. I'm skipping the details since others seem to have gone into those above.)
A Category Theory Book:
Locally Presentable and Accessible Categories, J. Adamek and J. Rosicky, Cambridge University Press (LMM 189)
See p. 215
See David Marker's "Model theory. An introduction." Although argument is model theoretic, you can easily transform it into syntactic one.
