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:
Theorem 22 (Soundness) Suppose that
is a set of formulas, and that
then
In particular, any theorem is a tautology, and therefore there are formally consistent sets.
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:
Fact 4
iff
is contradictory iff
iff
![]()
Remark 9 Note that
is monotone, in the sense that if
and
then
also, if
for all
and
then
![]()
10. Compactness
- 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:
Lemma 25 Any finite partial order can be extended to a total order.
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.