Reference: first-order equivalences 2.16 2003/02/11 2008/02/07 14:55:03.635 US/Central John Greiner greiner@cs.rice.edu Phokion Kolaitis kolaitis@cse.ucsc.edu Moshe Vardi vardi@cs.rice.edu Matthias Felleisen matthias@ccs.neu.edu John Greiner greiner@cs.rice.edu Ian Barland ibarland@radford.edu Some equivalences for manipulation of first-order formulas. 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 . First-order Logic Equivalences 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. R⁡(x,y) →∀y. ∃x. R⁡(x,y) ) 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”).