The information in this module is
outdated. Please see
my
course for a table of contents.
The following equivalences are in addition to
those of propositional logic (.ps).
First-order Logic Equivalences
| Complementation of Quantifiers
|
∀x.x. ¬φ ≡φ≡ ¬ ∃x. φx.φ
|
∃x.x. ¬φ ≡φ≡ ¬ ∀x. φx.φ
|
| Interchanging Quantifiers
|
∀x.x. ∀y. φ
≡y.φ≡ ∀y.y. ∀x. φx.φ
|
∃x.x. ∃y. φ
≡y.φ≡ ∃y.y. ∃x. φx.φ
|
| Distribution of Quantifiers
|
∀x. (φ ∧ ψ)
≡ (x.(φ∧ψ)≡(∀x. φ ∧x.φ∧ ∀x. ψ )x.ψ)
|
∃x. (φ ∨ ψ) ≡ (x.(φ∨ψ)≡(∃x. φ ∨x.φ∨ ∃x. ψ )x.ψ)
|
|
The following identities each assume that ψψ
does not have any free occurrences of variable xx.
|
| Simplification of Quantifiers
|
∀x. ψ ≡ ψx.ψ≡ψ
|
∃x. ψ ≡ ψ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.φ)
|
∃x. (ψ → φ) ≡ (ψ →x.(ψ→φ)≡(ψ→ ∃x. φ )x.φ)
|