Pulling a simultaneous induction through a relativized interpretation

The transport lemmas of DescriptiveComplexity.FixedPointStep, redone for interpretations with a definable domain (DescriptiveComplexity.RelFOInterpretation) – and with them, closure of membership under relativized ordered reductions ≤ʳᶠᵒ[≤] (DescriptiveComplexity.IFPDefinable.of_relOrderedReduction, DescriptiveComplexity.PFPDefinable.of_relOrderedReduction).

Why the fixed-point logics need it when the second-order ones did not: all the library's hardness travels along relativized reductions (they are what a spanning target problem requires), so bringing a problem of a class back from a complete problem – PSPACE ⊆ FO(≤, PFP) via the machine problem in DescriptiveComplexity.FixedPointPartialMachine – crosses a relativized reduction in the membership direction. For the second-order classes membership was always a direct sentence, and the crossing never happened.

The construction

Everything mirrors the plain pullback (DescriptiveComplexity.StepDef.pull), with the domain threaded through:

• the interpretation extends along a block with its domain unchanged (DescriptiveComplexity.RelFOInterpretation.extendSORel);
• an assignment of the block on the definable universe transfers to an assignment of the pulled block that holds only in-domain tuples (DescriptiveComplexity.SOBlock.pullAssignRel) – the transfer is injective (DescriptiveComplexity.SOBlock.pullAssignRel_injective), which is what carries fixed-point-ness back and forth for a deterministic iteration, where the existential-only transfer of DescriptiveComplexity.SecondOrderNewPull would not suffice;
• the step formula of a pulled variable is the guarded pullback of the original step (DescriptiveComplexity.guardPullRel, from DescriptiveComplexity.RelFOInterpretation.pullRel) gated by the domain formulas of its arguments (DescriptiveComplexity.domGateF), so that off-domain tuples are never derived and the stages stay in the image of the transfer;
• one application of the pulled step is the transfer of one application of the original (DescriptiveComplexity.StepDef.next_pullRel), whence the stages, limits, and values correspond (DescriptiveComplexity.StepDef.ifpHolds_pullRel, DescriptiveComplexity.StepDef.pfpHolds_pullRel).

Extending a relativized interpretation along a block

def DescriptiveComplexity.RelFOInterpretation.extendSORel {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dm : ℕ} (I : RelFOInterpretation L₁ L₂ Tag dm) (B : SOBlock) : RelFOInterpretation (L₁.sum (SOBlock.pull Tag dm B).lang) (L₂.sum B.lang) Tag dm

Extension of a relativized interpretation along a second-order quantifier block: the underlying interpretation extends as DescriptiveComplexity.FOInterpretation.extendSO, and the domain formula is unchanged (lifted to the expanded source vocabulary, which it does not use).

Equations

• I.extendSORel B = { toFOInterpretation := I.extendSO B, domFormula := fun (t : Tag) => FirstOrder.Language.LHom.sumInl.onFormula (I.domFormula t) }

Transferring assignments

def DescriptiveComplexity.SOBlock.pullAssignRel {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dm : ℕ} (B : SOBlock) (I : RelFOInterpretation L₁ L₂ Tag dm) {A : Type} [L₁.Structure A] (ρ : B.Assignment (I.MapRel A)) : (pull Tag dm B).Assignment A

Transfer of an assignment on the definable universe to an assignment of the pulled block: a pulled tuple is in the transferred relation when all its argument points lie in the domain and the packed tuple is in the original relation. Off-domain tuples are never held – which keeps the transfer injective.

Equations

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

theorem DescriptiveComplexity.SOBlock.pullAssignRel_iff {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dm : ℕ} (B : SOBlock) (I : RelFOInterpretation L₁ L₂ Tag dm) {A : Type} [L₁.Structure A] (ρ : B.Assignment (I.MapRel A)) {i : B.ι} {τ : Fin (B.arity i) → Tag} {x : Fin (B.arity i * dm) → A} (y : Fin (B.arity i) → I.MapRel A) (hy : ∀ (k : Fin (B.arity i)), ↑(y k) = (τ k, fun (j : Fin dm) => x (finProdFinEquiv (k, j)))) : B.pullAssignRel I ρ ⟨i, τ⟩ x ↔ ρ i y

The workhorse characterization of the transfer: reading it at a tuple of points whose components are known is reading the original assignment at those points.

theorem DescriptiveComplexity.SOBlock.pullAssignRel_botAssign {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dm : ℕ} (B : SOBlock) (I : RelFOInterpretation L₁ L₂ Tag dm) {A : Type} [L₁.Structure A] : B.pullAssignRel I (B.botAssign (I.MapRel A)) = (pull Tag dm B).botAssign A

Transferring the empty assignment gives the empty assignment.

theorem DescriptiveComplexity.SOBlock.pullAssignRel_injective {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dm : ℕ} (B : SOBlock) (I : RelFOInterpretation L₁ L₂ Tag dm) {A : Type} [L₁.Structure A] : Function.Injective (B.pullAssignRel I)

The transfer of assignments to the definable universe is injective: the original assignment is read back off the transferred one at the packed tuples.

The gated pullback of the step formulas

noncomputable def DescriptiveComplexity.domGateF {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dm : ℕ} (I : RelFOInterpretation L₁ L₂ Tag dm) (B : SOBlock) (p : (SOBlock.pull Tag dm B).ι) : (L₁.sum (SOBlock.pull Tag dm B).lang).Formula (Fin (B.arity p.fst * dm))

The domain gate of a pulled variable: all its argument points lie in the definable domain.

Equations

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

theorem DescriptiveComplexity.realize_domGateF {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dm : ℕ} (I : RelFOInterpretation L₁ L₂ Tag dm) (B : SOBlock) (p : (SOBlock.pull Tag dm B).ι) {A : Type} [L₁.Structure A] (σ : (SOBlock.pull Tag dm B).Assignment A) (x : Fin (B.arity p.fst * dm) → A) : (domGateF I B p).Realize x ↔ ∀ (k : Fin (B.arity p.fst)), (I.domFormula (p.snd k)).Realize fun (j : Fin dm) => x (finProdFinEquiv (k, j))

noncomputable def DescriptiveComplexity.guardPullRel {Tag : Type} [Finite Tag] {dm : ℕ} {L₃ L₄ : FirstOrder.Language} [L₄.IsRelational] (J : RelFOInterpretation L₃ L₄ Tag dm) {k : ℕ} (φ : L₄.Formula (Fin k)) (t : Fin k → Tag) : L₃.Formula (Fin (k * dm))

The guarded pullback of a formula on k free variables, at a static tag assignment: the relativized sibling of DescriptiveComplexity.guardPull.

Equations

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

theorem DescriptiveComplexity.realize_guardPullRel {Tag : Type} [Finite Tag] {dm : ℕ} {L₃ L₄ : FirstOrder.Language} [L₄.IsRelational] (J : RelFOInterpretation L₃ L₄ Tag dm) {A : Type} [L₃.Structure A] {k : ℕ} (φ : L₄.Formula (Fin k)) (t : Fin k → Tag) (w : Fin (k * dm) → A) (hw : ∀ (q : Fin k), (J.domFormula (t q)).Realize fun (j : Fin dm) => w (finProdFinEquiv (q, j))) : (guardPullRel J φ t).Realize w ↔ φ.Realize fun (q : Fin k) => ⟨(t q, fun (j : Fin dm) => w (finProdFinEquiv (q, j))), ⋯⟩

The extended structure equivalence

theorem DescriptiveComplexity.realize_extendSORel_domFormula {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dm : ℕ} (I : RelFOInterpretation L₁ L₂ Tag dm) (B : SOBlock) {A : Type} [L₁.Structure A] (σ : (SOBlock.pull Tag dm B).Assignment A) (t : Tag) (w : Fin dm → A) : ((I.extendSORel B).domFormula t).Realize w ↔ (I.domFormula t).Realize w

The domain formula of the extended relativized interpretation means the original domain formula.

noncomputable def DescriptiveComplexity.extendSORelPointEquiv {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dm : ℕ} (I : RelFOInterpretation L₁ L₂ Tag dm) (B : SOBlock) (A : Type) [L₁.Structure A] (σ : (SOBlock.pull Tag dm B).Assignment A) : (I.extendSORel B).MapRel A ≃ I.MapRel A

Points of the extended relativized universe are points of the original one: the two subtypes are cut out by equivalent conditions.

Equations

• DescriptiveComplexity.extendSORelPointEquiv I B A σ = (Equiv.refl (Tag × (Fin dm → A))).subtypeEquiv ⋯

noncomputable def DescriptiveComplexity.RelFOInterpretation.extendSORelEquiv {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dm : ℕ} (I : RelFOInterpretation L₁ L₂ Tag dm) (B : SOBlock) (A : Type) [L₁.Structure A] (ρ : B.Assignment (I.MapRel A)) : (L₂.sum B.lang).Equiv ((I.extendSORel B).MapRel A) (I.MapRel A)

Interpreting through the extended relativized interpretation agrees with expanding the definable universe by the block: repackaging the points is an isomorphism over the expanded target language, the block being read through the transfer on one side and directly on the other (the relativized sibling of DescriptiveComplexity.FOInterpretation.extendSOEquiv).

Equations

• I.extendSORelEquiv B A ρ = { toEquiv := DescriptiveComplexity.extendSORelPointEquiv I B A (B.pullAssignRel I ρ), map_fun' := ⋯, map_rel' := ⋯ }

The pulled induction and its stages

noncomputable def DescriptiveComplexity.StepDef.pullRel {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dm : ℕ} (dd : StepDef L₂) (I : RelFOInterpretation L₁ L₂ Tag dm) : StepDef L₁

The pullback of a simultaneous induction through a relativized interpretation: the block is pulled back variable by variable, the step formula of a pulled variable is the guarded pullback of the original step gated by the domain formulas of its arguments, and the output is the guarded pullback of the original output.

Equations

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

theorem DescriptiveComplexity.StepDef.next_pullRel {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dm : ℕ} (dd : StepDef L₂) (I : RelFOInterpretation L₁ L₂ Tag dm) {A : Type} [L₁.Structure A] (ρ : dd.B.Assignment (I.MapRel A)) : (dd.pullRel I).next (dd.B.pullAssignRel I ρ) = dd.B.pullAssignRel I (dd.next ρ)

One application of the pulled step formulas is the transfer of one application of the original ones.

theorem DescriptiveComplexity.StepDef.partStage_pullRel {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dm : ℕ} (dd : StepDef L₂) (I : RelFOInterpretation L₁ L₂ Tag dm) {A : Type} [L₁.Structure A] (n : ℕ) : (dd.pullRel I).partStage A n = dd.B.pullAssignRel I (dd.partStage (I.MapRel A) n)

The partial stages of the relativized pullback are the transfers of the original stages.

theorem DescriptiveComplexity.StepDef.inflStep_pullRel {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dm : ℕ} (dd : StepDef L₂) (I : RelFOInterpretation L₁ L₂ Tag dm) {A : Type} [L₁.Structure A] (ρ : dd.B.Assignment (I.MapRel A)) : (dd.pullRel I).inflStep (dd.B.pullAssignRel I ρ) = dd.B.pullAssignRel I (dd.inflStep ρ)

The inflationary step commutes with the transfer.

theorem DescriptiveComplexity.StepDef.inflStage_pullRel {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dm : ℕ} (dd : StepDef L₂) (I : RelFOInterpretation L₁ L₂ Tag dm) {A : Type} [L₁.Structure A] (n : ℕ) : (dd.pullRel I).inflStage A n = dd.B.pullAssignRel I (dd.inflStage (I.MapRel A) n)

The inflationary stages of the relativized pullback are the transfers of the original stages.

theorem DescriptiveComplexity.StepDef.inflLimit_pullRel {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dm : ℕ} (dd : StepDef L₂) (I : RelFOInterpretation L₁ L₂ Tag dm) {A : Type} [L₁.Structure A] : (dd.pullRel I).inflLimit A = dd.B.pullAssignRel I (dd.inflLimit (I.MapRel A))

The value of the pulled inflationary iteration is the transfer of the original value.

theorem DescriptiveComplexity.StepDef.isFixedPt_next_pullRel_iff {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dm : ℕ} (dd : StepDef L₂) (I : RelFOInterpretation L₁ L₂ Tag dm) {A : Type} [L₁.Structure A] (ρ : dd.B.Assignment (I.MapRel A)) : Function.IsFixedPt (dd.pullRel I).next (dd.B.pullAssignRel I ρ) ↔ Function.IsFixedPt dd.next ρ

Being a fixed point of the step is insensitive to the transfer.

theorem DescriptiveComplexity.StepDef.ifpHolds_pullRel {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dm : ℕ} (dd : StepDef L₂) (I : RelFOInterpretation L₁ L₂ Tag dm) {A : Type} [L₁.Structure A] : (dd.pullRel I).IFPHolds A ↔ dd.IFPHolds (I.MapRel A)

The value of the pulled inflationary definition is the value of the original one on the definable universe.

theorem DescriptiveComplexity.StepDef.pfpHolds_pullRel {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dm : ℕ} (dd : StepDef L₂) (I : RelFOInterpretation L₁ L₂ Tag dm) {A : Type} [L₁.Structure A] : (dd.pullRel I).PFPHolds A ↔ dd.PFPHolds (I.MapRel A)

The value of the pulled partial definition is the value of the original one on the definable universe.

Closure under relativized ordered reductions

theorem DescriptiveComplexity.IFPDefinable.of_relOrderedReduction {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] [L₁.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : RelOrderedFOReduction P Q) (h : IFPDefinable Q) : IFPDefinable P

FO(≤, IFP) definability is closed under relativized ordered reductions: the induction pulls back through the order-extended relativized interpretation, whose universe – the definable domain with the restricted lexicographic order – is identified with the ordered domain by DescriptiveComplexity.RelFOInterpretation.ordExtendRelLEquiv.

theorem DescriptiveComplexity.PFPDefinable.of_relOrderedReduction {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] [L₁.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : RelOrderedFOReduction P Q) (h : PFPDefinable Q) : PFPDefinable P

FO(≤, PFP) definability is closed under relativized ordered reductions.