Proof of `k-types capture first-order sentences of quantifier rank k`

groundedproofs/Lax314295Proofs/Results.lean · lax-314295

What this proof establishes

no assumptions

thm✓Lax314295.KTypesFOEquivalence

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 132 of the paper of lax-157538, Transducers

Description

Two strings have the same $k$ -type if and only if they satisfy the same first-order sentences of quantifier rank at most $k$ (Lemma C.4.13): compositionality of first-order logic for the direction from types to sentences, and Hintikka sentences describing the $k$ -type for the converse ( $Transducers.tp_eq_iff_fo_equiv$ ).

Proof strategy

The concept's $k$ -types are the source's through the bijection $tpEquiv$ ( $tp_eq_iff$ ); the quantification over concept sentences is turned into one over source sentences along $toSrc$ / $ofSrc$ , which preserve the first-order fragment, the free variables, the quantifier rank and satisfaction.

Attribution

Lemma C.4.13 of Transducers, Part C; formalised by Aristotle (Harmonic), $PartC/FOComp.lean$ , $PartC/FOHintikka.lean$ , $PartC/MSO.lean$ .

Lax Lean Archive