A defining formula of an interpretation, with its arguments pinned to rounds

DescriptiveComplexity.ExpExpansion.exists_transl translates a prenex formula over an exponential expansion into a kernel quantified by the rounds that remain above c, the rounds below c holding the values of its free variables. What an interpretation hands over is not that: it is a FirstOrder.Language.Formula (Fin k × Fin dim), one free variable per coordinate of each argument tuple.

This file closes the gap once and for all, for the two-argument case that covers every relation symbol of FirstOrder.Language.andOrGraph (a unary symbol simply ignores the second argument):

DescriptiveComplexity.ExpExpansion.exists_paramKernel – for every φ : (X.E + ≤).Formula (Fin 2 × Fin d) there is a round count D such that, at any layout with at least 2 * d parameter rounds and exactly D play rounds, a kernel K exists whose alternating value over the play rounds is φ, its argument (a, b) read at the round DescriptiveComplexity.ExpExpansion.paramIx a b – that is, at round a * d + b, so that the first argument occupies the rounds below d and the second the rounds below 2 * d.

The bookkeeping is three renamings and nothing else: the free variables become bound slots (FirstOrder.Language.BoundedFormula.relabel), the result is put in prenex form (FirstOrder.Language.BoundedFormula.toPrenex, whose proof is what exists_transl recurses on), and the slots are sent to their rounds by the hv argument of exists_transl.

Where an argument coordinate sits

def DescriptiveComplexity.ExpExpansion.paramIx (d n : ℕ) (h : 2 * d ≤ n) (a : Fin 2) (b : Fin d) : Fin n

Coordinate b of argument a sits at round a * d + b: the first argument's points occupy the rounds below d, the second's the next d.

Equations

• DescriptiveComplexity.ExpExpansion.paramIx d n h a b = ⟨↑a * d + ↑b, ⋯⟩

@[simp]

theorem DescriptiveComplexity.ExpExpansion.paramIx_val (d n : ℕ) (h : 2 * d ≤ n) (a : Fin 2) (b : Fin d) : ↑(paramIx d n h a b) = ↑a * d + ↑b

The formula, with its arguments freed into slots

noncomputable def DescriptiveComplexity.ExpExpansion.argsFreed {L : FirstOrder.Language} (X : ExpExpansion L) {d : ℕ} (φ : (X.E.sum FirstOrder.Language.order).Formula (Fin 2 × Fin d)) : (X.E.sum FirstOrder.Language.order).BoundedFormula Empty (2 * d)

The defining formula of an interpretation, its free variables pushed into bound slots so that DescriptiveComplexity.ExpExpansion.exists_transl can consume it.

Equations

• X.argsFreed φ = (FirstOrder.Language.BoundedFormula.relabel (fun (p : Fin 2 × Fin d) => Sum.inr ⟨↑p.1 * d + ↑p.2, ⋯⟩) φ).toPrenex

theorem DescriptiveComplexity.ExpExpansion.argsFreed_isPrenex {L : FirstOrder.Language} {X : ExpExpansion L} {d : ℕ} (φ : (X.E.sum FirstOrder.Language.order).Formula (Fin 2 × Fin d)) : (X.argsFreed φ).IsPrenex

theorem DescriptiveComplexity.ExpExpansion.realize_argsFreed {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {d : ℕ} (φ : (X.E.sum FirstOrder.Language.order).Formula (Fin 2 × Fin d)) (xs : Fin (2 * d) → X.Map A) : (X.argsFreed φ).Realize default xs ↔ φ.Realize fun (p : Fin 2 × Fin d) => xs ⟨↑p.1 * d + ↑p.2, ⋯⟩

Freeing the arguments changes nothing: read at any tuple of points, the freed formula says what the original said of the points its coordinates name.

The kernel

theorem DescriptiveComplexity.ExpExpansion.exists_paramKernel {L : FirstOrder.Language} (X : ExpExpansion L) {d : ℕ} (φ : (X.E.sum FirstOrder.Language.order).Formula (Fin 2 × Fin d)) : ∃ (D : ℕ), ∀ (n c : ℕ) (_hcn : c + D = n) (_h2d : 2 * d ≤ c), ∃ (K : ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock n).lang).Sentence), ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [inst_2 : Finite A] [inst_3 : Nonempty A] (pts : Fin n → X.Map A) (ext : (Fin D → X.pointBlock.Assignment A) → Fin n → X.pointBlock.Assignment A), (∀ (τs : Fin D → X.pointBlock.Assignment A) (k : Fin n), ↑k < c → ext τs k = pointAssign (pts k)) → (∀ (τs : Fin D → X.pointBlock.Assignment A) (i : Fin D) (k : Fin n), ↑k = c + ↑i → ext τs k = τs i) → (altBlockQuant A X.pointBlock D (fun (τs : Fin D → X.pointBlock.Assignment A) => A ⊨ K) true ↔ φ.Realize fun (p : Fin 2 × Fin d) => pts (paramIx d n ⋯ p.1 p.2))

A defining formula, played as an alternating prefix. The round count D depends on the formula alone; the layout – how many parameter rounds sit below the play rounds – is free, so that finitely many formulas can share one block by padding the short ones.