Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax314295.KTypesFOEquivalence

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

concepts/Lax314295/KTypesFOEquivalence.lean · lax-314295

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    Theorem

    Two strings have the same kk-type if and only if they satisfy the same first-order sentences of quantifier rank at most kk (Lemma C.4.13 of Transducers). From equal types to equal satisfaction is the compositionality of first-order logic: a position chosen on one string can be matched on the other so that all formulas of one rank lower are preserved. Conversely the set of strings of a given kk-type is defined by a first-order sentence of quantifier rank kk, built by induction on kk with quantification relativised to the two sides of a chosen position.

    Lean source view on GitHub

    1import Lax314295.MSOLogic
    2import Lax314295.KTypes
    3
    4/-!
    5---
    6title: k-types capture first-order sentences of quantifier rank k
    7type: theorem
    8---
    9Two strings have the same kk-type if and only if they satisfy the same
    10first-order sentences of quantifier rank at most kk (Lemma C.4.13 of
    11*Transducers*). From equal types to equal satisfaction is the compositionality
    12of first-order logic: a position chosen on one string can be matched on the
    13other so that all formulas of one rank lower are preserved. Conversely the set
    14of strings of a given kk-type is defined by a first-order sentence of
    15quantifier rank kk, built by induction on kk with quantification relativised
    16to the two sides of a chosen position.
    17
    18# Formalization notes
    19
    20The book says "formulas" where it means "sentences": satisfaction of a formula
    21with free variables has no meaning without a valuation. The statement therefore
    22quantifies over first-order formulas without free first-order variables,
    23satisfied under every valuation — which for a sentence is just satisfaction.
    24The alphabet is assumed finite.
    25-/
    26
    27namespace Lax314295.KTypesFOEquivalence
    28
    29open Lax314295.MSOLogic Lax314295.KTypes
    30
    31/-- Two strings have the same `k`-type if and only if they satisfy the same
    32first-order sentences of quantifier rank at most `k`. -/
    33axiom tp_eq_iff_fo_equiv {A : Type} [Finite A] (k : ℕ) (w v : List A) :
    34 tp k w = tp k v ↔
    35 ∀ φ : MSO A, φ.IsFO → φ.freeFO = ∅ → φ.qrank ≤ k →
    36 ((∀ fo so, MSO.Sat w fo so φ) ↔ (∀ fo so, MSO.Sat v fo so φ))
    37
    38end Lax314295.KTypesFOEquivalence
    39
    Show Proof

    Formalization notes

    The book says "formulas" where it means "sentences": satisfaction of a formula with free variables has no meaning without a valuation. The statement therefore quantifies over first-order formulas without free first-order variables, satisfied under every valuation — which for a sentence is just satisfaction. The alphabet is assumed finite.

    Builds on

    Used by

    none

    From Mathlib

    none

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…