next up previous
Next: About this document

Box diagrams tex2html_wrap_inline20
Completeness Theorem
If tex2html_wrap_inline22 is unsatisfiable, there is a refutation of tex2html_wrap_inline22 .
Compactness Theorem
If tex2html_wrap_inline22 is unsatisfiable, there is an unsatisfiable finite subset tex2html_wrap_inline28 of tex2html_wrap_inline22 .
Sko-Lo
If tex2html_wrap_inline22 is satisfiable, there is an interpretation tex2html_wrap_inline34 with an enumerable domain such that tex2html_wrap_inline34 tex2html_wrap_inline38 .
Lemma I
For any set tex2html_wrap_inline22 , there is a canonical derivation tex2html_wrap_inline42 from tex2html_wrap_inline22 .
tex2html_wrap_inline34 matches tex2html_wrap_inline48
Lemma II
What is it; how the proof of it works.

displaymath50

`` tex2html_wrap_inline20 So let us suppose that tex2html_wrap_inline22 is unsatisfiable. By Lemma I, there is a canonical derivation tex2html_wrap_inline42 from tex2html_wrap_inline22 . Since tex2html_wrap_inline22 is unsatisfiable and is a subset of all the sentences appearing in tex2html_wrap_inline42 , there is no model of the set of all such sentences. By Lemma II, then, there is no model of the set tex2html_wrap_inline64 of quantifier-free sentences in tex2html_wrap_inline42 that matches tex2html_wrap_inline64 . If we could prove a proposition to the effect that

(+)
if every finite subset of tex2html_wrap_inline64 is satisfiable then some interpretation maches tex2html_wrap_inline64

then we should have proved the completeness theorem, for we should know that some finite set of the quantifier-free sentences in tex2html_wrap_inline42 is unsatisfiable" (p. 135).

Let's make sure we get this tex2html_wrap_inline20





Selmer Bringsjord
Tue Apr 15 11:30:32 EDT 1997