Predicate logic builds on Propositional logic and adds variables, quantifiers (there-exists and for-all), and often equality. This page serves as an index for proof modules and interfaces in this area.

##
First-order logic

In first-order logic a quantifier is for a variable (not for a predicate or some higher-level concept).

The next few pages add the ability to substitute a term for a variable.

Those pages prove the following interface, which is the predicate logic used by most of the `general` pages.