Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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