First order logic Glossary
First order logic allows quantification over the set of individuals constituting the domain of an interpretation. Those individuals can be named and described using predicates interpreted as functions from individuals to truth values.
Crucially, predicate symbols and function symbols cannot be bound by quantifiers, as relations and functions defined on the domain are not objects which can be named. Logic in which functions and relations are treated as first-class objects are higher order, not first order.
Sometimes propositional logic is considered to be part of first order logic. The definitions used in these notes allow for this usage. However, the propositional (quantifier-free) fragment is so different from first order logic with quantifiers that it makes sense to think of it as a separate system—zero order logic, if we like.
The logic of Logic for Fun is first order, though it has multiple sorts, meaning multiple domains, instead of just one. It treats the truth values as one of those sorts, so it does allow propositional quantifiers ALLp, SOMEq, etc. which is a small step towards higher order logic.
Set theory is not treated here, beyond the basics needed to describe languages and interpretations. It occupies a special place in logic, being a first order theory designed to simulate higher order reasoning about functions and other such concepts. This actually raises technical difficulties—at the very least, its models have to be described very carefully. For the purposes of these notes, we leave these details unexplored.