Example 13 is a tautology. This is an example of De Morgan’s laws.
Example 14 is a tautology.
Definition 19 A formula is satisfiable iff there is some valuation such that Otherwise, we say that is contradictory, or unsatisfiable.
Remark 7 is unsatisfiable iff is a tautology.
Example 15 is not a tautology, but it is satisfiable.
Definition 20 If is a valuation and is a set of formulas, iff for all For a given if there is such a valuation we say that is satisfiable, or has a model, and that is a model of Otherwise, is unsatisfiable or contradictory.
Example 16 Let Then is satisfiable, as witnessed by the valuation given by
Definition 21 iff for any valuation if then also
Remark 8 Note that if is contradictory, then for any Also, iff
We can now prove that there are sets that are formally consistent. We begin by observing that the semantic version of MP holds:
Proof: Since the axioms are tautologies, the first part of the result is immediate from Fact 3 by induction on the length of proofs. For the second part, note that there are formulas that are not tautologies, and that those formulas cannot be theorems. So is formally consistent.
The semantic versions of the deduction theorem, of proof by contradiction, and of proof by contrapositive also hold:
- is contradictory iff
Remark 9 Note that is monotone, in the sense that if and then also, if for all and then
- Suppose that every finite subset of a set of formulas is satisfiable. Then so is
- Suppose that Then there is a finite such that
Proof: The first item is immediate from König’s lemma. For the second: Suppose that Then is not satisfiable, so by item (1), there is a finite such that is not satisfiable. But then
To illustrate the power of Theorem 23, I present now two applications. First, I explain how to deduce König’s lemma from it (so that König’s lemma and compactness are actually equivalent).
Let be a given infinite finite branching tree. For each node let be a propositional variable. (Note that has countably many nodes, so this labeling is possible.) Intuitively, we want to find a branch of and think of as being the statement “ is in ” We now pass to describe a theory that, if satisfiable, will ensure that there is such a branch. In fact, we will arrange things so that from any valuation modeling we can easily define a branch.
(It is customary to refer to sets of formulas as theories.)
Let are nodes at the same level, or for some is at level is at level and is not an immediate successor of for some is the -th level of
We have two tasks: First, we need to see that from a valuation one can (“easily”) define a branch through What we actually want is to check that given such a the set
is a branch.
This is actually easy. By induction, check that for each there is exactly one in at level such that and that if then is an initial segment of or vice versa.
The second task is where we use compactness: We need to show that there is indeed at least one valuation that models For this, compactness tells us that it is enough to check that any finite is satisfiable. We can do this as follows: For any such the set
is contained in the first levels of for some Pick any node at level and define on the first levels of so that iff It is easy to see that and we are done.
The second application is the following result:
Theorem 24 Any countable partial order can be extended to a total order.
Proof: We first verify the result for finite partial orders:
Proof: Let be a finite partial order. We argue by induction on If there is nothing to do. Suppose that and that the result holds for Say that is minimal iff there is no Since is finite, there is at least one minimal Since the set is of size we can use the induction hypothesis and find a linear extension of on Further extend this order to all of by letting be its minimum.
Now we proceed to the infinite case. Let be a poset. We want to find a total extension of For each let be a propositional variable. Our intention is that is the statement “.” As before, we build a theory so that a valuation of provides us with the desired extension, and use compactness to check that is satisfiable.
needs to code the fact that is a linear order, and that it extends With this in mind, it is easy to see that the following theory works:
where and The axioms in code that is irreflexive, codes that it is transitive, and that it is total. Finally, codes that it extends
If we have that we can then set and this is the desired extension.
It remains to show that is satisfiable. By compactness, it suffices to show that any finite is satisfiable. Given such Lemma 25 tells us that the restriction of to
can be extended to a linear order Define so that given we have iff It is easy to see that and we are done.
It is instructive to use compactness to prove the infinite Ramsey’s theorem from its finite version (the finite version has nice, relatively easy, combinatorial proofs), or to prove that any countable graph whose finite subgraphs are -colorable is -colorable as well.
Compactness also holds for theories of arbitrary size, not just countable ones, but our argument, dependant in König’s lemma, needs to be modified.
Typeset using LaTeX2WP. Here is a printable version of this post.