Minimal predicates P satisfying a given first-order description φ(P)
occur widely in mathematical logic and computer science. We give
an explicit first-order syntax for special first-order ‘PIA
conditions’ φ(P) which guarantees unique existence
of such minimal predicates. Our main technical result is a preservation
theorem showing PIA-conditions to be expressively complete
for all those first-order formulas that are preserved under a
natural model-theoretic operation of ‘predicate intersection’.
Next, we show how iterated predicate minimization on PIA-conditions
yields a language MIN(FO) equal in expressive power to LFP(FO),
first-order logic closed under smallest fixed-points for monotone
operations. As a concrete illustration of these notions, we show
how our sort of predicate minimization extends the usual frame
correspondence theory of modal logic, leading to a proper hierarchy
of modal axioms: first-order-definable, first-order fixed-point
definable, and beyond.