Finite quantifier blocks for Lω₁ω formulas

Finite blocks of existential and universal quantifiers over the last k bound variables, with their realization semantics in Fin.append form.

Main Definitions

• FirstOrder.Language.BoundedFormulaω.existsBlock: quantify the last k bound variables existentially, by iterating ex.
• FirstOrder.Language.BoundedFormulaω.forallBlock: the universal analogue, iterating all.

Main Results

• realize_existsBlock: (existsBlock φ).Realize v xs ↔ ∃ ys : Fin k → M, φ.Realize v (Fin.append xs ys) — the first n coordinates remain the ambient bound environment and the last k coordinates are the block's witnesses.
• realize_forallBlock: the universal analogue.

Implementation Notes

The environment in the realization lemmas is the plain Fin.append xs ys (well-typed since Fin (n + k) is the formula's bound-variable index); the successor step is the standard Fin.snoc (Fin.append xs ys) y = Fin.append xs (Fin.snoc ys y) exchange. This is reusable syntax infrastructure independent of any particular application.

def FirstOrder.Language.BoundedFormulaω.existsBlock {L : Language} {α : Type u'} {n k : ℕ} : L.BoundedFormulaω α (n + k) → L.BoundedFormulaω α n

Existentially quantify the last k bound variables of a formula, by iterating ex.

Equations

• φ.existsBlock = φ
• φ.existsBlock = φ.ex.existsBlock

def FirstOrder.Language.BoundedFormulaω.forallBlock {L : Language} {α : Type u'} {n k : ℕ} : L.BoundedFormulaω α (n + k) → L.BoundedFormulaω α n

Universally quantify the last k bound variables of a formula, by iterating all.

Equations

• φ.forallBlock = φ
• φ.forallBlock = φ.all.forallBlock

theorem FirstOrder.Language.BoundedFormulaω.realize_existsBlock {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} {k : ℕ} (φ : L.BoundedFormulaω α (n + k)) : φ.existsBlock.Realize v xs ↔ ∃ (ys : Fin k → M), φ.Realize v (Fin.append xs ys)

Realization of a finite existential block: witnesses for the last k bound variables, in Fin.append form.

theorem FirstOrder.Language.BoundedFormulaω.realize_forallBlock {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} {k : ℕ} (φ : L.BoundedFormulaω α (n + k)) : φ.forallBlock.Realize v xs ↔ ∀ (ys : Fin k → M), φ.Realize v (Fin.append xs ys)

Realization of a finite universal block: all values of the last k bound variables, in Fin.append form.