5.1. Binding and Interpretation🔗

Cslib.Logic.FO.Operator.Shape records the number of term arguments, the number of formula bodies, and the local binders of each body. Each binder lists its relation arities and its number of first-order variables. A body keeps ambient parameters under Sum.inl and sees its new tuple variables under Sum.inr.

Cslib.Logic.FO.Operator.Formula uses Mathlib's native first-order terms and formulas for its base language. A relation context is a list of arities: RelVar.here denotes the nearest relation binder, and RelVar.there passes an inner binder to reach an outer variable. An interpretation supplies the meaning of each operator; binding itself is independent of that meaning.

Reusable formulas can move beneath a new relation binder with (φ.weakenRel [k]).relabel Sum.inl. The first operation shifts outer relation variables; the second shifts the free first-order parameters. Local binders inside φ remain local. The Cslib.Logic.FO.Operator.Formula.realize_weakenRel theorem shows that the new relation's value cannot affect the weakened formula, and both operations preserve formation checks.