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:combining_fol_models [2012/05/21 19:48]
vkuncak
sav08:combining_fol_models [2012/05/21 20:09]
vkuncak
Line 11: Line 11:
 **Proof (using interpolation):​** First-order logic has interpolation property, by Craig'​s interpolation theorem. Suppose we have models for  **Proof (using interpolation):​** First-order logic has interpolation property, by Craig'​s interpolation theorem. Suppose we have models for 
 $C_1 \cup Ax_1$ and $C_2 \cup Ax_2$, but that there is no model for $C_1 \cup Ax_1$ and $C_2 \cup Ax_2$, but that there is no model for
-$C_1 \cup C_2 \cup Ax_1 \cup Ax_2$. By compactness for first-order logic there exists a finite subset that is contradictory. By interpolation there exists an interpolant $I$ that is, say, implied by $C_1 \cup Ax_1$ and contradictory with $C_2 \cup Ax_2$. The interpolant is in the common language, so it contains only equalities. It can be quantified, but over infinite domains quantifiers can be eliminated in a very simple way. So, the result is a disjunction of conjunctions of equalities and disequalities among the common variables. But because $C_1$ and $C_2$ contain a complete atomic type, they either imply or are contradictory with $I$, depending on whether the atomic diagram normal form contains the atomic type present in $C_1,C_2$ or not. Note that $I \cup C_2 \cup Ax_2$ is contradictory since $I$ is interpolant,​ so each conjunct in its DNF is contradictory. Therefore, $I$ does not have as a disjunct the atomic diagram present in $C_2$ or $C_1$. Then $I$ is contradictory with $C_1$ as well. Since $I$ is a consequence of $C_1 \cup Ax_1$, it follows that $C_1 \cup Ax_1$ is contradictory. But we assumed it is satisfiable. **End**+$C_1 \cup C_2 \cup Ax_1 \cup Ax_2$. By compactness for first-order logic there exists a finite subset that is contradictory. By interpolation there exists an interpolant $I$ that is, say, implied by $C_1 \cup Ax_1$ and contradictory with $C_2 \cup Ax_2$. The interpolant is in the common language, so it contains only equalities. It can be quantified, but over infinite domains quantifiers can be eliminated in a very simple way (and in any case, it is a fragment of BAPA that has QE). So, the result is a disjunction of conjunctions of equalities and disequalities among the common variables. But because $C_1$ and $C_2$ contain a complete atomic type, they either imply or are contradictory with $I$, depending on whether the atomic diagram normal form contains the atomic type present in $C_1,C_2$ or not. Note that $I \cup C_2 \cup Ax_2$ is contradictory since $I$ is interpolant,​ so each conjunct in its DNF is contradictory. Therefore, $I$ does not have as a disjunct the atomic diagram present in $C_2$ or $C_1$. Then $I$ is contradictory with $C_1$ as well. Since $I$ is a consequence of $C_1 \cup Ax_1$, it follows that $C_1 \cup Ax_1$ is contradictory. But we assumed it is satisfiable. **End**
  
 **Example:​** Take formula **Example:​** Take formula