5.6. Adding Other Operators🔗

Cslib.Logic.FO.Operator.Policy declares each body's variance and its locally positive relation variables. An interpretation proves Cslib.Logic.FO.Operator.Interpretation.Respects for that variance. Positive slots preserve implication; negative slots reverse it; arbitrary slots require equivalence. The polarity checker propagates these requirements through nesting.

A regular-language quantifier can use this binding interface and declare arbitrary variance for a body whose changes are not monotone. In a recursive context, that declaration requires both polarity checks and conservatively excludes dependence on the recursive relation. The interface supports such an extension; no REG interpretation or FO(REG) capture theorem is implemented here.

The operator examples exercise nesting, rejected negative recursion, finite iteration, relation weakening, empty domains, and formula synthesis. The model-checker tests cover executable iteration and encoding rejection; the capture tests use the public characterization and native input-symbol formulas.