Pulling ∃SO[new] definability back through an interpretation

Closure of definability in existential second-order logic with value invention under first-order reductions (DescriptiveComplexity.SigmaSONewDefinable.of_foReduction), the closure that makes RE a DescriptiveComplexity.ComplexityClass.

The construction

Let I be the interpretation of a reduction P ≤ᶠᵒ Q, and let Q be defined by a block B and a kernel φ read in the extended universe I.Map A ⊕ Fin m. The extended universe of the source is A ⊕ Fin m – the same number of invented values – and the point of the construction is that the target's extended universe is definable inside it:

• a point of I.Map A is a tag t together with dim original elements;
• an invented value is an invented value.

Both are tagged tuples, so they are the universe of a relativized interpretation DescriptiveComplexity.newInterp with tags Tag ⊕ Unit and dimension dim + 1, whose domain formula asks, at tag Sum.inl t, that the first dim coordinates be original, and at tag Sum.inr (), that the last coordinate be invented and the others copy it (a diagonal, so that each invented value is one point). The spare coordinate of a Sum.inl point has to be pinned to a single element, for which the block guesses a canonical element (DescriptiveComplexity.canonSym), constrained to be unique by DescriptiveComplexity.canonGuard; pinning it to a coordinate of the tuple would not survive dim = 0, where I.Map A is a constant-size structure.

Everything else is machinery that already exists:

• the kernel is pulled back by the guarded pullback DescriptiveComplexity.RelFOInterpretation.pullRel of DescriptiveComplexity.RelComposition, which relativizes quantifiers to the definable universe and substitutes the defining formulas for atoms;
• the relation variables of B are pulled back exactly as in DescriptiveComplexity.SecondOrderPull, one (k · (dim+1))-ary variable per tuple of tags (DescriptiveComplexity.SOBlock.pull). Their assignments transfer in the flipped direction a definable universe forces: DescriptiveComplexity.targetAssign reads a guessed assignment back on the target's universe, DescriptiveComplexity.sourceAssign extends an assignment of the target's block by junk off the interpreted points, and the composite targetAssign ∘ sourceAssign is the identity on the nose (DescriptiveComplexity.targetAssign_sourceAssign) – which is all an existential block needs;
• the interpretation's own defining formulas quantify over A, so they are read in A ⊕ Fin m relativized to the original elements (DescriptiveComplexity.relOld of DescriptiveComplexity.Relativize).

The pulled block

@[reducible, inline]

abbrev DescriptiveComplexity.newBlock (Tag : Type) [Finite Tag] (dim : ℕ) (B : SOBlock) : SOBlock

The block guessed on the source side: a canonical element (used to pin the spare coordinate of an interpreted point) together with the pullback of the target's block through the interpretation below.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.canonSym (Tag : Type) [Finite Tag] (dim : ℕ) (B : SOBlock) : (newBlock Tag dim B).lang.Relations 1

The canonical-element variable of the guessed block.

Equations

• DescriptiveComplexity.canonSym Tag dim B = ⟨Sum.inl (), ⋯⟩

def DescriptiveComplexity.newPullSym (Tag : Type) [Finite Tag] (dim : ℕ) (B : SOBlock) {k : ℕ} (r : B.lang.Relations k) (τ : Fin k → Tag ⊕ Unit) : (newBlock Tag dim B).lang.Relations (B.arity ↑r * (dim + 1))

The pulled relation variable of the target's block selected by a tuple of tags.

Equations

• DescriptiveComplexity.newPullSym Tag dim B r τ = ⟨Sum.inr ⟨↑r, fun (j : Fin (B.arity ↑r)) => τ (Fin.cast ⋯ j)⟩, ⋯⟩

@[reducible, inline]

abbrev DescriptiveComplexity.canonPart {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} {M : Type} (ρ : (newBlock Tag dim B).Assignment M) : M → Prop

The canonical-element part of a guessed assignment.

Equations

• DescriptiveComplexity.canonPart ρ c = ρ (Sum.inl ()) ![c]

@[reducible, inline]

abbrev DescriptiveComplexity.pullPart {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} {M : Type} (ρ : (newBlock Tag dim B).Assignment M) : (SOBlock.pull (Tag ⊕ Unit) (dim + 1) B).Assignment M

The pulled-block part of a guessed assignment: an assignment of the block pulled back through the interpretation below.

Equations

• DescriptiveComplexity.pullPart ρ p = ρ (Sum.inr p)

def DescriptiveComplexity.joinParts {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} {M : Type} (c : (Fin 1 → M) → Prop) (σ : (SOBlock.pull (Tag ⊕ Unit) (dim + 1) B).Assignment M) : (newBlock Tag dim B).Assignment M

A guessed assignment, from its two parts.

Equations

• DescriptiveComplexity.joinParts c σ (Sum.inl val) = c
• DescriptiveComplexity.joinParts c σ (Sum.inr p) = σ p

theorem DescriptiveComplexity.canonPart_joinParts {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} {M : Type} (c : (Fin 1 → M) → Prop) (σ : (SOBlock.pull (Tag ⊕ Unit) (dim + 1) B).Assignment M) (x : M) : canonPart (joinParts c σ) x ↔ c ![x]

theorem DescriptiveComplexity.pullPart_joinParts {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} {M : Type} (c : (Fin 1 → M) → Prop) (σ : (SOBlock.pull (Tag ⊕ Unit) (dim + 1) B).Assignment M) : pullPart (joinParts c σ) = σ

The two vocabularies

@[reducible, inline]

abbrev DescriptiveComplexity.newHost (L₁ : FirstOrder.Language) (Tag : Type) [Finite Tag] (dim : ℕ) (B : SOBlock) : FirstOrder.Language

The vocabulary the pulled-back kernel is written in: the source vocabulary, the marker old, and the guessed relation variables.

Equations

• DescriptiveComplexity.newHost L₁ Tag dim B = (DescriptiveComplexity.newLang L₁).sum (DescriptiveComplexity.newBlock Tag dim B).lang

@[reducible, inline]

abbrev DescriptiveComplexity.newTarget (L₂ : FirstOrder.Language) (B : SOBlock) : FirstOrder.Language

The vocabulary the target's kernel is written in.

Equations

• DescriptiveComplexity.newTarget L₂ B = (DescriptiveComplexity.newLang L₂).sum B.lang

@[reducible, inline]

abbrev DescriptiveComplexity.tgtBaseSym (L₂ : FirstOrder.Language) (B : SOBlock) {k : ℕ} (R : L₂.Relations k) : (newTarget L₂ B).Relations k

A symbol of the target vocabulary, as a symbol of the extended one.

Equations

• DescriptiveComplexity.tgtBaseSym L₂ B R = Sum.inl (Sum.inl R)

@[reducible, inline]

abbrev DescriptiveComplexity.tgtOldSym (L₂ : FirstOrder.Language) (B : SOBlock) : (newTarget L₂ B).Relations 1

The marker old of the target's extended vocabulary.

Equations

• DescriptiveComplexity.tgtOldSym L₂ B = Sum.inl (Sum.inr FirstOrder.Language.oldSym)

@[reducible, inline]

abbrev DescriptiveComplexity.tgtBlockSym (L₂ : FirstOrder.Language) (B : SOBlock) {k : ℕ} (r : B.lang.Relations k) : (newTarget L₂ B).Relations k

A relation variable of the target's block, as a symbol.

Equations

• DescriptiveComplexity.tgtBlockSym L₂ B r = Sum.inr r

The interpretation of the target's extended universe

@[reducible, inline]

abbrev DescriptiveComplexity.oldHostSym (L₁ : FirstOrder.Language) (Tag : Type) [Finite Tag] (dim : ℕ) (B : SOBlock) : (newHost L₁ Tag dim B).Relations 1

The marker old, as a symbol of the host vocabulary.

Equations

• DescriptiveComplexity.oldHostSym L₁ Tag dim B = Sum.inl (Sum.inr FirstOrder.Language.oldSym)

@[reducible, inline]

abbrev DescriptiveComplexity.canonHostSym (L₁ : FirstOrder.Language) (Tag : Type) [Finite Tag] (dim : ℕ) (B : SOBlock) : (newHost L₁ Tag dim B).Relations 1

The canonical-element variable, as a symbol of the host vocabulary.

Equations

• DescriptiveComplexity.canonHostSym L₁ Tag dim B = Sum.inr (DescriptiveComplexity.canonSym Tag dim B)

@[reducible, inline]

abbrev DescriptiveComplexity.blockHostSym (L₁ : FirstOrder.Language) (Tag : Type) [Finite Tag] (dim : ℕ) (B : SOBlock) {k : ℕ} (r : B.lang.Relations k) (τ : Fin k → Tag ⊕ Unit) : (newHost L₁ Tag dim B).Relations (B.arity ↑r * (dim + 1))

A pulled relation variable, as a symbol of the host vocabulary.

Equations

• DescriptiveComplexity.blockHostSym L₁ Tag dim B r τ = Sum.inr (DescriptiveComplexity.newPullSym Tag dim B r τ)

def DescriptiveComplexity.oldHostF (L₁ : FirstOrder.Language) (Tag : Type) [Finite Tag] (dim : ℕ) (B : SOBlock) {α : Type} (x : α) : (newHost L₁ Tag dim B).Formula α

old x, as a formula over the host vocabulary.

Equations

• DescriptiveComplexity.oldHostF L₁ Tag dim B x = (DescriptiveComplexity.oldHostSym L₁ Tag dim B).formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.canonHostF (L₁ : FirstOrder.Language) (Tag : Type) [Finite Tag] (dim : ℕ) (B : SOBlock) {α : Type} (x : α) : (newHost L₁ Tag dim B).Formula α

C x, the canonical-element variable, as a formula over the host vocabulary.

Equations

• DescriptiveComplexity.canonHostF L₁ Tag dim B x = (DescriptiveComplexity.canonHostSym L₁ Tag dim B).formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.newDom (L₁ : FirstOrder.Language) (Tag : Type) [Finite Tag] (dim : ℕ) (B : SOBlock) : Tag ⊕ Unit → (newHost L₁ Tag dim B).Formula (Fin (dim + 1))

The domain formula: a Sum.inl t point is a tuple of original elements with its spare coordinate pinned to the canonical element; a Sum.inr () point is a diagonal tuple of one invented value.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.newRelF (L₁ : FirstOrder.Language) {L₂ : FirstOrder.Language} (Tag : Type) [Finite Tag] (dim : ℕ) (B : SOBlock) (I : FOInterpretation L₁ L₂ Tag dim) {k : ℕ} : (newTarget L₂ B).Relations k → (Fin k → Tag ⊕ Unit) → (newHost L₁ Tag dim B).Formula (Fin k × Fin (dim + 1))

The defining formulas: a symbol of the target vocabulary holds of interpreted points exactly when the reduction's own defining formula holds of their coordinates (read among the original elements), it never holds of an invented point; old marks the interpreted points; a relation variable of the target's block is read off the pulled variable selected by the tags.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.newRelF L₁ Tag dim B I (Sum.inl (Sum.inr FirstOrder.Language.oldRel.old)) τ_1 = if (τ_1 0).isLeft = true then ⊤ else ⊥

noncomputable def DescriptiveComplexity.newInterp (L₁ : FirstOrder.Language) {L₂ : FirstOrder.Language} (Tag : Type) [Finite Tag] (dim : ℕ) (B : SOBlock) (I : FOInterpretation L₁ L₂ Tag dim) : RelFOInterpretation (newHost L₁ Tag dim B) (newTarget L₂ B) (Tag ⊕ Unit) (dim + 1)

The interpretation of the target's extended universe in the source's: tagged (dim+1)-tuples, an interpreted point per tag of the reduction and an invented value per diagonal.

Equations

• DescriptiveComplexity.newInterp L₁ Tag dim B I = { relFormula := fun {n : ℕ} => DescriptiveComplexity.newRelF L₁ Tag dim B I, domFormula := DescriptiveComplexity.newDom L₁ Tag dim B }

noncomputable def DescriptiveComplexity.canonGuard (L₁ : FirstOrder.Language) (Tag : Type) [Finite Tag] (dim : ℕ) (B : SOBlock) : (newHost L₁ Tag dim B).Sentence

The guard: the canonical-element variable holds of exactly one element.

Equations

• DescriptiveComplexity.canonGuard L₁ Tag dim B = FirstOrder.Language.Formula.iExsUnique (Fin 1) (DescriptiveComplexity.canonHostF L₁ Tag dim B (Sum.inr 0))

Realization in the host structure

@[instance_reducible]

noncomputable def DescriptiveComplexity.hostStruc {L₁ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} (A : Type) [L₁.Structure A] [Nonempty A] (n : ℕ) (ρ : (newBlock Tag dim B).Assignment (A ⊕ Fin n)) : (newHost L₁ Tag dim B).Structure (A ⊕ Fin n)

The host structure: the extended structure of the instance, expanded by the guessed relation variables.

Equations

• DescriptiveComplexity.hostStruc A n ρ = (DescriptiveComplexity.newLang L₁).sumStructure (DescriptiveComplexity.newBlock Tag dim B).lang (A ⊕ Fin n)

theorem DescriptiveComplexity.realize_oldHostF {L₁ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} {A : Type} [L₁.Structure A] [Nonempty A] {n : ℕ} {ρ : (newBlock Tag dim B).Assignment (A ⊕ Fin n)} {α : Type} (x : α) (v : α → A ⊕ Fin n) : (oldHostF L₁ Tag dim B x).Realize v ↔ IsOld (v x)

theorem DescriptiveComplexity.realize_canonHostF {L₁ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} {A : Type} [L₁.Structure A] [Nonempty A] {n : ℕ} {ρ : (newBlock Tag dim B).Assignment (A ⊕ Fin n)} {α : Type} (x : α) (v : α → A ⊕ Fin n) : (canonHostF L₁ Tag dim B x).Realize v ↔ canonPart ρ (v x)

theorem DescriptiveComplexity.realize_newDom_inl {L₁ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} {A : Type} [L₁.Structure A] [Nonempty A] {n : ℕ} {ρ : (newBlock Tag dim B).Assignment (A ⊕ Fin n)} (t : Tag) (w : Fin (dim + 1) → A ⊕ Fin n) : (newDom L₁ Tag dim B (Sum.inl t)).Realize w ↔ (∀ (j : Fin dim), IsOld (w j.castSucc)) ∧ canonPart ρ (w (Fin.last dim))

theorem DescriptiveComplexity.realize_newDom_inr {L₁ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} {A : Type} [L₁.Structure A] [Nonempty A] {n : ℕ} {ρ : (newBlock Tag dim B).Assignment (A ⊕ Fin n)} (u : Unit) (w : Fin (dim + 1) → A ⊕ Fin n) : (newDom L₁ Tag dim B (Sum.inr u)).Realize w ↔ ¬IsOld (w (Fin.last dim)) ∧ ∀ (j : Fin dim), w j.castSucc = w (Fin.last dim)

theorem DescriptiveComplexity.realize_canonGuard {L₁ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} {A : Type} [L₁.Structure A] [Nonempty A] {n : ℕ} {ρ : (newBlock Tag dim B).Assignment (A ⊕ Fin n)} : (A ⊕ Fin n) ⊨ canonGuard L₁ Tag dim B ↔ ∃! c : A ⊕ Fin n, canonPart ρ c

theorem DescriptiveComplexity.realize_newRelF_base {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} {A : Type} [L₁.Structure A] [Nonempty A] {n : ℕ} {ρ : (newBlock Tag dim B).Assignment (A ⊕ Fin n)} (I : FOInterpretation L₁ L₂ Tag dim) {k : ℕ} (R : L₂.Relations k) (t : Fin k → Tag) (a : Fin k → Fin dim → A) (w : Fin k × Fin (dim + 1) → A ⊕ Fin n) (hw : ∀ (i : Fin k) (j : Fin dim), w (i, j.castSucc) = Sum.inl (a i j)) : (newRelF L₁ Tag dim B I (tgtBaseSym L₂ B R) fun (i : Fin k) => Sum.inl (t i)).Realize w ↔ (I.relFormula R t).Realize fun (p : Fin k × Fin dim) => a p.1 p.2

A base symbol at a tuple of interpreted tags: the reduction's own defining formula, read among the original elements.

theorem DescriptiveComplexity.newRelF_base_eq_bot {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} (I : FOInterpretation L₁ L₂ Tag dim) {k : ℕ} (R : L₂.Relations k) (τ : Fin k → Tag ⊕ Unit) (h : ¬∃ (t : Fin k → Tag), ∀ (i : Fin k), τ i = Sum.inl (t i)) : newRelF L₁ Tag dim B I (tgtBaseSym L₂ B R) τ = ⊥

A base symbol never holds of an invented point.

theorem DescriptiveComplexity.realize_newRelF_old {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} {A : Type} [L₁.Structure A] [Nonempty A] {n : ℕ} {ρ : (newBlock Tag dim B).Assignment (A ⊕ Fin n)} (I : FOInterpretation L₁ L₂ Tag dim) (τ : Fin 1 → Tag ⊕ Unit) (w : Fin 1 × Fin (dim + 1) → A ⊕ Fin n) : (newRelF L₁ Tag dim B I (tgtOldSym L₂ B) τ).Realize w ↔ (τ 0).isLeft = true

The marker old holds exactly of the interpreted points.

theorem DescriptiveComplexity.realize_newRelF_block {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} {A : Type} [L₁.Structure A] [Nonempty A] {n : ℕ} {ρ : (newBlock Tag dim B).Assignment (A ⊕ Fin n)} (I : FOInterpretation L₁ L₂ Tag dim) {k : ℕ} (r : B.lang.Relations k) (τ : Fin k → Tag ⊕ Unit) (w : Fin k × Fin (dim + 1) → A ⊕ Fin n) : (newRelF L₁ Tag dim B I (tgtBlockSym L₂ B r) τ).Realize w ↔ pullPart ρ ⟨↑r, fun (j : Fin (B.arity ↑r)) => τ (Fin.cast ⋯ j)⟩ fun (mm : Fin ((SOBlock.pull (Tag ⊕ Unit) (dim + 1) B).arity ⟨↑r, fun (j : Fin (B.arity ↑r)) => τ (Fin.cast ⋯ j)⟩)) => w (Fin.cast ⋯ (finProdFinEquiv.symm mm).1, (finProdFinEquiv.symm mm).2)

A relation variable of the target's block is read off the pulled variable selected by the tags.

The interpreted universe is the target's extended universe

def DescriptiveComplexity.newPoint {L₁ L₂ : FirstOrder.Language} {Tag : Type} {dim : ℕ} {A : Type} {n : ℕ} (I : FOInterpretation L₁ L₂ Tag dim) (c₀ : A ⊕ Fin n) : I.Map A ⊕ Fin n → (Tag ⊕ Unit) × (Fin (dim + 1) → A ⊕ Fin n)

The tagged tuple representing a point of the target's extended universe: an interpreted point becomes its tag together with its coordinates, the spare coordinate pinned to c₀; an invented value becomes a diagonal tuple.

Equations

• DescriptiveComplexity.newPoint I c₀ (Sum.inl p) = (Sum.inl p.1, Fin.snoc (fun (j : Fin dim) => Sum.inl (p.2 j)) c₀)
• DescriptiveComplexity.newPoint I c₀ (Sum.inr i) = (Sum.inr (), fun (x : Fin (dim + 1)) => Sum.inr i)

@[simp]

theorem DescriptiveComplexity.newPoint_inl {L₁ L₂ : FirstOrder.Language} {Tag : Type} {dim : ℕ} {A : Type} {n : ℕ} (I : FOInterpretation L₁ L₂ Tag dim) (c₀ : A ⊕ Fin n) (p : I.Map A) : newPoint I c₀ (Sum.inl p) = (Sum.inl p.1, Fin.snoc (fun (j : Fin dim) => Sum.inl (p.2 j)) c₀)

@[simp]

theorem DescriptiveComplexity.newPoint_inr {L₁ L₂ : FirstOrder.Language} {Tag : Type} {dim : ℕ} {A : Type} {n : ℕ} (I : FOInterpretation L₁ L₂ Tag dim) (c₀ : A ⊕ Fin n) (i : Fin n) : newPoint I c₀ (Sum.inr i) = (Sum.inr (), fun (x : Fin (dim + 1)) => Sum.inr i)

theorem DescriptiveComplexity.newPoint_injective {L₁ L₂ : FirstOrder.Language} {Tag : Type} {dim : ℕ} {A : Type} {n : ℕ} (I : FOInterpretation L₁ L₂ Tag dim) (c₀ : A ⊕ Fin n) : Function.Injective (newPoint I c₀)

theorem DescriptiveComplexity.newPoint_mem_dom {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} {A : Type} [L₁.Structure A] [Nonempty A] {n : ℕ} {I : FOInterpretation L₁ L₂ Tag dim} {c₀ : A ⊕ Fin n} (ρ : (newBlock Tag dim B).Assignment (A ⊕ Fin n)) (hc₀ : canonPart ρ c₀) (x : I.Map A ⊕ Fin n) : (newDom L₁ Tag dim B (newPoint I c₀ x).1).Realize (newPoint I c₀ x).2

theorem DescriptiveComplexity.newPoint_surjective {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} {A : Type} [L₁.Structure A] [Nonempty A] {n : ℕ} {I : FOInterpretation L₁ L₂ Tag dim} {c₀ : A ⊕ Fin n} (ρ : (newBlock Tag dim B).Assignment (A ⊕ Fin n)) (hc : ∀ (y : A ⊕ Fin n), canonPart ρ y ↔ y = c₀) (z : (Tag ⊕ Unit) × (Fin (dim + 1) → A ⊕ Fin n)) (hz : (newDom L₁ Tag dim B z.1).Realize z.2) : ∃ (x : I.Map A ⊕ Fin n), newPoint I c₀ x = z

Every point of the interpreted universe is the image of a point of the target's extended universe: an interpreted tag carries a tuple of original elements, an invented tag a single invented value.

theorem DescriptiveComplexity.isLeft_newPoint {L₁ L₂ : FirstOrder.Language} {Tag : Type} {dim : ℕ} {A : Type} {n : ℕ} {I : FOInterpretation L₁ L₂ Tag dim} {c₀ : A ⊕ Fin n} (x : I.Map A ⊕ Fin n) : (newPoint I c₀ x).1.isLeft = true ↔ IsOld x

Transfer of the kernel

def DescriptiveComplexity.targetAssign {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} {A : Type} {n : ℕ} (I : FOInterpretation L₁ L₂ Tag dim) (c₀ : A ⊕ Fin n) (ρ : (newBlock Tag dim B).Assignment (A ⊕ Fin n)) : B.Assignment (I.Map A ⊕ Fin n)

The assignment of the target's block on the target's extended universe, read off a guessed assignment on the source's: the pulled variable selected by the tags of the arguments, at their coordinates.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.newTargetEquiv {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] [Nonempty Tag] {dim : ℕ} {B : SOBlock} {A : Type} [L₁.Structure A] [Nonempty A] {n : ℕ} (I : FOInterpretation L₁ L₂ Tag dim) (c₀ : A ⊕ Fin n) (ρ : (newBlock Tag dim B).Assignment (A ⊕ Fin n)) (hc : ∀ (y : A ⊕ Fin n), canonPart ρ y ↔ y = c₀) : (newTarget L₂ B).Equiv (I.Map A ⊕ Fin n) ((newInterp L₁ Tag dim B I).MapRel (A ⊕ Fin n))

The interpreted structure is the target's extended structure: the map sending a point of I.Map A ⊕ Fin n to its tagged tuple is an isomorphism over the target's extended vocabulary, the target's block being interpreted by DescriptiveComplexity.targetAssign.

Equations

• DescriptiveComplexity.newTargetEquiv I c₀ ρ hc = { toEquiv := Equiv.ofBijective (fun (x : I.Map A ⊕ Fin n) => ⟨DescriptiveComplexity.newPoint I c₀ x, ⋯⟩) ⋯, map_fun' := ⋯, map_rel' := ⋯ }

theorem DescriptiveComplexity.realize_transfer {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] [Nonempty Tag] {dim : ℕ} {B : SOBlock} {A : Type} [L₁.Structure A] [Nonempty A] {n : ℕ} (I : FOInterpretation L₁ L₂ Tag dim) (c₀ : A ⊕ Fin n) (ρ : (newBlock Tag dim B).Assignment (A ⊕ Fin n)) (hc : ∀ (y : A ⊕ Fin n), canonPart ρ y ↔ y = c₀) (ρT : B.Assignment (I.Map A ⊕ Fin n)) (hT : targetAssign I c₀ ρ = ρT) (φ : (newTarget L₂ B).Sentence) : (I.Map A ⊕ Fin n) ⊨ φ ↔ (newInterp L₁ Tag dim B I).MapRel (A ⊕ Fin n) ⊨ φ

Sentence transfer: what the target's kernel says in the target's extended universe, it says in the interpreted universe.

The guarded pullback of a sentence

noncomputable def DescriptiveComplexity.RelFOInterpretation.pullRelSentence {L₃ L₄ : FirstOrder.Language} {TagJ : Type} {dJ : ℕ} (J : RelFOInterpretation L₃ L₄ TagJ dJ) [L₄.IsRelational] [Finite TagJ] (φ : L₄.Sentence) : L₃.Sentence

The guarded pullback of a sentence through a relativized interpretation: an L₃-sentence that holds in A exactly when the original sentence holds in the definable universe J.MapRel A (the relativized counterpart of DescriptiveComplexity.FOInterpretation.pullSentence).

Equations

• J.pullRelSentence φ = FirstOrder.Language.Formula.relabel (fun (p : (Empty ⊕ Fin 0) × Fin dJ) => isEmptyElim p.1) (J.pullRel φ fun (a : Empty ⊕ Fin 0) => isEmptyElim a)

theorem DescriptiveComplexity.RelFOInterpretation.realize_pullRelSentence {L₃ L₄ : FirstOrder.Language} {TagJ : Type} {dJ : ℕ} (J : RelFOInterpretation L₃ L₄ TagJ dJ) [L₄.IsRelational] [Finite TagJ] (φ : L₄.Sentence) (A : Type) [L₃.Structure A] : A ⊨ J.pullRelSentence φ ↔ J.MapRel A ⊨ φ

Reproducing an assignment of the target's block

def DescriptiveComplexity.sourceAssign {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} {A : Type} {n : ℕ} (I : FOInterpretation L₁ L₂ Tag dim) (c₀ : A ⊕ Fin n) (ρT : B.Assignment (I.Map A ⊕ Fin n)) : (SOBlock.pull (Tag ⊕ Unit) (dim + 1) B).Assignment (A ⊕ Fin n)

The pulled-block assignment reproducing a given assignment of the target's block: a pulled variable holds of a tuple exactly when that tuple is the image of a tuple of the target's universe that the assignment relates.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.targetAssign_sourceAssign {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dim : ℕ} {B : SOBlock} {A : Type} {n : ℕ} (I : FOInterpretation L₁ L₂ Tag dim) (c₀ : A ⊕ Fin n) (ρT : B.Assignment (I.Map A ⊕ Fin n)) : targetAssign I c₀ (joinParts (fun (z : Fin 1 → A ⊕ Fin n) => z 0 = c₀) (sourceAssign I c₀ ρT)) = ρT

Reading the reproduced assignment back gives the original one: the two transfers compose to the identity in the direction a definable universe allows.

The closure theorem

theorem DescriptiveComplexity.sorealize_newPull {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] [Nonempty Tag] {dim : ℕ} (I : FOInterpretation L₁ L₂ Tag dim) (B : SOBlock) (φ : (newTarget L₂ B).Sentence) (A : Type) [L₁.Structure A] [Nonempty A] (n : ℕ) : SORealize (newLang L₂) (I.Map A ⊕ Fin n) [B] φ true ↔ SORealize (newLang L₁) (A ⊕ Fin n) [newBlock Tag dim B] (canonGuard L₁ Tag dim B ⊓ (newInterp L₁ Tag dim B I).pullRelSentence φ) true

Definability in ∃SO[new] transfers through an interpretation: with the same number of invented values, the target's kernel holds in the target's extended universe exactly when its guarded pullback holds in the source's.

theorem DescriptiveComplexity.SigmaSONewDefinable.of_foReduction {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : FOReduction P Q) (h : SigmaSONewDefinable Q) : SigmaSONewDefinable P

∃SO[new]-definability is closed under first-order reductions, the closure that makes RE a complexity class: the target's extended universe is interpreted inside the source's, with the same invented values, and the kernel is pulled back through that interpretation.