Lax Lean Archive

Relativized first-order interpretations

Lax904597.Relativized · concepts/Lax904597/Relativized.lean · lax-904597

definition

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

    Definition

    A relativized interpretation adds to a first-order interpretation a domain formula for each tag: the universe of the interpreted structure is the definable subset of the tagged tuples whose coordinates satisfy their tag's domain formula. This is the textbook universe of an interpretation, needed when the target universe is not a product; a relativized ordered reduction asks in addition that the domain be inhabited on every finite nonempty ordered input. Cofinal hardness is stated with these reductions, so that it travels forward along reductions out of arbitrary vocabularies.

    Concept map
    3 concepts; 4 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax904597.Interpretations
    2
    3/-!
    4---
    5title: Relativized first-order interpretations
    6type: definition
    7---
    8A *relativized* interpretation adds to a first-order interpretation a domain
    9formula for each tag: the universe of the interpreted structure is the
    10definable subset of the tagged tuples whose coordinates satisfy their tag's
    11domain formula. This is the textbook universe of an interpretation, needed
    12when the target universe is not a product; a relativized ordered reduction
    13asks in addition that the domain be inhabited on every finite nonempty
    14ordered input. Cofinal hardness is stated with these reductions, so that it
    15travels forward along reductions out of arbitrary vocabularies.
    16-/
    17
    18namespace Lax904597.Relativized
    19
    20open FirstOrder FirstOrder.Language Lax904597.Problems Lax904597.Interpretations
    21
    22/-- A relativized interpretation: an interpretation together with the domain
    23formula of each tag. -/
    24structure RelFOInterpretation (L L' : Language.{0, 0}) (Tag : Type) (dim : ℕ)
    25 extends FOInterpretation L L' Tag dim where
    26 /-- The domain formula of each tag: a tagged tuple `(t, ā)` belongs to the
    27 target universe iff `domFormula t` holds of `ā`. -/
    28 domFormula : Tag → L.Formula (Fin dim)
    29
    30namespace RelFOInterpretation
    31
    32variable {L L' : Language.{0, 0}} {Tag : Type} {dim : ℕ}
    33variable (I : RelFOInterpretation L L' Tag dim) (A : Type) [L.Structure A]
    34
    35/-- The universe of the relativized interpretation in `A`: the tagged tuples
    36whose coordinates satisfy their tag's domain formula. -/
    37protected def MapRel : Type :=
    38 {x : Tag × (Fin dim → A) // (I.domFormula x.1).Realize x.2}
    39
    40/-- The `L'`-structure interpreted on the definable subset. -/
    41instance mapRelStructure [L'.IsRelational] : L'.Structure (I.MapRel A) where
    42 funMap f := isEmptyElim f
    43 RelMap R xs := (I.relFormula R fun i => (xs i).1.1).Realize fun p => (xs p.1).1.2 p.2
    44
    45end RelFOInterpretation
    46
    47/-- A relativized ordered first-order reduction from `P` to `Q`. -/
    48structure RelOrderedFOReduction {L L' : Language.{0, 0}} [L.IsRelational] [L'.IsRelational]
    49 (P : DecisionProblem L) (Q : DecisionProblem L') where
    50 /-- The tags used by the underlying interpretation. -/
    51 Tag : Type
    52 /-- Tags are finite, so that finite structures map to finite structures. -/
    53 [tagFinite : Finite Tag]
    54 /-- The dimension of the underlying interpretation. -/
    55 dim : ℕ
    56 /-- The underlying relativized interpretation, over the ordered expansion. -/
    57 toRelInterpretation : RelFOInterpretation (L.sum Language.order) L' Tag dim
    58 /-- The definable domain is inhabited: some tagged tuple satisfies its tag's
    59 domain formula. -/
    60 dom_nonempty : ∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A],
    61 ∃ (t : Tag) (w : Fin dim → A), (toRelInterpretation.domFormula t).Realize w
    62 /-- Yes-instances map exactly to yes-instances, whatever the linear order. -/
    63 correct : ∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A],
    64 P A ↔ Q (toRelInterpretation.MapRel A)
    65
    66end Lax904597.Relativized
    67
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…