Conventions of $1$ st-order logic in these notes

Quantification

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

(\exists 𝑥) 𝜑 (𝑥) (\forall 𝑥) 𝜑 (𝑥)

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)

(\exists 𝑥 : T) 𝜑 (𝑥) (\exists T 𝑥) 𝜑 (𝑥)

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

(\exists P 𝑥) 𝜑 (𝑥) d e f ⟺ (\exists 𝑥) [P (𝑥) \land 𝜑 (𝑥)] (\forall P 𝑥) 𝜑 (𝑥) d e f ⟺ (\forall 𝑥) [P (𝑥) \Rightarrow 𝜑 (𝑥)]

and if $\in$ is a binary predicate,

(\exists 𝑥 \in 𝑦) 𝜑 (𝑥) d e f ⟺ (\exists 𝑥) [𝑥 \in 𝑦 \land 𝜑 (𝑥)] (\forall 𝑥 \in 𝑦) 𝜑 (𝑥) d e f ⟺ (\forall 𝑥) [𝑥 \in 𝑦 \Rightarrow 𝜑 (𝑥)]

We also have the following abbreviation for nonexistence

(∄ 𝑥) 𝜑 (𝑥) d e f ⟺ \neg (\exists 𝑥) 𝜑 (𝑥)

#state/develop | #lang/en | #SemBr

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

Conventions of 1st-order logic in these notes

Quantification

Footnotes

Conventions of $1$ st-order logic in these notes