   Box diagrams Completeness Theorem
If is unsatisfiable, there is a refutation of .
Compactness Theorem
If is unsatisfiable, there is an unsatisfiable finite subset of .
Sko-Lo
If is satisfiable, there is an interpretation with an enumerable domain such that  .
Lemma I
For any set , there is a canonical derivation from . matches Lemma II
What is it; how the proof of it works. `` So let us suppose that is unsatisfiable. By Lemma I, there is a canonical derivation from . Since is unsatisfiable and is a subset of all the sentences appearing in , there is no model of the set of all such sentences. By Lemma II, then, there is no model of the set of quantifier-free sentences in that matches . If we could prove a proposition to the effect that

(+)
if every finite subset of is satisfiable then some interpretation maches then we should have proved the completeness theorem, for we should know that some finite set of the quantifier-free sentences in is unsatisfiable" (p. 135).

Let's make sure we get this Selmer Bringsjord
Tue Apr 15 11:30:32 EDT 1997