Certified synthesis of formulas with logical operators

fo_definable proves uniform definability of an ordinary Lean predicate by constructing a well-formed formula, using the extensible Aesop rule set FODefinable. Its witness is a single formula for the whole family of structures, rather than a formula chosen separately for each structure. The built-in rules cover first-order atoms, Boolean connectives, and quantification.

To add a semantic operation, prove a theorem whose conclusion is Operator.Definable and register it with @[aesop safe apply (rule_sets := [FODefinable])]. The theorem must supply a well-formed formula and prove its meaning; Definable.of_formula provides the explicit-witness entry point. Free-variable renaming and equivalent semantic presentations are also available through Definable.relabel and Definable.congr. When the search fails, its error ends with a note giving these options.

Synthesis does not unfold fixed points or search over arbitrary formulas. Semantic reasoning about an explicit formula continues to use the existing fo_realize simp set. In particular, fixed-point unfolding is not a global simplification rule.

Main definitions

• fo_definable: synthesize a uniformly defining, well-formed formula from registered rules.
• fo_wf: check formation conditions of explicit syntax, with optional simplification lemmas.

def foDefinable : Lean.ParserDescr

Construct a well-formed defining formula by composing registered semantic certificates.

def evalFoDefinable : Lean.Elab.Tactic.Tactic

Elaborate fo_definable: search the FODefinable rule set, with a note on failure.

def foWf : Lean.ParserDescr

Prove the formation conditions of explicit formula syntax. fo_wf [φ, policy] unfolds named formulas and formation policies in addition to the structural checks. The tactic fails unless it closes the goal; it never assumes positivity of a recursive relation.