Differences

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

--- sav08:compactness_for_first-order_logic [2008/03/20 12:25]
vkuncak created
+++ sav08:compactness_for_first-order_logic [2008/03/20 17:51]
vkuncak
@@ Line 3: / Line 3: @@
 Let $S_0$ be a set of first-order formulas.
-Suppose $S_0$ has no model.  Then $expandProp(clauses(S_0))$ has no model.  Some finite subset of it has no model.  Some finite subset of $clauses(S_0)$ has no model. Some finite subset of $S_0$ has no model.
+Suppose $S_0$ has no model.
+Then $expandProp(clauses(S_0))$ has no model.
+Some finite subset $S_1 \subseteq expandProp(clauses(S_0))$ of it has no model.
+There is then finite subset of clauses $S_2 \subseteq clauses(S_0)$ that generate $S_1$, i.e. such that $S_1 \subseteq expandProp(S_2)$.  Therefore, $S_2$ has no model.
+These clauses are generated by a finite subset $S_3 \subseteq S_0$, i.e. $S_2 \subseteq clauses(S_3)$.
+Therefore $S_3$ has no model.