1st-order logic

Conventions of 1st-order logic in these notes

See also Conventions of 0th-order logic in these notes

Quantification

The statement “there exists 𝑥 satisfying 𝜑(𝑥)” and “all 𝑥 satisfy 𝜑(𝑥)” are written as

(∃𝑥)𝜑(𝑥)(∀𝑥)𝜑(𝑥)

If T is a type, then either of the following notations may be used for “there exists 𝑥 of type T satisfying 𝜑(𝑥)” (the notation for the universal quantifier is similar)

(∃𝑥:T)𝜑(𝑥)(∃T⁡𝑥)𝜑(𝑥)

This notation is also used as an abbreviation for quantifications with predicates.¹ If P is a unary predicate,

(∃P⁡𝑥)𝜑(𝑥)def⟺(∃𝑥)[P⁡(𝑥)∧𝜑(𝑥)](∀P⁡𝑥)𝜑(𝑥)def⟺(∀𝑥)[P⁡(𝑥)⇒𝜑(𝑥)]

and if ∈ is a binary predicate,

(∃𝑥∈𝑦)𝜑(𝑥)def⟺(∃𝑥)[𝑥∈𝑦∧𝜑(𝑥)](∀𝑥∈𝑦)𝜑(𝑥)def⟺(∀𝑥)[𝑥∈𝑦⇒𝜑(𝑥)]

We also have the following abbreviation for nonexistence

(∄𝑥)𝜑(𝑥)def⟺¬(∃𝑥)𝜑(𝑥)

---

develop | en | SemBr

Footnotes

1. This is of course compatible with the flattening of a finite-typed 1st-order logic to a single typed one with predicates. ↩