6.2 First-order equivalences

The following equivalences are in addition to those of propositional logic . In these, $\phi$ and $\psi$ each stand for any WFF, but $\theta$ stands for any WFF with no free occurrences of $x$ .

When citing Distribution of Quantifiers, say what you're distributing over what: e.g. ,

distribute ∀ over ∨ (with $\theta$ being $x$ -free)

In renaming , the notation $(\phi , \left[\mapsto (x, y)\right])$ means

$\phi$ with each free occurrence of $x$ replaced by $y$

This set of equivalences isn't actually quite complete. For instance, $\exists x\colon \forall y\colon R(x, y)\implies \forall y\colon \exists x\colon R(x, y)$ is equivalent to $\mbox{true}$ , but we can't show it using only the rules above. It does become complete It's not obvious whenthis system is complete; that's Gödel's completeness theorem , his 1929 Ph.D. thesis.Don't confuse it with his more celebrated In completeness Theorem, on the other hand, which talks about the ability to prove formulas which are true in allinterpretations which include arithmetic (as opposed to all interpretations everywhere.) if we add some analogs of the first-order inference rules , replacing ⊢ with ⇒(and carrying along their baggage of

arbitrary

free-to-substitute-in