ABSTRACT
This chapter of our book contains the proof of the compactness theorem for propositional logic. The special case we study is based on clausal logic (a minor limitation; compactness of clausal logic entails compactness of full propositional logic, see below). What happens here is that we restrict ourselves to the situation where the underlying language has only a denumerable number of formulas (clauses in our case). This limits the number of variables to finite or infinite denumerable. In such circumstances we can enumerate with integers all formulas (clauses in our case) and so we can enumerate all clauses over a given set of variables. This limitation allows for use of a very powerful tool, known as Ko¨nig lemma. In the next section we will prove Ko¨nig lemma. Then, with this tool we will show how the compactness property for denumerable CNFs is a relatively simple corollary to that result. It should be stated that the proof of the compactness theorem we present here hides rather than elucidates the fundamental principles related to compactness of propositional logic. In fact, one can give a general argument for compactness of propositional logic that does not depend on the cardinality of the set of clauses. Such an argument uses, however, additional tools and goes beyond the scope of our book.
