m11045 Reference: first-order equivalences 2.18 2003/02/11 2009/03/24 15:40:17.455 GMT-5 John Greiner John Greiner greiner@cs.rice.edu Phokion Kolaitis Phokion Kolaitis kolaitis@cse.ucsc.edu Moshe Vardi Moshe Vardi vardi@cs.rice.edu Matthias Felleisen Matthias Felleisen matthias@ccs.neu.edu John Greiner John Greiner greiner@cs.rice.edu Ian Barland Ian Barland ibarland@radford.edu John Greiner John Greiner greiner@cs.rice.edu Phokion Kolaitis Phokion Kolaitis kolaitis@cse.ucsc.edu Moshe Vardi Moshe Vardi vardi@cs.rice.edu Matthias Felleisen Matthias Felleisen matthias@ccs.neu.edu Science and Technology Some equivalences for manipulation of first-order formulas. en The following equivalences are in addition to those of propositional logic. In these, φ and ψ each stand for any WFF, but θ stands for any WFF with no free occurrences of x . Equivalence ∀ Variant ∃ Variant Complementation of Quantifiers x φ x φ x φ x φ Interchanging Quantifiers x y φ y x φ x y φ y x φ Distribution of Quantifiers x φ ψ x φ x ψ x φ ψ x φ x ψ x φ θ x φ θ x φ θ x φ θ x φ θ x φ θ x θ φ θ x φ Distribution of Quantifiers — with non-empty domain x φ θ x φ θ x φ θ x φ θ x φ θ x φ θ x θ φ θ x φ Renaming ↦ x φ y ⁡ φ ↦ x y ↦ x φ y ⁡ φ ↦ x y Simplification of Quantifiers — with non-empty domain x θ θ x θ θ Simplification of Quantifiers — with empty domain x φ x φ When citing Distribution of Quantifiers, say what you're distributing over what: e.g., distribute ∀ over ∨ (with θ being x-free) . In renaming, the notation ↦ ⁡ φ ↦ x y means φ with each free occurrence of x replaced by y . It is a meta-formula; when writing any particular formula you don't write any brackets, and instead just do the replacement. This set of equivalences isn't actually quite complete. For instance, x y Rxy y x Rxy is equivalent to , but we can't show it using only the rules above. It does become complete It's not obvious when this system is complete; that's Gödel's completeness theorem, his 1929 Ph.D. thesis. Don't confuse it with his more celebrated Incompleteness Theorem, on the other hand, which talks about the ability to prove formulas which are true in all interpretations 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 and free-to-substitute-in).