1st-order logic

Conventions of st-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 is a type, then either of the following notations may be used for “there exists of type satisfying ” (the notation for the universal quantifier is similar)

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

and if is a binary predicate,

We also have the following abbreviation for nonexistence

---

develop | en | sembr

Footnotes

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