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 xx
.
First-order Logic Equivalences
| Equivalence |
∀∀ Variant |
∃∃ Variant |
|
Complementation of Quantifiers
|
∀x. ¬φ ≡¬ ∃x. φ ∀x. ¬φ ≡¬ ∃x. φ
|
∃x. ¬φ ≡¬ ∀x. φ ∃x. ¬φ ≡¬ ∀x. φ
|
|
Interchanging Quantifiers
|
∀x. ∀y. φ ≡∀y. ∀x. φ ∀x. ∀y. φ ≡∀y. ∀x. φ
|
∃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. φ ∨θ)∀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. φ ∨θ)
|
|
|
∃x. (φ→θ) ≡(∀x. φ →θ)∃x. (φ→θ) ≡(∀x. φ →θ)
|
|
∃x. (θ→φ) ≡(θ→∃x. φ )∃x. (θ→φ) ≡(θ→∃x. φ )
|
|
Renaming
|
∀x.φ≡∀y.
φ[x↦y]
∀x.φ≡∀y.
φ[x↦y]
|
∃x.φ≡∃y.
φ[x↦y]
∃x.φ≡∃y.
φ[x↦y]
|
|
Simplification of Quantifiers — with non-empty domain
|
∀x. θ ≡θ∀x. θ ≡θ
|
∃x. θ ≡θ∃x. θ ≡θ
|
|
Simplification of Quantifiers — with empty domain
|
∀x. φ ≡true∀x. φ ≡
|
∃x. φ ≡false∃x. φ ≡
|
When citing Distribution of Quantifiers,
say what you're distributing over what: e.g.,
“distribute ∀∀ over ∨∨ (with θθ being xx-free)”.
In
renaming,
the notation
φ[x↦y]φ[x↦y]
means
“φφ with each free occurrence of xx replaced by yy”.
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)
)(∃x.
∀y.
R(x,y)
→∀y.
∃x.
R(x,y)
)
is equivalent to true, but we can't show it using only the rules above.
It does become complete
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”).