Compactness Theorem for First Order Logic - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-25T17:33:35Z http://mathoverflow.net/feeds/question/45487 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/45487/compactness-theorem-for-first-order-logic Compactness Theorem for First Order Logic Eran 2010-11-09T21:47:10Z 2010-11-21T14:49:45Z <p>Hi all, I am interested in proofs without using Goedel's completeness theorem.</p> <ul> <li>Does anyone have a reference to a proof of this theorem that uses Skolem Functions?</li> <li>How come Enderton's (Introduction to Logic) has a half a page proof (which looks OK to me) and Boolos (Computability And Logic) has a full chapter of it?</li> </ul> <p>Thanks.</p> http://mathoverflow.net/questions/45487/compactness-theorem-for-first-order-logic/45490#45490 Answer by Pete L. Clark for Compactness Theorem for First Order Logic Pete L. Clark 2010-11-09T22:10:29Z 2010-11-09T22:10:29Z <p>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</p> <p><a href="http://www.math.uga.edu/~pete/modeltheory2010Chapter6.pdf" rel="nofollow">http://www.math.uga.edu/~pete/modeltheory2010Chapter6.pdf</a></p> http://mathoverflow.net/questions/45487/compactness-theorem-for-first-order-logic/45498#45498 Answer by Andreas Blass for Compactness Theorem for First Order Logic Andreas Blass 2010-11-09T23:47:19Z 2010-11-09T23:47:19Z <p>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.</p> <p>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$.</p> http://mathoverflow.net/questions/45487/compactness-theorem-for-first-order-logic/45500#45500 Answer by Andres Caicedo for Compactness Theorem for First Order Logic Andres Caicedo 2010-11-09T23:59:07Z 2010-11-09T23:59:07Z <p>There is a nice recent book by Richard Kaye, <strong>The mathematics of logic</strong> (Cambridge, 2007). </p> <p>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. </p> <p>Some of the exercises (from the very beginning) are challenging. I found it a very nice introduction to the topic. </p> http://mathoverflow.net/questions/45487/compactness-theorem-for-first-order-logic/45501#45501 Answer by Joel David Hamkins for Compactness Theorem for First Order Logic Joel David Hamkins 2010-11-10T00:20:42Z 2010-11-10T18:37:42Z <p>There are indeed many proofs of the Compactness theorem. As I mention in <a href="http://mathoverflow.net/questions/9309/in-model-theory-does-compactness-easily-imply-completeness/9317#9317" rel="nofollow">this MO answer</a>, 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.</p> <p>The <a href="http://en.wikipedia.org/wiki/Compactness_theorem" rel="nofollow">Compactness Theorem</a> is the assertion that if a first order theory $T$ is finitely satisfiable (all finite subtheories have a model), then $T$ itself is satisfiable.</p> <p>Let me describe a number of proofs.</p> <ul> <li><p>Goedel's original proof was via the <a href="http://en.wikipedia.org/wiki/Completeness_theorem" rel="nofollow">Completeness theorem</a>, 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.</p></li> <li><p>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.</p></li> <li><p>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.</p></li> <li><p>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.</p></li> <li><p>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.</p></li> <li><p>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.</p></li> </ul> http://mathoverflow.net/questions/45487/compactness-theorem-for-first-order-logic/45559#45559 Answer by Buschi Sergio for Compactness Theorem for First Order Logic Buschi Sergio 2010-11-10T15:19:25Z 2010-11-10T15:19:25Z <p>A Category Theory Book:</p> <p>Locally Presentable and Accessible Categories, J. Adamek and J. Rosicky, Cambridge University Press (LMM 189)</p> <p>See p. 215 </p> http://mathoverflow.net/questions/45487/compactness-theorem-for-first-order-logic/45579#45579 Answer by Michael Hardy for Compactness Theorem for First Order Logic Michael Hardy 2010-11-10T18:15:54Z 2010-11-21T00:34:19Z <p>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: <code>$$m(A) = \begin{cases} 1 &amp; \text{if }A \in F, \\ 0 &amp; \text{if }I \setminus A \in F \\ \text{undefined} &amp; \text{otherwise} \end{cases}$$</code> 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.)</p> http://mathoverflow.net/questions/45487/compactness-theorem-for-first-order-logic/46824#46824 Answer by Sergei Tropanets for Compactness Theorem for First Order Logic Sergei Tropanets 2010-11-21T14:49:45Z 2010-11-21T14:49:45Z <p>See David Marker's "Model theory. An introduction." Although argument is model theoretic, you can easily transform it into syntactic one.</p>