502 – Propositional logic (3)

Example 13 {\lnot(A\land B)\leftrightarrow(\lnot A\lor\lnot B)} is a tautology. This is an example of De Morgan’s laws.

Example 14 {A\lor(B\land C)\leftrightarrow(A\lor B)\land(A\lor C)} is a tautology.

Definition 19 A formula {A} is satisfiable iff there is some valuation {v} such that {v\models A.} Otherwise, we say that {A} is contradictory, or unsatisfiable.

Remark 7 {A} is unsatisfiable iff {\lnot A} is a tautology.

Example 15 {(p\rightarrow q)\rightarrow(q\rightarrow p)} is not a tautology, but it is satisfiable.

Definition 20 If {v} is a valuation and {S} is a set of formulas, {v\models S} iff {v\models A} for all {A\in S.} For a given {S,} if there is such a valuation {v,} we say that {S} is satisfiable, or has a model, and that {v} is a model of {S.} Otherwise, {S} is unsatisfiable or contradictory.

Example 16 Let {S=\{p_i\lor p_2,\lnot p_2\lor\lnot p_3, p_3\lor p_4,\lnot p_4\lor\lnot p_5,\dots\}.} Then {S} is satisfiable, as witnessed by the valuation {v} given by 

\displaystyle v(p_i)=i\mod2.

Definition 21 {S\models A} iff for any valuation {v,} if {v\models S,} then also {v\models A.}

Remark 8 Note that if {S} is contradictory, then {S\models A} for any {A.} Also, {\models A} iff {\emptyset\models A.}

We can now prove that there are sets {S} that are formally consistent. We begin by observing that the semantic version of MP holds:

Fact 3 {\{A,A\rightarrow B\}\models B.} {\Box}

Theorem 22 (Soundness) Suppose that {S} is a set of formulas, and that {S\vdash A;} then {S\models A.} 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 {\emptyset} is formally consistent. \Box

The semantic versions of the deduction theorem, of proof by contradiction, and of proof by contrapositive also hold:

Fact 4

  1. {S\cup\{A\}\models B} iff {S\models A\rightarrow B.}
  2. {S\cup\{A\}} is contradictory iff {S\models\lnot A.}
  3. {S\cup\{A\}\models\lnot B} iff {S\cup\{B\}\models\lnot A.} {\Box}

Remark 9 Note that {\models} is monotone, in the sense that if {S\models A} and {S\subseteq S',} then {S'\models A.} also, if {S\models A} for all {A\in T,} and {T\models B,} then {S\models B.}

10. Compactness

Theorem 23 (Compactness)


  1. Suppose that every finite subset of a set {S} of formulas is satisfiable. Then so is {S.}
  2. Suppose that {S\models A.} Then there is a finite {S_0\subseteq S} such that {S_0\models A.}

Proof: The first item is immediate from König’s lemma. For the second: Suppose that {S\models A.} Then {S\cup\{\lnot A\}} is not satisfiable, so by item (1), there is a finite {S_0\subseteq S} such that {S_0\cup\{\lnot A\}} is not satisfiable. But then {S_0\models A.} \Box

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 {T} be a given infinite finite branching tree. For each node {\nu\in T} let {p_\nu} be a propositional variable. (Note that {T} has countably many nodes, so this labeling is possible.) Intuitively, we want to find a branch {b} of {T,} and think of {p_\nu} as being the statement “{\nu} is in {b.}” We now pass to describe a theory {S} that, if satisfiable, will ensure that there is such a branch. In fact, we will arrange things so that from any valuation modeling {S} we can easily define a branch.

(It is customary to refer to sets of formulas as theories.)

Let {S=\{p_\emptyset\}\cup\{p_\nu\rightarrow\lnot p_\mu\mid \nu\ne \mu} are nodes at the same level, or for some {n,} {\nu} is at level {n,} {\mu} is at level {n+1,} and {\mu} is not an immediate successor of {\nu\}\cup\{p_{\nu_1}\lor\dots\lor p_{\nu_k}\mid} for some {m,} {\{p_{\nu_1},\dots,p_{\nu_k}\}} is the {m}-th level of {T\}.}

We have two tasks: First, we need to see that from a valuation {v\models S} one can (“easily”) define a branch through {T.} What we actually want is to check that given such a {v,} the set

\displaystyle b=\{\nu\mid v(p_\nu)=1\}

is a branch.

This is actually easy. By induction, check that for each {n} there is exactly one {\nu} in {T} at level {n} such that {v(p_\nu)=1,} and that if {v(p_\nu)=v(p_\mu)=1,} then {\nu} is an initial segment of {\mu,} or vice versa.

The second task is where we use compactness: We need to show that there is indeed at least one valuation {v} that models {S.} For this, compactness tells us that it is enough to check that any finite {S_0\subset S} is satisfiable. We can do this as follows: For any such {S_0,} the set

\displaystyle {\rm supp}(S_0)=\bigcup\{{\rm supp}(A)\mid A\in S_0\}

is contained in the first {n} levels of {T,} for some {n.} Pick any node {\mu} at level {n+1,} and define {v} on the first {n} levels of {T} so that {v(p_\nu)=1} iff {\nu\sqsubset\mu.} It is easy to see that {v\models S_0,} 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 {(X,<)} be a finite partial order. We argue by induction on {n=|X|.} If {n=1} there is nothing to do. Suppose that {n>1} and that the result holds for {n-1.} Say that {x\in X} is minimal iff there is no {y<x.} Since {X} is finite, there is at least one minimal {x_0\in X.} Since the set {X\setminus\{x_0\}} is of size {n-1,} we can use the induction hypothesis and find a linear extension of {<} on {X\setminus\{x_0\}.} Further extend this order to all of {X} by letting {x_0} be its minimum. \Box

Now we proceed to the infinite case. Let {({\mathbb N},\prec)} be a poset. We want to find a total extension {\hat\prec} of {\prec.} For each {i,j} let {p_{ij}} be a propositional variable. Our intention is that {p_{ij}} is the statement “{i\hat\prec j}.” As before, we build a theory {S} so that a valuation of {S} provides us with the desired extension, and use compactness to check that {S} is satisfiable.

{S} needs to code the fact that {\hat\prec} is a linear order, and that it extends {\prec.} With this in mind, it is easy to see that the following theory works:

{S=S_0\cup S_1\cup S_2\cup S_3,} where {S_0=\{p_{ij}\rightarrow\lnot p_{ji}\mid i,j\in{\mathbb N}\},} {S_1=\{p_{ij}\land p_{jk}\rightarrow p_{ik}\mid i,j,k\in{\mathbb N}\},} {S_2=\{p_{ij}\lor p_{ji}\mid i\ne j\},} and {S_3=\{p_{ij}\mid i\prec j\}.} The axioms in {S_0} code that {\hat\prec} is irreflexive, {S_1} codes that it is transitive, and {S_2} that it is total. Finally, {S_3} codes that it extends {\prec.}

If we have that {v\models S,} we can then set {\hat\prec=\{(i,j)\mid v(p_{ij})=1\},} and this is the desired extension.

It remains to show that {S} is satisfiable. By compactness, it suffices to show that any finite {S'\subseteq S} is satisfiable. Given such {S',} Lemma 25 tells us that the restriction of {\prec} to

\displaystyle X=\{ i\mid \mbox{ for some }j,p_{ij}\in{\rm supp}(S')\}

can be extended to a linear order {\prec'.} Define {v} so that given {p_{ij}\in {\rm supp}(S'),} we have {v(p_{ij})=1} iff {i\prec' j.} It is easy to see that {v\models S',} and we are done. \Box

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 {k}-colorable is {k}-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.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: