Proof of `Formulas with free variables define regular languages of annotated strings`

groundedproofs/Lax314295Proofs/Results.lean · lax-314295

What this proof establishes

no assumptions

thm✓Lax314295.MSOFreeVariables

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

In the paper

page 119 of the paper of lax-157538, Transducers

Description

The annotated strings satisfying a formula with free variables form a regular language (Lemma C.4.2): induction on the formula, with projection for the quantifiers ( $Transducers.mso_annotated_regular$ ).

Proof strategy

The concept's $annotate$ , $extFO$ and $extSO$ are the source's by $rfl$ ; the formula is transported along $toSrc$ , which preserves the free variables ( $freeFO_toSrc$ , $freeSO_toSrc$ ) and satisfaction ( $sat_toSrc$ ), so the two languages are equal by extensionality.

Attribution

Lemma C.4.2 of Transducers, Part C; formalised by Aristotle (Harmonic), $PartC/MSOAnnot.lean$ , $PartC/MSO.lean$ .

Lax Lean Archive