LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
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
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.