Differences

This shows you the differences between two versions of the page.

--- sav08:compactness_theorem [2012/05/06 00:23]
vkuncak
+++ sav08:compactness_theorem [2015/04/21 17:30]
@@ Line 1: / Line 1: @@
-====== Compactness Theorem for Propositional Logic ======
-Among the application of compactness theorem is showing that certain theorem proving methods are "complete in the limit".
-Notation:
-  * ${\cal B} = \{ \mbox{false},\mbox{true} \}$
-  * $V$ is the countably infinite set of all propositional variables of interest
-  * interpretation $I : V \to {\cal B}$ maps propositional variables $V$ to truth values ${\cal B}$
-  * if $F$ is a propositional formula, $I \models F$ means that $F$ is true when the variables are interpreted according to $I$
-  * if $S$ is a set of formulas, $I \models S$ means: for each $F \in S$, $I \models F$
-**Theorem (Compactness Theorem for Propositional Logic)**: Let $S$ be a (possibly infinite) set of [[Propositional Logic Syntax|propositional formulas]].  Then $S$ is satisfiable if and only if every finite subset of $S$ is satisfiable.
-**Equivalent statement of compactness:** If a set $S$ is not satisfiable, then some finite subset of $S$ is not satisfiable.
-If we allow infinite disjunctions in formulas, compactness fails.  Note that we do not consider formulas with infinite connectives as propositional formulas (such formulas are usually called 'infinitary'), and from that reason the compactness theorem does not apply to this example.
-Example. $S = \{ D, p_1, p_2, p_3, \ldots \}$ where $D = \bigvee\limits_{i=1}^{\infty} \lnot p_i$, that is, $D$ is equivalent to $\exists i \ge 0. \lnot p_i$.
-In this example, every finite subset of $S$ is satisfiable, but $S$ itself is not.
-**Proof of the compactness theorem:** One direction is trivial: if $S$ is satisfiable then there exists $I$ such that $I \models S$.  Then for every finite subset $T \subseteq S$ we have $I \models T$, so $T$ is satisfiable.  We need to show the converse.
-Intuition: A finitely satisfiable set has "all finite pieces" satisfiable (using potentially different interpretations).  The question is whether we can somehow assemble interpretations for all finite pieces $T$ into one large interpretation for the entire infinite set $S$.  We will define such interpretation by extending it variable by variable, while preserving finite satisfiability for interepretations that begin with values for propositional variables chosen so far.
-Let $S$ be finitely satisfiable.  Let $V = \{ p_1,p_2,\ldots \}$ be the sequence of all propositional variables for formulas in $S$ (this set is countable by our assumption on [[Propositional Logic Syntax]], but can be infinite).
-Given a sequence of boolean values $u_1,u_2,\ldots,u_n \in {\cal B}$ of length $n \ge 0$, by an $u_1,u_2,\ldots,u_n$-interpretation we mean an interpretation $I : V \to {\cal B}$ such that $I(p_1)=u_1,\ldots,I(p_n)=u_n$.
-We will define interpretation $I^*(p_k) = v_k$ where the sequence of values $v_1,v_2,\ldots$ is given as follows:
-\[
-    v_{k+1} = \left\{\begin{array}{l}
-{\it false}, \mbox{ if for every finite } T \subseteq S, \mbox{ there exists a } v_1,\ldots,v_k,{\it false}-\mbox{interpretation } I \mbox{ such that } I \models T \\
-{\it true}, \mbox{otherwise}
-\]
-We next show by induction the following.
-FIRST PART.
-Claim: For every non-negative integer $k$, every finite subset $T \subseteq S$ has a $v_1,\ldots,v_k$-interpretation $I$ such that $I \models T$.
-Base case: For $k=0$ the statement reduces to claim that every finite subset of $S$ is satisfiable, which is an assumption of the theorem.
-Inductive step: Assume the claim for $k$: every finite subset $T \subseteq S$ has a $v_1,\ldots,v_k$-interpretation $I$ such that $I \models T$, we show that the statement holds for $k+1$.  If $v_{k+1}={\it false}$, the inductive statement holds by definition of $v_{k+1}$.  Let $v_{k+1}={\it true}$.   Then by definition of $v_{k+1}$, there exists a finite set $A \subseteq S$ that has no $v_1,\ldots,v_k,{\it false}$ interpretation.  We wish to show that every finite set $B \subseteq T$ has a $v_1,\ldots,v_k,{\it true}$ interpretation such that $I \models B$.  Take any such set $B$.  Consider the set $A \cup B$.  This is a finite set, so by inductive hypothesis, it has a $v_1,\ldots,v_k$-interpretation $I$.  Because $I \models A$ which has no $v_1,\ldots,v_k,{\it false}$-interpretation, we have $I(p_{k+1})={\it true}$. Therefore, $I$ is a $v_1,\ldots,v_k,{\it true}$-interpretation for $A \cup B$, and therefore for $B$.  This completes the inductive proof.
-SECOND PART. We finally show that $I^* \models S$.  Let $F \in S$.  Let $FV(F) = \{p_{i_1},\ldots,p_{i_k} \}$ and $M = \max(i_1,\ldots,i_k)$. Then $FV(F) \subseteq \{p_1,\ldots,p_M\}$.  The set $\{F\}$ is finite, so, by the Claim, it has a $v_1,\ldots,v_M$-interpretation $I$ such that $I \models F$.  Because $I^*$ is also a $v_1,\ldots,v_M$-interpretation, we have $I^* \models F$.
-**End of Proof.**
-How does this proof break if we allow infinite disjunctions? Consider the above example $S = \{ D, p_1, p_2, p_3, \ldots \}$ where $D = \bigvee\limits_{i=1}^{\infty} \lnot p_i$. The inductively proved claim still holds, and the sequence defined must be $true, true, true, \ldots$. Here is why the claim holds for every $k$. Let $k$ be arbitrary and $T \subseteq S$ be finite. Define
-\[
-   m = \max(k, \max \{i \mid p_i \in T \})
-\]
-Then consider interpretation that assigns to true all $p_j$ for $j \le m$ and sets the rest to false. Such interpretation makes $D$ true, so if it is in the set $T$, then interpretation makes it true. Moreover, all other formulas in $T$ are propositional variables set to true, so the interpretation makes $T$ true. Thus, we see that the inductively proved statement holds even in this case. What the infinite formula $D$ breaks is the second argument, that from arbitrarily long interpretations we can derive an interpretation for infinitely many variables. Indeed, this part of the proof explicitly refers to a finite number of variables in the formula.