Completeness vs Compactness in logic

Question

One standard approach to showing compactness of first-order logic is to show completeness, of which compactness is an easy corollary. I am told this approach is deprecated nowadays, as Compactness is seen as the "deeper" result.

Could someone explain this intuition? In particular, are there logical systems which are compact but not complete?

EDIT: Andreas brings up an excellent point, which is that the Completeness theorem is really a combination of two very important but almost unrelated results. First, the Compactness theorem. Second, the recursive enumerability of logical validities. Note that neither of these results depends on the details on the syntactic or axiomatic system.

What is the connection between these two aspects of completeness? Are there logical systems that have one of these properties but not the other?

Answer 1

The point is that we care about the models, rather than about the proofs. The compactness theorem---the claim that a theory is satisfiable iff every finite subset of it is satisfiable---is fundamentally connected to the models, and the possiblility of truth in these models. To use it, you need to understand your theory, the models of your theory and the models of finite pieces of your theory. And this is what we want to be thinking about and what we know about. In particular, when working with models, we can use all the mathematical tools and constructions at our disposal, with no need to remain inside any first-order language or formal system (well, perhaps we have set theory as our background system). We are free to reason about the models via reducts and ultrapowers and limits of systems of morphisms and so on, using any mathematical method at all.

The completeness theorem, in contrast, is fundamentally connected with the details of a formal deduction system. And so when using it, one is thinking about whether certain tautologies might be provable or not, or whether a certain formal consequence is allowed in the system or not. But when we are studying a certain first-order class of groups or rings or whatever, such details about the proof system might seem to be an irrelevant distraction.

Answer 2

I have two, somewhat conflicting, views on this.

From the point of view of modern model theory, the Compactness Theorem is central to almost everything in the model theory of first order logic, while the Completeness Theorem is almost irrelevant. Completeness comes into play when proving the decidability of complete recursively axiomatized theories or in dealing with recursively saturated models for example, but these are not very central. Even when we want to apply Completeness, what's important is that the set of logical consequences of $T$ is recursively enumerable in $T$--the details of the proof system are of no importance whatsoever. This explains why in my model theory book, while I do explain that Compactness is an almost trivial consequence of Completeness, I give a direct Henkin-style proof.

Nevertheless, I view the Completeness Theorem as one of the great intellectual achievements of our subject. The fact that the semantic notion of "logical consequence" can be captured by the syntactic notion of "proof" is really surprising. The first is, a priori, $\Pi_1$ over the universe of sets, while the second is recursively enumerable. I find this amazing.

Answer 3

In this edit the postcript has been modified.

I will address the the most recent version of the question, which asks about the relationship between the following two features of a logic $L$, but note that a careful discussion of this topic should first clearly define what counts as a logic.

(1) Abstract Completeness of $L$: The set of valid $L$-sentences is recursively/computably enumerable [hereafter: r.e.].

(2) Compactness of $L$: A set $S$ of sentences of $L$ has a model if every finite subset of $S$ has a model.

(1) does not imply (2).

For example, let $Q$ be the quantifier expressing "there are uncountably many", i.e., $Qx\phi(x)$ holds in a structure $\cal{M}$ with universe $M$ iff the set of $m\in M$ such that $\phi(m)$ holds in $\cal{M}$ is uncountable. Let $L_{FO}(Q)$ be the result of augmenting first order logic $L_{FO}$ with the new quantifier $Q$. Vaught proved that the set of valid sentences of $L_{FO}(Q)$ is r.e. Later [1970] in a seminal paper, Keisler gave an elegant axiomatization of $L_{FO}(Q)$.

On the other hand, it is easy to see that $L_{FO}(Q)$ does not satisfy compactness, e.g., for $\alpha < \aleph_1$ introduce constant symbols $c_{\alpha}$ and consider the set $S$ of sentences consisting of $\lnot Qx (x=x)$ [expressing "the universe is not uncountable"] plus sentences of the form $c_{\alpha}\neq c_\beta$ for $\alpha < \beta < \aleph_1$. It is easy to see that every subset of $S$ has a model, but S itself does not have a model.

I should point out that $L_{FO}(Q)$ has a limited form of compactness known as countable compactness: if $S$ is a countable set of sentences of $L_{FO}(Q)$, then S has a model if every finite subset of $S$ has a model [Vaught, ibid].

All of the above features of $L_{FO}(Q)$ [abstractly complete, countably but not fully compact] are shared by a number of other generalized quantifiers, including the stationary quantifier [introduced in the late 1970's and intensely studied in the 1980's]. However, as shown by Shelah, there are other generalized quantifiers that generate fully compact logics that also are abstractly complete

(2) does not imply (1) either.

For example consider the "logic" whose nonlogical symbols are the arithmetical ones, and whose axioms are the usual axioms of first order logic plus all the axioms of true arithmetic , i.e, arithmetical sentences that hold in $\Bbb{N}$. The semantics of the logic is the same as first order logic, so compactness continues to hold; but clearly abstract completeness fails by Tarski's undefinability of truth-theorem, which says that $Th(\Bbb{N})$ is not arithmetical, let alone r.e.

PS A "naturally occurring logic" that also serves to show that (2) does not imply (1) is the existential fragment of second order logic [denoted $ESO$, and which has the same expressive power as "Independence Friendly Logic", see here Section 4.1 of here]. The compactness of $ESO$ follows from the usual proofs of compactness of first order logic [including the ultraproduct proof], but the set of valid sentences $VAL_{ESO}$ of $ESO$ is not even arithmetically definable let alone r.e., since one can "read off" true arithmetic from $VAL_{ESO}$. More specifically, for a sentence $\varphi$ in the language of arithmetic, it is easy to see that $$\mathbb{N}\models \varphi\Leftrightarrow [ \exists X \big( (\mathsf{Q}\land ``~X \mathrm{~is~nonempty~and~has~a~least~element"})\rightarrow \varphi \big)\in VAL_{ESO}].$$ In the above $\mathsf{Q}$ is the conjunction of the finitely many axioms of Robinson arithmetic (Thanks to Noah Schweber for pointing out the argument for nonarithmeticity of $VAL_{ESO}$, and to Rodrigo Freire for catching a blooper; the previous version incorrectly asserted that $VAL_{ESO}$ is co-r.e.).

Answer 4

This is a side comment. There are several answers that explain why compactness is so important in model theory, and I agree with what they say. But I want to point out that the "in model theory" part is key here. In the overall study of logic, not restricted to model theory, both compactness and completeness are important, and each of those has areas of logic that favor it. Model theory, being a semantic field, naturally identifies more with semantic notions.

In mathematics outside logic, I think there is more implicit use of completeness than of compactness. Every time I prove that an identify is derivable from the the axioms of a group by working semantically and showing that the identity holds in every group, I am implicitly using the completeness theorem. It is easy to miss this or take it for granted, because the completeness theorem is so well known.

There are systems that do not have complete deduction systems; one example is second-order logic with full second-order semantics. In this system it is perfectly possible for something to be true in every model without being provable in our usual proof system. Therefore, when we study this system in logic, we have to keep a close watch on whether we have shown something is provable, or just shown that it is logically valid.

Imagine the difficulties in an alternate world where mathematicians have to distinguish between "true in all groups" and "provable from the axioms of a group". The completeness theorem is what lets us ignore this. By comparison, it's more difficult to see reflections of the compactness theorem in everyday mathematics.

Answer 5

Really, compactness is seen as the deeper result? I have to say that I am also more interested in the models rather than formulas and deduction systems, and hence like to teach students proofs of the compactness theorem that do not use the completeness theorem. Typically I prove compactness using ultraproducts.

On the other hand, I still believe that the completeness theorem for first order logic is the most important theorem of mathematical logic.
The theorem tells you that in principle there are computer checkable proofs for all "true" theorems. I know that many mathematicians are not really concerned with having a solid foundation for the concept of a "proof" (you know it when you see it). But having this formal concept of proof in the background helps tremendously when you want to fight off people who present their $n$-th proof of the inconsistency of PA or ZFC, or that there are no infinite sets or that CH holds. Also, the completeness theorem does explain why we can do mathematics the way we do. Even though nobody really writes formal proofs of anything, ever, unless the correctness of the proofs is seriously challenged (see the FLYSPECK project at http://code.google.com/p/flyspeck/).

Also, I think that the proof of the completeness theorem is deeper than of the compactness theorem. In some sense the proof of the completeness theorem (I am thinking of the proof where one builds a canonical model of a maximally consistent Henkin theory) is more straight forward than for example the ultraproduct proof of the compactness theorem, but it is more complicated in the details and certainly less accessible to mainstream mathematics than for instance the ultraproduct proof of the compactness theorem.

Answer 6

Because of my natural inclination toward semantics rather than syntax, I tend to view the completeness theorem (for first-order logic) as being essentially the conjunction of two rather different facts. One is the compactness theorem. The other is the recursive enumerability of the set of valid sentences (say in any finite vocabulary). Both of these facts are often deduced from the completeness theorem, though they can also be proved by other methods (I like a version of Herbrand's theorem that doesn't mention any axioms or rules). But there is also a sort of converse, if one is willing to accept an unorthodox (but in my opinion fairly reasonable) notion of deduction. Namely, fix an algorithm $A$ enumerating the valid sentences, and define a "deduction" of a conclusion $\phi$ from a set $H$ of hypotheses to be a finite conjunction $\eta$ of members of $H$ together with a computation showing that $\eta\to\phi$ is enumerated by $A$. The completeness of this "deductive" system is an immediate consequence of the compactness theorem plus the fact that $A$ enumerates the valid sentences.

Answer 7

Here is an interesting quote from Bruno Poizat's "A Course in Model Theory":

The compactness theorem, in the forms of Theorems 4.5 and 4.6, is due to Gödel; in fact, as explained in the beginning of Section 4.3 [Henkin's Method], the theorem was for Gödel a simple corollary (we could even say an unexpected corollary, a rather strange remark!) of his "completeness theorem" of logic, in which he showed that a finite system of rules of inference is sufficient to express the notion of consequence (see Chapter 7). It could also have been taken from [Herbrand 1928] or [Gentzen 1934], in which results of the same sort were proven.

This unfortunate compactness theorem was brought in by the back door, and we might say that its original modesty still does it wrong in logic textbooks. In my opinion it is a much more essential and primordial (and thus also less sophisticated) than Gödel's completeness theorem, which states that we can formalize deduction in a certain arithmetic way; it is an error in method to deduce it from the latter.

If we do it this way, it is by a very blind fidelity to the historic conditions that witnessed its birth. The weight of this tradition is apparent even in a work like [Chang-Keisler 1973], which was considered a bible of model theory in the 1970s; it begins with syntactic developments that have nothing to do with anything in the succeeding chapters. This approach---deducing Compactness from the possibility of axiomatizing the notion of deduction---once applied to the propositional calculus gives the strangest proof on record of the compactness of $2^\omega$!

It is undoubtedly more "logical," but it is inconvenient, to require the student to absorb a system of formal deduction, ultimately quite arbitrary, which can be justified only much later when we can show that it indeed represents the notion of semantic consequence. We should not lose sight of the fact that the formalisms have no raison d'être except insofar as they are adequate for representing notions of substance.

See also this old answer of mine where the same quote appears.

Answer 8

I was to say that the answers given so far are all wrong and misleading, but thanksfully I recalled that I am not a mathematician :-)

There are mainly two approaches to the concept of "logic".

1. The classical (or mathematical) approach to logic. Roughly speaking, a logic consists of two classes: a set of formulae and a class of models, together with a satisfiability relation saying what formulae are true in what models. Then, we may develop a proof system (or various proof systems) for the logic, which helps us --- in a systematic and coherent way --- derive satisfiability of formulae. Desirable properties of such proof systems are soundness (what we have derived is true), completness (what is true, we can derive). There is also compactness (if something follows a theory then it follows from a finite subset of the theory) that refers to the logic itself (here: satisfiability relation). This is how mathematicians are taught logic.

2. Modern (or computer-scientistic) approach to logic. Logic is a kind of a formal system (deductive system). To help proving facts about such a system, we may introduce the concept of "models" (or various concepts of models) for the logic. Desirable properties of such classes of models are that the deductive system over them is sound and complete (that is --- for a given system --- we develop the appropriate concept of models, such that the proof system is sound and complete; if we add/remove some axioms/rules to the system then we have to restrict/extend our class of models; this is most easily seen in temporal logics --- for example, LTL is sound and complete in linear models). There is also compactness (if something follows a theory then it follows from a finite subset of the theory) that refers to the logic itself (here: proof system; if a logic allows only finitary proofs, then it is obviously compact). Simply, in this approach, the system is fundamental here. This is how computer scientists are taught logic.

Of course, in the presence of soundness and completeness, classical compactness and modern compactness coincide.

So, moving back to your question --- I do agree with other answers saying that completeness and compactness are just far different concepts, so neither is "deeper". However, I do not think that the classification of wht belongs to models and what belongs to proofs is that obvious --- it is just all about how you think of logic.

Answer 9

I think that everything important that can be said about the differences between Compactness and Completeness Theorems and their proofs from the technical point of view has been said. (I also like most the detailed and elucidating answer given by Joel David Hamkins (at In model theory, does compactness easily imply completeness?)). On the other hand, one of the most important differences between these theorems is a non-technical one, and indeed some previous answers contain hints to this effect. Indeed, Completeness Theorem has an obvious metamathematical (or even philosophical) flavour as opposed to Compactness Theorem. Actually, it is about the relation between the two most important mathematical notions, i.e., those of proof and truth.

And here I would like to argue with those (Carl Mummert and Stefan Geschke) who claim that sometimes Completeness Theorem is used in everyday mathematics. Actually, as I see it, it is about everyday mathematics, but it does not belong to everyday mathematics.

Actually, contrary to what Carl Mummert says, I doubt that, in everyday mathematics, anybody in any time uses completeness theorem in either an explicit or implicit way. Obviously, one can successfully work in any field of mathematics (which are not intimately connected to logic) without any knowledge of mathematical logic. (Clearly she or he has to have a good sense of logic, but this is a completely different matter.) In other words (unlike Carl Mummert), I cannot imagine any `difficulties in an alternate world where mathematicians have to distinguish between "true in all groups" and "provable from the axioms of a group" '. The reason is simple. I do not think that anyone proves "that a group identity is derivable from the axioms of a group by working semantically and showing that the identity holds in every group." Though I am not a group theorist, I think that no group theorist is interested in the statements that are provable from the axioms of group theory alone. (On the other hand, of course, the most important elementary statements needed to begin group theory at all are usually derived directly from the axioms.) Most mathematicians work in intuitive set theory and freely make use of the different possibilities that this rich theory offers (independently of the fact that she or he is aware of the existence of ZFC). (Actually, the notion of a group itself is defined as a model, that is, generally in terms of sets rather than a first order theory. And, of course, this kind of definition is very practical, since otherwise every course on groups have to be preceded by an introduction to logic.) I think that the pure first order theory of groups has only theoretical or didactic significance for being a nice widely known example of a first order theory.

Likewise, I do not agree with Stefan Geschke that "the completeness theorem does explain why we can do mathematics the way we do." Just the other way around. Clearly, metamathematics is the study of real mathematics by exact mathematical means. Therefore, its notions are intended to mimic those of everyday informal mathematics as faithfully as this is possible. So a metamathematical result cannot explain or justify anything. What it can do is to describe in exact terms and clarify the way mathematics is normally done (and, of course, to draw consequences about everyday mathematics from the results of this description). But its results do not affect the way mathematics is normally done. Obviously, we would do everyday mathematics in exactly the same way if the Completeness Theorem did not hold. Just as those mathematicians do who never have heard of this theorem. And indeed, we do arithmetic in exactly the same way as mathematicians before Gödel (who might well think that true arithmetic was recursively axiomatizable) did.

Answer 10

Compactness is a "semantic" theorem, whose statement involves no "syntactic" concepts such as proofs or provability. So it seems one should not need the latter concepts to prove compactness (and of course, one does not).