- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

sav08:compactness_theorem [2012/05/06 00:24] vkuncak |
sav08:compactness_theorem [2015/04/21 17:30] (current) |
||
---|---|---|---|

Line 28: | Line 28: | ||

We will define interpretation $I^*(p_k) = v_k$ where the sequence of values $v_1,v_2,\ldots$ is given as follows: | We will define interpretation $I^*(p_k) = v_k$ where the sequence of values $v_1,v_2,\ldots$ is given as follows: | ||

- | \[ | + | \begin{equation*} |

v_{k+1} = \left\{\begin{array}{l} | 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 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} | {\it true}, \mbox{otherwise} | ||

- | \] | + | \end{equation*} |

We next show by induction the following. | We next show by induction the following. | ||

Line 43: | Line 43: | ||

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. | 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$. | + | 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, and it agrees on all variables in $F$, we have $I^* \models F$. |

**End of Proof.** | **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 | 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 | ||

- | \[ | + | \begin{equation*} |

m = \max(k, \max \{i \mid p_i \in T \}) | m = \max(k, \max \{i \mid p_i \in T \}) | ||

- | \] | + | \end{equation*} |

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 part, which, from the existence of interpretations that agree on an arbitrarily long finite prefix 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. | 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 part, which, from the existence of interpretations that agree on an arbitrarily long finite prefix 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. | ||