• English only

# Differences

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

 sav08:compactness_for_first-order_logic [2008/03/20 17:57]vkuncak sav08:compactness_for_first-order_logic [2008/03/20 17:58] (current)vkuncak Both sides previous revision Previous revision 2008/03/20 17:58 vkuncak 2008/03/20 17:57 vkuncak 2008/03/20 17:56 vkuncak 2008/03/20 17:55 vkuncak 2008/03/20 17:51 vkuncak 2008/03/20 12:25 vkuncak created 2008/03/20 17:58 vkuncak 2008/03/20 17:57 vkuncak 2008/03/20 17:56 vkuncak 2008/03/20 17:55 vkuncak 2008/03/20 17:51 vkuncak 2008/03/20 12:25 vkuncak created Line 11: Line 11: Then \$expandProp(clauses(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.  ​ + Then by [[Compactness Theorem]] for propositional logic, 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. 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.