Documentation

DescriptiveComplexity.Problems.FinSat.Reduction

The reduction to FINSAT, and its correctness #

DescriptiveComplexity.FinSat.Hardness evaluates the encoded sentence σ_A node by node; this file closes the two directions and assembles the ordered first-order reduction.

The two remaining pieces of bookkeeping the converse needs are here too: the truth definition at the nodes only the converse inspects (the prefix, the top conjunction and a distinctness literal), and the fact that Gval only sees an interpretation at the symbols some node carries (DescriptiveComplexity.FinSat.gval_congr_I), which is what lets the model's own interpretation be replaced by the one a block assignment induces.

The head of a one-block second-order satisfaction #

source
theorem DescriptiveComplexity.FinSat.sorealize_head_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A' : Type} [(newLang L).Structure A'] :
SORealize (newLang L) A' [B] φ true ↔ ∃ (μ : B.Assignment A'), Tseitin.RealizeWith μ φ finZeroElim

Realization of a one-block ∃SO sentence is realization of its kernel in the expansion by an assignment.

Dependency graph

The extended universe reads the instance through Sum.inl #

The two facts about the model that the kernel recursion (DescriptiveComplexity.FinSat.gval_kernel) asks for, on the extended structure.

source
theorem DescriptiveComplexity.FinSat.relMap_ext_iff' {L : FirstOrder.Language} {A : Type} [L.Structure A] [Nonempty A] {m k : ℕ} (r : L.Relations k) (u : Fin k → A ⊕ Fin m) :
FirstOrder.Language.Structure.RelMap (Sum.inl r) u ↔ ∃ (y : Fin k → A), FirstOrder.Language.Structure.RelMap r y ∧ ∀ (j : Fin k), u j = Sum.inl (y j)
Dependency graph
source
theorem DescriptiveComplexity.FinSat.relMap_ext_old' {L : FirstOrder.Language} {A : Type} [L.Structure A] [Nonempty A] {m : ℕ} (u : Fin 1 → A ⊕ Fin m) :
FirstOrder.Language.Structure.RelMap (Sum.inr FirstOrder.Language.oldSym) u ↔ ∃ (a : A), u 0 = Sum.inl a
Dependency graph

⟹ : an assignment of the block is a model of the encoded sentence #

source
theorem DescriptiveComplexity.FinSat.finSatOn_of_realizeWith {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] [L.IsRelational] [Finite A] [Nonempty A] {m : ℕ} (μ : B.Assignment (A ⊕ Fin m)) (hμ : Tseitin.RealizeWith μ φ finZeroElim) :
FinSatOn ((finsatInterp B φ).Map A)

The image of a yes-instance is finitely satisfiable: the extended universe carrying the assignment is a model of σ_A, with Sum.inl as the intended assignment of the prefix variables.

Dependency graph

The nodes only the converse inspects #

Reading a model of σ_A means going through the truth definition at the nodes the ⟹ direction only had to build: a node of the existential prefix, the top conjunction, and a distinctness literal of the diagram. As everywhere, the clauses that cannot fire are ruled out by the tag.

source
theorem DescriptiveComplexity.FinSat.not_eqG_tag {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t : FTag B φ) (ht : ∀ (t' t'' : FTag B φ), eqBodyF B φ t t' t'' = ⊥) (w : Fin (tagDim B φ t) → A) (x y : (finsatInterp B φ).Map A) :
¬EqG (ptOf B φ a₀ t w) x y

A tag no positive equality literal is defined at carries none.

Dependency graph
source
theorem DescriptiveComplexity.FinSat.not_neqG_tag {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t : FTag B φ) (ht : ∀ (t' t'' : FTag B φ), neqBodyF B φ t t' t'' = ⊥) (w : Fin (tagDim B φ t) → A) (x y : (finsatInterp B φ).Map A) :
¬NeqG (ptOf B φ a₀ t w) x y

The same for the negated equality literals.

Dependency graph
source
theorem DescriptiveComplexity.FinSat.bindG_pre_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (a : A) (x : (finsatInterp B φ).Map A) :
BindG (prePt B φ a₀ a) x ↔ x = pvarPt B φ a₀ a

A node of the prefix binds its own variable, and nothing else.

Dependency graph
source
theorem DescriptiveComplexity.FinSat.neqG_neq_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (a b : A) (x y : (finsatInterp B φ).Map A) :
NeqG (neqPt B φ a₀ a b) x y ↔ a ≠ b ∧ x = pvarPt B φ a₀ a ∧ y = pvarPt B φ a₀ b

A distinctness literal of the diagram, inverted: it exists only for a distinct pair, and relates the two prefix variables of that pair.

Dependency graph
source
theorem DescriptiveComplexity.FinSat.gstep_pre {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (rec : ((finsatInterp B φ).Map A → M) → (finsatInterp B φ).Map A → Prop) (v : (finsatInterp B φ).Map A → M) (a : A) :
gstep I rec v (prePt B φ a₀ a) ↔ ∃ (d : M) (c : (finsatInterp B φ).Map A), ChildG (prePt B φ a₀ a) c ∧ rec (upd v (pvarPt B φ a₀ a) d) c

The truth definition at a node of the existential prefix: it binds its own variable, so the only clause that can fire hands over a value for it.

Dependency graph
source
theorem DescriptiveComplexity.FinSat.gstep_body {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (rec : ((finsatInterp B φ).Map A → M) → (finsatInterp B φ).Map A → Prop) (v : (finsatInterp B φ).Map A → M) :
gstep I rec v (bodyPt B φ a₀) ↔ ∀ (c : (finsatInterp B φ).Map A), ChildG (bodyPt B φ a₀) c → rec v c

The truth definition at the top conjunction.

Dependency graph
source
theorem DescriptiveComplexity.FinSat.gstep_neq {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (rec : ((finsatInterp B φ).Map A → M) → (finsatInterp B φ).Map A → Prop) (v : (finsatInterp B φ).Map A → M) (a b : A) :
gstep I rec v (neqPt B φ a₀ a b) ↔ a ≠ b ∧ v (pvarPt B φ a₀ a) ≠ v (pvarPt B φ a₀ b)

The truth definition at a distinctness literal of the diagram.

Dependency graph
source
theorem DescriptiveComplexity.FinSat.gval_pre_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (v : (finsatInterp B φ).Map A → M) (a : A) :
Gval I v (prePt B φ a₀ a) ↔ ∃ (d : M) (c : (finsatInterp B φ).Map A), ChildG (prePt B φ a₀ a) c ∧ Gval I (upd v (pvarPt B φ a₀ a) d) c
Dependency graph
source
theorem DescriptiveComplexity.FinSat.gval_body_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (v : (finsatInterp B φ).Map A → M) :
Gval I v (bodyPt B φ a₀) ↔ ∀ (c : (finsatInterp B φ).Map A), ChildG (bodyPt B φ a₀) c → Gval I v c
Dependency graph
source
theorem DescriptiveComplexity.FinSat.gval_neq_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (v : (finsatInterp B φ).Map A → M) (a b : A) :
Gval I v (neqPt B φ a₀ a b) ↔ a ≠ b ∧ v (pvarPt B φ a₀ a) ≠ v (pvarPt B φ a₀ b)
Dependency graph
source
theorem DescriptiveComplexity.FinSat.exists_body_env {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (a : A) (v : (finsatInterp B φ).Map A → M) :
Gval I v (prePt B φ a₀ a) → ∃ (v' : (finsatInterp B φ).Map A → M), (∀ b < a, v' (pvarPt B φ a₀ b) = v (pvarPt B φ a₀ b)) ∧ Gval I v' (bodyPt B φ a₀)

The witnesses of the prefix, read off a model: from the node of a the truth definition hands over a value for x_a and passes to the next node, so an induction along the input order produces an environment satisfying the top conjunction and agreeing with the given one below a.

Dependency graph

The interpretation a model carries is a block assignment #

The truth definition reads an interpretation only at the symbols some node carries, and those are exactly the symbols of the relation variables. So the model's own interpretation may be replaced by the one induced by the assignment that reads it back – which is what turns a model of σ_A into a witness of the ∃SO[new] definition.

source
theorem DescriptiveComplexity.FinSat.gval_congr_I {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {M : Type} {I I' : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop} (h : ∀ (s : (finsatInterp B φ).Map A) (w : (finsatInterp B φ).Map A → M), (∃ (g : (finsatInterp B φ).Map A), PosG g s ∨ NegG g s) → (I s w ↔ I' s w)) (k : ℕ) (v : (finsatInterp B φ).Map A → M) (g : (finsatInterp B φ).Map A) :
gval I k v g → gval I' k v g

Gval only sees an interpretation at the symbols of the atoms.

Dependency graph
source
theorem DescriptiveComplexity.FinSat.eq_aposPt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) {x : (finsatInterp B φ).Map A} {j : Fin (finsatDim B φ)} (ht : x.1 = Tag.apos j) (h : Canon 0 x.2) :
x = aposPt B φ a₀ j

An element canonical at dimension zero carrying the tag of an argument position is that position.

Dependency graph
source
theorem DescriptiveComplexity.FinSat.aposPt_inj {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {a₀ : A} {j j' : Fin (finsatDim B φ)} (h : aposPt B φ a₀ j = aposPt B φ a₀ j') :
j = j'
Dependency graph
source
noncomputable def DescriptiveComplexity.FinSat.blockOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A M : Type} (a₀ : A) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (junk : M) :
B.Assignment M

The block assignment a model's interpretation carries: the relation of a variable is its symbol's, read at an assignment of the argument positions holding the tuple.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    theorem DescriptiveComplexity.FinSat.blockOf_agree {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} (ha₀ : IsBot a₀) {I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop} (hloc : Local I) (junk : M) (i : B.ι) (hari : B.arity i ≤ finsatDim B φ) (w : (finsatInterp B φ).Map A → M) :
    I (symPt B φ a₀ i) w ↔ blockI B φ a₀ (blockOf B φ a₀ I junk) (symPt B φ a₀ i) w

    It reads the interpretation back: at the symbol of a relation variable whose arity fits in the dimension, the interpretation induced by that assignment is the interpretation itself.

    Dependency graph

    ⟸ : a model of the encoded sentence is an assignment of the block #

    source
    @[instance_reducible]
    def DescriptiveComplexity.FinSat.viaIotaBase {L : FirstOrder.Language} {A : Type} [L.Structure A] {M : Type} [L.IsRelational] (ι : A → M) :
    L.Structure M

    The model, seen through the intended assignment of the prefix variables: a relation of the instance holds of a tuple of the model exactly when the tuple is the image of one where it holds. This is the shape an extended universe has (DescriptiveComplexity.relMap_ext_iff), and all the kernel recursion asks of a model.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Dependency graph
      source
      @[instance_reducible]
      def DescriptiveComplexity.FinSat.viaIotaOld {A M : Type} (ι : A → M) :
      FirstOrder.Language.oldMark.Structure M

      The marking predicate on such a model: the elements in the image.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Dependency graph
        source
        @[instance_reducible]
        def DescriptiveComplexity.FinSat.viaIota {L : FirstOrder.Language} {A : Type} [L.Structure A] {M : Type} [L.IsRelational] (ι : A → M) :
        (newLang L).Structure M

        The model as a structure over DescriptiveComplexity.newLang L.

        Equations
        Instances For
          Dependency graph
          source
          theorem DescriptiveComplexity.FinSat.realizeWith_of_finSatOn {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] [L.IsRelational] [Finite A] [Nonempty A] (hfs : FinSatOn ((finsatInterp B φ).Map A)) :
          ∃ (m : ℕ), SORealize (newLang L) (A ⊕ Fin m) [B] φ true

          A model of the encoded sentence is an extended universe: the intended assignment is injective, so its complement is the invented part.

          Dependency graph

          The reduction #

          source
          theorem DescriptiveComplexity.FinSat.finsat_image_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] [L.IsRelational] [Finite A] [Nonempty A] :
          (∃ (m : ℕ), SORealize (newLang L) (A ⊕ Fin m) [B] φ true) ↔ FinSatOn ((finsatInterp B φ).Map A)

          The image is finitely satisfiable exactly at the yes-instances.

          Dependency graph
          source
          noncomputable def DescriptiveComplexity.FinSat.finsatReduction {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) [L.IsRelational] (Q : DecisionProblem L) (hφ : ∀ (A : Type) [inst : L.Structure A] [Finite A] [inst_2 : Nonempty A], Q.Holds A ↔ ∃ (m : ℕ), SORealize (newLang L) (A ⊕ Fin m) [B] φ true) :
          OrderedFOReduction Q FINSAT

          The reduction to FINSAT: the ordered first-order interpretation sending an instance to the encoded sentence σ_A, from any problem defined, on nonempty finite structures, by an ∃SO[new] sentence with a single block.

          Relational for now: DescriptiveComplexity.CofinalHard admits source languages with function symbols, whose junk interpretation on invented arguments the sentence would have to guess: the term layer, which DescriptiveComplexity.exists_relational_of_sigmaSONewDefinable removes from the source instead.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Dependency graph
            source
            theorem DescriptiveComplexity.FinSat.finsat_hard_of_sigmaSONewDefinable {L : FirstOrder.Language} [L.IsRelational] (Q : DecisionProblem L) :
            SigmaSONewDefinable Q → Nonempty (OrderedFOReduction Q FINSAT)

            Trakhtenbrot's theorem, the hardness half over a relational vocabulary: every ∃SO[new]-definable problem over a relational vocabulary admits an ordered first-order reduction to finite satisfiability.

            Membership is DescriptiveComplexity.FinSat.finsat_mem_RE; together they say that finite satisfiability is complete for ∃SO[new] among relational vocabularies. Lifting the restriction is the term layer, which is what DescriptiveComplexity.RE.Hard – cofinal hardness, quantified over every source vocabulary – additionally asks for; DescriptiveComplexity.exists_relational_of_sigmaSONewDefinable supplies it, and the umbrella composes the two.

            Dependency graph