Lab for Automated Reasoning and Analysis 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.
 
sav08/compactness_for_first-order_logic.txt · Last modified: 2008/03/20 17:58 by vkuncak
 
© EPFL 2018 - Legal notice