202309261409

Tags : Logic

Finite Sat for FOL Motivation

---

We will try what we did in propositional logic.

1. $\{x_1\equiv x_2,x_2\equiv x_3,x_3\not\equiv x_1\}$. Simply replacing each formula with an atomic proposition doesn’t work because we lose information about the relations between the formulas. $\{p_{12},p_{23},p_{31},p_{12}\wedge p_{23}⟹\neg p_{31}\}$, however, works!

2. $\{\forall x(r(x)⟹s(x)),\forall x(r(x)),\exists x(\neg s(x))\}$ The previous way shouldn’t work because it’s not as straightforward to see that two of these formulas imply that the third should be negated. If we were to try proving that, it would be equivalent to finding whether this set is satisfiable in FOL itself, which defeats the purpose.

Prime formulas: formulas of the form $t_1\equiv t_2,r(t_1,\dots ,t_n),\text{ or }\exists x\phi$. $\{\neg \exists x(r(x)\wedge s(x)),\neg \exists x\neg r(x),\exists x\neg s(x)\}$

• $p_1:\exists x(r(x)\wedge \neg s(x))$,
• $p_2:\exists x\neg r(x)$,
• $p_3:\exists x\neg s(x)$

$\{\neg p_1,\neg p_2,p_3\}$

Prime formula structure: For FO language $L$, let ${\mathcal{P}}_L$ be the set of all prime formulas.

---

Lemma: Let $\mathcal{I}$ be an interpretation. There exists a valuation $v:{\mathcal{P}}_L\to \{\top ,\perp \}$ s.t. for FO formula $\phi$, $\mathcal{I}{\models }_{FO}\phi$ iff $v{\models }_{{\mathcal{P}}_L}\phi$. (All this lemma is saying is that we can make up a valuation. The valuation loses a lot of information that the interpretation has, so the converse is not true.)

• Equality is transitive.
• Suppose $\exists x\phi (x)$ is true. There is a term $t_{\phi }$ which certifies this. We add $\exists x\phi (x)⟹\phi (t_{\phi })$.
• Suppose $\neg \exists x\phi (x)$ is true. Every element satisfies $\neg \phi$. We add $\neg \exists x\phi (x)⟹\neg \phi (t)$ for an arbitrary term $t$.

---

References

First Order Logic Finite Sat for FOL