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.
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.