An induction cannot separate two k-pebble equivalent structures

DescriptiveComplexity.Invariant.Stages carries ≡ᵏ-invariance through the stages of an inflationary induction inside one structure. The same argument, run against the two-structure game of DescriptiveComplexity.Invariant.TwoPebble, carries it between two structures: stage by stage, the assignments computed on either side agree on k-pebble equivalent tuples (DescriptiveComplexity.StepDef.inflStage_invariant₂), and therefore so do the limits, and therefore the output sentence is true on one structure exactly when it is on the other (DescriptiveComplexity.StepDef.ifpHolds_equivK₂).

That last statement is what separates a Boolean query: a query distinguishing two structures the duplicator can play forever on is not order-free FO(IFP)-definable. Over bare sets, where k pebbles cannot count past k (DescriptiveComplexity.equivK₂_bare), this is the inexpressibility of DescriptiveComplexity.EVEN for order-free inflationary induction – the failure of capture, since parity is decidable in polynomial time.

Jointly invariant assignments

def DescriptiveComplexity.AssignInvariant₂ {L : FirstOrder.Language} (S : Set ((n : ℕ) × L.Relations n)) (M N : Type) [L.Structure M] [L.Structure N] (k : ℕ) {B : SOBlock} (ρ : B.Assignment M) (σ : B.Assignment N) : Prop

A pair of assignments of a block, one on each structure, is jointly ≡ᵏ-invariant when corresponding relations agree on k-pebble equivalent tuples, however their arguments are selected from the k coordinates.

Equations

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

The stages

theorem DescriptiveComplexity.StepDef.next_invariant₂ {L : FirstOrder.Language} {M N : Type} {k : ℕ} {S : Set ((n : ℕ) × L.Relations n)} [L.Structure M] [L.Structure N] [L.IsRelational] [Finite M] [Finite N] (d : StepDef L) (hd : d.VarBound k) (hrels : d.UsesRels S) {ρ : d.B.Assignment M} {σ : d.B.Assignment N} (hρσ : AssignInvariant₂ S M N k ρ σ) : AssignInvariant₂ S M N k (d.next ρ) (d.next σ)

One application of the step formulas preserves joint invariance: the two-structure k-variable invariance lemma, over the structures expanded by the (jointly invariant) current stages.

theorem DescriptiveComplexity.StepDef.inflStage_invariant₂ {L : FirstOrder.Language} {M N : Type} {k : ℕ} {S : Set ((n : ℕ) × L.Relations n)} [L.Structure M] [L.Structure N] [L.IsRelational] [Finite M] [Finite N] (d : StepDef L) (hd : d.VarBound k) (hrels : d.UsesRels S) (n : ℕ) : AssignInvariant₂ S M N k (d.inflStage M n) (d.inflStage N n)

Corresponding stages of the inflationary iteration are jointly invariant.

theorem DescriptiveComplexity.StepDef.ifpHolds_equivK₂ {L : FirstOrder.Language} {M N : Type} {k : ℕ} {S : Set ((n : ℕ) × L.Relations n)} [L.Structure M] [L.Structure N] [L.IsRelational] [Finite M] [Finite N] (d : StepDef L) (hd : d.VarBound k) (hrels : d.UsesRels S) (hout : qdepth d.out ≤ k) {v : Fin k → M} {w : Fin k → N} (hvw : EquivK₂ (atomicAgreeOn₂ S M N k) v w) : d.IFPHolds M ↔ d.IFPHolds N

An order-free inflationary induction cannot separate two structures carrying a k-pebble equivalent pair of tuples, k covering both its variable budget and the quantifier depth of its output sentence. This is the Boolean-query form of ≡ᵏ-invariance, and the one a capture statement needs: the value of the induction is the same on both sides. Registered in the Lax archive as Lax945089.PebbleInvariance.ifpHolds_equivK₂.