5. First-Order Logic with Operators🔗

First-order formulas often describe a local step: two vertices share an edge, a tuple satisfies a constraint, or a relation gains a new tuple. Logical operators turn those steps into paths or least fixed points. The library provides a shared syntax for these extensions, concrete FO(LFP) and FO(TC) interpretations, and certificates that construct formulas from ordinary Lean predicates.

1. 5.1. Binding and Interpretation
2. 5.2. Least Fixed Points
3. 5.3. Capturing Polynomial Time
4. 5.4. Tuple Reachability
5. 5.5. Constructing Formulas from Predicates
6. 5.6. Adding Other Operators