Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Gaifman's Theorem

lax-512892·formalized by Fatemeh Ghasemi @faghasemi·created ·GitHub @4e1cc75·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

Community review

Flags

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

No flags have been submitted.

    Community review

    Flag this submission

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

    Abstract

    This submission formalizes Gaifman's normal-form theorem for first-order logic over finite relational vocabularies. It develops the syntax and semantics of relational structures and first-order formulas, the associated Gaifman graph and its metric neighborhoods, local formulas, and uniform basic local sentences.

    The main result states that every first-order formula is equivalent to a Boolean combination of formulas local around its free variables and sentences asserting the existence of pairwise distant witnesses satisfying one fixed local formula. The formalization follows Gaifman's original theorem and the uniform formulation in Libkin's Elements of Finite Model Theory.

    Concepts

    Concept map
    4 concepts
    100%
    Open claimDefinitionThis submissionA → B: B builds on A

    Proofs

    No proofs in this submission.

    Related submissions

    No other submission in the archive builds on this one, and this one builds on none.

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-512892,
  author = {Fatemeh Ghasemi},
  title = {Gaifman's Theorem},
  year = {2026},
  howpublished = {Lax Archive, lax-512892},
  url = {https://laxarchive.org/lax-512892/},
  note = {draft},
}

    References

    1. Haim Gaifman. On Local and Non-Local Properties. In Proceedings of the Herbrand Symposium 107:105–135, 1982. doi:10.1016/S0049-237X(08)71879-2
    2. Leonid Libkin. Elements of Finite Model Theory. Springer, 2004. doi:10.1007/978-3-662-07003-1

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…