The translation lemma

A first-order sentence over an exponential expansion is a second-order sentence over the base. This is the type-lowering reading of Henkin 1950 made into a theorem, and the honest statement of the obstruction that keeps an interpretation from being composed after an expansion: a quantifier ranging over the points of X.Map A ranges over block assignments, so it is a second-order quantifier over A. The translation writes that down rather than avoiding it.

The construction is the standard one, with everything it needs already built.

• Prenex first. FirstOrder.Language.BoundedFormula.toPrenex puts the sentence in prenex form, so the quantifiers can be peeled from the outside. The recursion runs on the FirstOrder.Language.BoundedFormula.IsPrenex proof, not on the formula: ∃ is encoded as ∼(∼φ).all, which no structural recursion can match, while IsPrenex carries all and ex as genuine constructors.
• One quantifier, two rounds. DescriptiveComplexity.SORealize alternates strictly, while a prenex prefix has runs of the same quantifier. Each quantifier therefore takes two rounds – one ∃, one ∀ – of which one is real and the other vacuous. Every round is guarded to hold a point (DescriptiveComplexity.ExpExpansion.stepF), so a vacuous round is discharged by DescriptiveComplexity.ExpExpansion.mapNonempty rather than by a syntactic independence argument, and the matrix may read every round.
• The rounds are addressed absolutely. The matrix mentions the outermost quantifiers, so a round is named by its index in the merged block rather than relative to the quantifier being peeled. Peeling then instantiates the outer rounds one at a time, which is what the ext parameter of DescriptiveComplexity.ExpExpansion.exists_transl tracks: it places the rounds that remain at their absolute positions and fills the positions below with the points already chosen.

The sentence is produced existentially, not by a total recursive definition. That is what keeps the round arithmetic honest: the inequalities saying that the rounds a subformula needs exist are in scope exactly where the Fin-indices are built, so no fallback round and no cast is needed anywhere. The number of rounds is likewise produced by the induction (the d of DescriptiveComplexity.ExpExpansion.exists_transl) instead of by a second recursion counting quantifiers.

The kernel, read at an arbitrary family of rounds

@[instance_reducible]

noncomputable def DescriptiveComplexity.ExpExpansion.roundStructure {L : FirstOrder.Language} (X : ExpExpansion L) {n : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (ρs : Fin n → X.pointBlock.Assignment A) : ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock n).lang).Structure A

The structure the kernel of the translation is realized against: the base, expanded by one copy of the point block per round. It is DescriptiveComplexity.ExpExpansion.prefixStructure with the rounds allowed to hold assignments not (yet) known to be points.

Equations

• X.roundStructure ρs = (DescriptiveComplexity.repMerged X.pointBlock n).structure₁ (DescriptiveComplexity.repBlockAssign X.pointBlock A n ρs)

Freeing the bound variables of the matrix

theorem DescriptiveComplexity.ExpExpansion.isQF_toFormula {L' : FirstOrder.Language} {α : Type} {k : ℕ} {ψ : L'.BoundedFormula α k} (hψ : ψ.IsQF) : FirstOrder.Language.BoundedFormula.IsQF ψ.toFormula

Turning the bound variables of a quantifier-free formula into free ones keeps it quantifier-free.

noncomputable def DescriptiveComplexity.ExpExpansion.matrixF {L : FirstOrder.Language} (X : ExpExpansion L) {n j : ℕ} (hv : Fin j → Fin n) (ψ : (X.E.sum FirstOrder.Language.order).BoundedFormula Empty j) : ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock n).lang).Sentence

The matrix of the prefix: the quantifier-free matrix of a prenex sentence, its bound variables freed and each sent to the round holding its point.

Equations

• X.matrixF hv ψ = X.translQF n finZeroElim (FirstOrder.Language.Formula.relabel (Sum.elim Empty.elim hv) ψ.toFormula)

theorem DescriptiveComplexity.ExpExpansion.realize_matrixF {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {n j : ℕ} (pts : Fin n → X.Map A) (hv : Fin j → Fin n) {ψ : (X.E.sum FirstOrder.Language.order).BoundedFormula Empty j} (hqf : ψ.IsQF) : A ⊨ X.matrixF hv ψ ↔ ψ.Realize default fun (i : Fin j) => pts (hv i)

The matrix says what it should: read against the rounds, it holds exactly when the formula holds of the points they carry.

One quantifier, two rounds

noncomputable def DescriptiveComplexity.ExpExpansion.stepF {L : FirstOrder.Language} (X : ExpExpansion L) {n : ℕ} (i₀ i₁ : Fin n) (K : ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock n).lang).Sentence) : ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock n).lang).Sentence

The kernel contributed by one quantifier: its two rounds, each guarded to hold a point – the first existentially, as a conjunct, the second universally, as a hypothesis.

Equations

• X.stepF i₀ i₁ K = X.roundPointGuardF n i₀ ⊓ FirstOrder.Language.BoundedFormula.imp (X.roundPointGuardF n i₁) K

theorem DescriptiveComplexity.ExpExpansion.altBlockQuant_peel_step {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] {n r : ℕ} (i₀ i₁ : Fin n) (K : ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock n).lang).Sentence) (ext : (Fin (r + 2) → X.pointBlock.Assignment A) → Fin n → X.pointBlock.Assignment A) (h₀ : ∀ (τs : Fin (r + 2) → X.pointBlock.Assignment A), ext τs i₀ = τs 0) (h₁ : ∀ (τs : Fin (r + 2) → X.pointBlock.Assignment A), ext τs i₁ = τs (Fin.succ 0)) : altBlockQuant A X.pointBlock (r + 2) (fun (τs : Fin (r + 2) → X.pointBlock.Assignment A) => A ⊨ X.stepF i₀ i₁ K) true ↔ ∃ (p : X.Map A), ∀ (q : X.Map A), altBlockQuant A X.pointBlock r (fun (τs : Fin r → X.pointBlock.Assignment A) => A ⊨ K) true

Peeling a quantifier: its two rounds become a point chosen existentially and a point chosen universally, of which the kernel that remains uses one.

theorem DescriptiveComplexity.ExpExpansion.transl_step {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {n j c d : ℕ} (hc0 : c < n) (hc1 : c + 1 < n) {hv : Fin j → Fin n} (hlt : ∀ (i : Fin j), ↑(hv i) < c) (iv : Fin n) {K : ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock n).lang).Sentence} {ψ : (X.E.sum FirstOrder.Language.order).BoundedFormula Empty (j + 1)} (hK : ∀ (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 + 2 → ext τs k = pointAssign (pts k)) → (∀ (τs : Fin d → X.pointBlock.Assignment A) (i : Fin d) (k : Fin n), ↑k = c + 2 + ↑i → ext τs k = τs i) → (altBlockQuant A X.pointBlock d (fun (τs : Fin d → X.pointBlock.Assignment A) => A ⊨ K) true ↔ ψ.Realize default fun (i : Fin (j + 1)) => pts (Fin.snoc hv iv i))) (pts : Fin n → X.Map A) (ext : (Fin (d + 2) → X.pointBlock.Assignment A) → Fin n → X.pointBlock.Assignment A) (hfix : ∀ (τs : Fin (d + 2) → X.pointBlock.Assignment A) (k : Fin n), ↑k < c → ext τs k = pointAssign (pts k)) (hemb : ∀ (τs : Fin (d + 2) → X.pointBlock.Assignment A) (i : Fin (d + 2)) (k : Fin n), ↑k = c + ↑i → ext τs k = τs i) (p q : X.Map A) : altBlockQuant A X.pointBlock d (fun (τs : Fin d → X.pointBlock.Assignment A) => A ⊨ K) true ↔ ψ.Realize default (Fin.snoc (fun (i : Fin j) => pts (hv i)) (Function.update (Function.update pts ⟨c, hc0⟩ p) ⟨c + 1, hc1⟩ q iv))

The bookkeeping shared by the two quantifier cases: once the two rounds of a quantifier have been peeled into the points p and q, the induction hypothesis applies at the round c + 2, its variables read at the family of points updated at those two rounds.

The translation

theorem DescriptiveComplexity.ExpExpansion.exists_transl {L : FirstOrder.Language} {X : ExpExpansion L} {j : ℕ} {ψ : (X.E.sum FirstOrder.Language.order).BoundedFormula Empty j} (hψ : ψ.IsPrenex) : ∃ (d : ℕ), ∀ (n c r : ℕ), c + r = n → r = d → ∀ (hv : Fin j → Fin n), (∀ (i : Fin j), ↑(hv i) < 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 r → X.pointBlock.Assignment A) → Fin n → X.pointBlock.Assignment A), (∀ (τs : Fin r → X.pointBlock.Assignment A) (k : Fin n), ↑k < c → ext τs k = pointAssign (pts k)) → (∀ (τs : Fin r → X.pointBlock.Assignment A) (i : Fin r) (k : Fin n), ↑k = c + ↑i → ext τs k = τs i) → (altBlockQuant A X.pointBlock r (fun (τs : Fin r → X.pointBlock.Assignment A) => A ⊨ K) true ↔ ψ.Realize default fun (i : Fin j) => pts (hv i))

The translation lemma, by induction on the prenex proof. A prenex formula with j bound variables, each already held by a round below c, is translated into a sentence of the prefix quantified by the r rounds that remain: d rounds are needed, two per quantifier.

theorem DescriptiveComplexity.ExpExpansion.exists_translate {L : FirstOrder.Language} (X : ExpExpansion L) (φ : (X.E.sum FirstOrder.Language.order).Sentence) : ∃ (Bs : List SOBlock) (ψ : (soLang (L.sum FirstOrder.Language.order) Bs).Sentence) (pol : Bool), ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [inst_2 : Finite A] [inst_3 : Nonempty A], X.Map A ⊨ φ ↔ SORealize (L.sum FirstOrder.Language.order) A Bs ψ pol

An FO sentence over an expansion is a second-order sentence over the base. The obstruction the exponential classes are built around, stated rather than avoided: the quantifiers of a sentence read on the expanded universe become second-order quantifier blocks over the base, two blocks per quantifier.