Lax Lean Archive

Invariance and characterization of finite satisfiability

Lax624099.FiniteSatisfiabilityInvariance · concepts/Lax624099/FiniteSatisfiabilityInvariance.lean · lax-624099

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.

    Natural Language Statement

    Lemma

    Finite satisfiability of an encoded sentence is invariant under isomorphism of instances, and an instance is a yes-instance of FINSAT exactly when its encoded sentence has a finite model.

    Concept map
    15 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 finsat_iff proven

    2 finSatOn_iso proven

    Lean source view on GitHub

    1import Lax904597.Problems
    2import Lax904597.Interpretations
    3import Lax904597.Relativized
    4import Lax904597.Classes
    5import Lax624099.Problems
    6import Lax624099.ValueInvention
    7import Lax624099.ClassRE
    8import Lax624099.FiniteSatisfiability
    9import Lax624099.Halting
    10import Lax624099.CodeHalting
    11import Lax624099.PostCorrespondence
    12import Lax624099.ConcreteInstances
    13import Lax904597.Machines
    14
    15/-!
    16---
    17title: Invariance and characterization of finite satisfiability
    18type: lemma
    19---
    20Finite satisfiability of an encoded sentence is invariant under isomorphism of
    21instances, and an instance is a yes-instance of FINSAT exactly when its
    22encoded sentence has a finite model.
    23-/
    24
    25namespace Lax624099.FiniteSatisfiabilityInvariance
    26
    27open FirstOrder FirstOrder.Language
    28open Lax904597.Problems Lax904597.Interpretations Lax904597.Relativized Lax904597.Classes
    29open Lax904597.Machines Lax624099.Problems Lax624099.ValueInvention Lax624099.ClassRE
    30open Lax624099.FiniteSatisfiability
    31open Lax624099.Halting Lax624099.CodeHalting Lax624099.PostCorrespondence
    32open Lax624099.ConcreteInstances
    33
    34/-- The property `FinSat.FinSatOn` is isomorphism-invariant. -/
    35axiom finSatOn_iso : ∀ {A B : Type} [finsat.Structure A] [finsat.Structure B],
    36 (A ≃[finsat] B) → (FinSat.FinSatOn A ↔ FinSat.FinSatOn B)
    37
    38/-- The yes-instances of FINSAT are exactly the satisfiable encoded
    39sentences. -/
    40axiom finsat_iff : ∀ (A : Type) [finsat.Structure A], FINSAT A ↔ FinSat.FinSatOn A
    41
    42end Lax624099.FiniteSatisfiabilityInvariance
    43
    Show ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…