A quantifier prefix of k copies of one block

The shape every Σₖ definition in this library has: k alternating blocks that are all the same block, one per round of whatever the definition describes — one truth assignment per quantifier block for DescriptiveComplexity.QBF, one run per round of the game for the machine bridge of the polynomial hierarchy.

DescriptiveComplexity.SecondOrderMerge collapses a prefix into a single block, at the cost of turning the alternation into DescriptiveComplexity.altAssign, an alternating quantification over the pieces of one merged assignment. That is awkward to use: the pieces are indexed by the shape of the merge rather than by the round. This file removes the awkwardness when all the blocks are equal:

• DescriptiveComplexity.repBlockAssign assembles a merged assignment out of a family Fin k → B.Assignment A, one per round (DescriptiveComplexity.QBF's own repAssign is its monadic special case, and should be folded into it);
• DescriptiveComplexity.repSym names the relation variable of the i-th round, and DescriptiveComplexity.relMap_repSym reads it back;
• DescriptiveComplexity.altBlockQuant is the alternating quantification over such a family, and DescriptiveComplexity.altAssign_repBlocks identifies it with altAssign.

Nothing here is specific to a block: the symbol and the assignment are built by the same recursion on k, so the reading lemma is Iff.rfl at the head and the induction hypothesis at the tail.

The prefix and its merge

@[reducible, inline]

abbrev DescriptiveComplexity.repBlocks (B : SOBlock) (k : ℕ) : List SOBlock

A quantifier prefix of k copies of the block B.

Equations

• DescriptiveComplexity.repBlocks B k = List.replicate k B

@[simp]

theorem DescriptiveComplexity.repBlocks_length (B : SOBlock) (k : ℕ) : (repBlocks B k).length = k

@[reducible, inline]

abbrev DescriptiveComplexity.repMerged (B : SOBlock) (k : ℕ) : SOBlock

The single block merging a prefix of k copies of B.

Equations

• DescriptiveComplexity.repMerged B k = DescriptiveComplexity.mergeBlocks (DescriptiveComplexity.repBlocks B k)

def DescriptiveComplexity.repSym (B : SOBlock) {n : ℕ} (x : B.ι) (h : B.arity x = n) (k : ℕ) : Fin k → (repMerged B k).lang.Relations n

The relation variable of B used by the i-th round, as a symbol of the merged block's vocabulary. The arity proof is carried along the recursion, so that reading the symbol back needs no cast.

Equations

• DescriptiveComplexity.repSym B x h 0 i = i.elim0
• DescriptiveComplexity.repSym B x h n_1.succ ⟨0, isLt⟩ = ⟨Sum.inl x, h⟩
• DescriptiveComplexity.repSym B x h k.succ ⟨j.succ, hj⟩ = ⟨Sum.inr ↑(DescriptiveComplexity.repSym B x h k ⟨j, ⋯⟩), ⋯⟩

def DescriptiveComplexity.repBlockAssign (B : SOBlock) (A : Type) (k : ℕ) : (Fin k → B.Assignment A) → (repMerged B k).Assignment A

The merged assignment determined by one assignment of B per round.

Equations

• DescriptiveComplexity.repBlockAssign B A 0 x_2 = DescriptiveComplexity.nilAssign A
• DescriptiveComplexity.repBlockAssign B A k.succ ρs = DescriptiveComplexity.consAssign (ρs 0) (DescriptiveComplexity.repBlockAssign B A k fun (i : Fin k) => ρs i.succ)

theorem DescriptiveComplexity.relMap_repSym (B : SOBlock) {A : Type} {n : ℕ} (x : B.ι) (h : B.arity x = n) (k : ℕ) (ρs : Fin k → B.Assignment A) (i : Fin k) (v : Fin n → A) : FirstOrder.Language.Structure.RelMap (repSym B x h k i) v ↔ ρs i x fun (j : Fin (B.arity x)) => v (Fin.cast h j)

Reading back the relation variable of a round.

Alternating over the rounds

def DescriptiveComplexity.altBlockQuant (A : Type) (B : SOBlock) (k : ℕ) : ((Fin k → B.Assignment A) → Prop) → Bool → Prop

Alternating quantification over one assignment of B per round: the round of index 0 is quantified outermost, existentially if pol is true, and the polarities alternate inwards.

Equations

• DescriptiveComplexity.altBlockQuant A B 0 P x✝ = P Fin.elim0
• DescriptiveComplexity.altBlockQuant A B k.succ P true = ∃ (ρ : B.Assignment A), DescriptiveComplexity.altBlockQuant A B k (fun (ρs : Fin k → B.Assignment A) => P (Fin.cons ρ ρs)) false
• DescriptiveComplexity.altBlockQuant A B k.succ P false = ∀ (ρ : B.Assignment A), DescriptiveComplexity.altBlockQuant A B k (fun (ρs : Fin k → B.Assignment A) => P (Fin.cons ρ ρs)) true

theorem DescriptiveComplexity.altBlockQuant_congr {A : Type} {B : SOBlock} (k : ℕ) (P Q : (Fin k → B.Assignment A) → Prop) : (∀ (ρs : Fin k → B.Assignment A), P ρs ↔ Q ρs) → ∀ (pol : Bool), altBlockQuant A B k P pol ↔ altBlockQuant A B k Q pol

Alternating quantification over the rounds only depends on the quantified predicate up to pointwise equivalence.

theorem DescriptiveComplexity.altAssign_repBlocks (B : SOBlock) {A : Type} (k : ℕ) (P : (repMerged B k).Assignment A → Prop) (pol : Bool) : altAssign A (repBlocks B k) P pol ↔ altBlockQuant A B k (fun (ρs : Fin k → B.Assignment A) => P (repBlockAssign B A k ρs)) pol

The prefix quantifies one assignment per round: alternating over the pieces of the merged assignment of k copies of B is alternating over k assignments of B.

The definability statement

Put together: a sentence over the single merged block, transported into the iterated expansion by DescriptiveComplexity.unmergeHom, is satisfied alternately exactly when the k round assignments are quantified alternately. This is the form a Σₖ-definability proof consumes.

theorem DescriptiveComplexity.sorealize_repBlocks (B : SOBlock) (L : FirstOrder.Language) (A : Type) (instL : L.Structure A) (k : ℕ) (ψ : (L.sum (repMerged B k).lang).Sentence) (pol : Bool) : SORealize L A (repBlocks B k) ((unmergeHom (repBlocks B k) L).onSentence ψ) pol ↔ altBlockQuant A B k (fun (ρs : Fin k → B.Assignment A) => A ⊨ ψ) pol