Skip to main content
1 of 3
François G. Dorais
  • 44.4k
  • 6
  • 150
  • 233

I think you're looking for the Fraïssé School of Model Theory which is based strictly on structures and types as primitives and avoids all syntax. I don't know of a good source for the extremist Fraïssean approach, but Bruno Poizat's "A Course in Model Theory" is a good bridge (if you can tolerate Poizat's eccentic, and sometimes polemic, style).

Poizat starts off defining types (via back & forth) in Chapter 1, then he (apologetically) introduces formulas in Chapter 2. In Chapter 4, he proves the Compactness Theorem using ultrapowers and then presents the Henkin method as an afterthought. (He does more formal deduction later in Chapter 7, but only in order to prove the Incompleteness Theorems.) In the notes at the end of Chapter 4, Poizat writes:

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 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.

There are two key points in there. The first, which comes through rather clearly, is that Model Theory could ultimately be done without any formal syntax and deduction rules. The second, much more subtle point, is present only in the parenthetical remark "and thus also less sophisticated" in the second paragraph. This sounds like Poizat is saying that the Completeness Theorem does not follow from the Compactness Theorem, but it does, at least in some abstract sense. The Compactness Theorem does imply that there is some system of finitary rules for deduction which are complete for semantic consequence. The only "sophisticated" part missing is that this set of rules has a simple description. In particular, the Incompleteness Theorems are not consequences of the Compactness Theorem.

François G. Dorais
  • 44.4k
  • 6
  • 150
  • 233