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:57]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Compactness for First-Order Logic ======
-Let $S_0$ be a set of first-order formulas.
+**Theorem (Compactness for First-Order Logic):** If every finite subset of a set $S_0$ of first-order formulas has a model, then $S_0$ has a model.
-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.
+**Proof:**
+Let $S_0$ be a set of first-order formulas.  We show contrapositive.
+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 the finite subset $S_3$ of $S_0$ has no model.
+**End of Proof.**