Finite connectives and quantifier blocks

Finite conjunctions and disjunctions express tag choices in an interpretation. Quantifier blocks replace a quantifier over tuples by quantification over each coordinate. envBlock σ v puts the coordinates of v first, followed by σ. These constructions include empty blocks and empty families.

def Complexity.DescriptiveComplexity.envBlock {card n : ℕ} (σ : Env card n) {k : ℕ} : Env card k → Env card (n + k)

Extend an environment by an entire tuple, placing its first coordinate at index zero.

Equations

• Complexity.DescriptiveComplexity.envBlock σ x_2 = σ
• Complexity.DescriptiveComplexity.envBlock σ v = Complexity.DescriptiveComplexity.envCons (v 0) (Complexity.DescriptiveComplexity.envBlock σ (Fin.tail v))

theorem Complexity.DescriptiveComplexity.envBlock_new {card n k : ℕ} (σ : Env card n) (v : Env card k) (i : Fin k) : envBlock σ v ⟨↑i, ⋯⟩ = v i

The new variables evaluate to the corresponding tuple coordinates.

def Complexity.DescriptiveComplexity.Term.shiftBy {V : Vocabulary} {n : ℕ} (t : Term V n) (k : ℕ) : Term V (n + k)

Shift a term across a block of fresh variables.

Equations

• t.shiftBy 0 = t
• t.shiftBy k.succ = (t.shiftBy k).shift

theorem Complexity.DescriptiveComplexity.Term.shiftBy_eval {V : Vocabulary} {n k : ℕ} (A : FinStruct V) (σ : Env A.card n) (v : Env A.card k) (t : Term V n) : eval A (envBlock σ v) (t.shiftBy k) = eval A σ t

Old terms retain their value when moved across a block of quantifiers.

def Complexity.DescriptiveComplexity.Formula.existBlock {V : Vocabulary} {n : ℕ} (k : ℕ) : Formula V (n + k) → Formula V n

Existentially bind a block of the first k variables.

Equations

• Complexity.DescriptiveComplexity.Formula.existBlock 0 φ = φ
• Complexity.DescriptiveComplexity.Formula.existBlock k.succ φ = Complexity.DescriptiveComplexity.Formula.existBlock k φ.exist

def Complexity.DescriptiveComplexity.Formula.allBlock {V : Vocabulary} {n : ℕ} (k : ℕ) : Formula V (n + k) → Formula V n

Universally bind a block of the first k variables.

Equations

• Complexity.DescriptiveComplexity.Formula.allBlock 0 φ = φ
• Complexity.DescriptiveComplexity.Formula.allBlock k.succ φ = Complexity.DescriptiveComplexity.Formula.allBlock k φ.all

theorem Complexity.DescriptiveComplexity.Formula.existBlock_sat {V : Vocabulary} {n k : ℕ} (A : FinStruct V) (σ : Env A.card n) (φ : Formula V (n + k)) : Sat A σ (existBlock k φ) ↔ ∃ (v : Env A.card k), Sat A (envBlock σ v) φ

Existential block quantification is quantification over all coordinate tuples.

theorem Complexity.DescriptiveComplexity.Formula.allBlock_sat {V : Vocabulary} {n k : ℕ} (A : FinStruct V) (σ : Env A.card n) (φ : Formula V (n + k)) : Sat A σ (allBlock k φ) ↔ ∀ (v : Env A.card k), Sat A (envBlock σ v) φ

Universal block quantification is quantification over all coordinate tuples.

def Complexity.DescriptiveComplexity.Formula.conjList {V : Vocabulary} {n : ℕ} (xs : List (Formula V n)) : Formula V n

A finite conjunction, with verum as the empty conjunction.

Equations

• Complexity.DescriptiveComplexity.Formula.conjList xs = List.foldr Complexity.DescriptiveComplexity.Formula.conj Complexity.DescriptiveComplexity.Formula.verum xs

def Complexity.DescriptiveComplexity.Formula.disjList {V : Vocabulary} {n : ℕ} (xs : List (Formula V n)) : Formula V n

A finite disjunction, with falsum as the empty disjunction.

Equations

• Complexity.DescriptiveComplexity.Formula.disjList xs = List.foldr Complexity.DescriptiveComplexity.Formula.disj Complexity.DescriptiveComplexity.Formula.falsum xs

theorem Complexity.DescriptiveComplexity.Formula.conjList_sat {V : Vocabulary} {n : ℕ} (A : FinStruct V) (σ : Env A.card n) (xs : List (Formula V n)) : Sat A σ (conjList xs) ↔ ∀ (φ : Formula V n), φ ∈ xs → Sat A σ φ

A finite conjunction holds exactly when every member holds.

theorem Complexity.DescriptiveComplexity.Formula.disjList_sat {V : Vocabulary} {n : ℕ} (A : FinStruct V) (σ : Env A.card n) (xs : List (Formula V n)) : Sat A σ (disjList xs) ↔ ∃ (φ : Formula V n), φ ∈ xs ∧ Sat A σ φ

A finite disjunction holds exactly when some member holds.

def Complexity.DescriptiveComplexity.Formula.conjFin {V : Vocabulary} {n k : ℕ} (φ : Fin k → Formula V n) : Formula V n

Conjunction over a finite index type.

Equations

• Complexity.DescriptiveComplexity.Formula.conjFin φ = Complexity.DescriptiveComplexity.Formula.conjList (List.map φ (List.finRange k))

def Complexity.DescriptiveComplexity.Formula.disjFin {V : Vocabulary} {n k : ℕ} (φ : Fin k → Formula V n) : Formula V n

Disjunction over a finite index type.

Equations

• Complexity.DescriptiveComplexity.Formula.disjFin φ = Complexity.DescriptiveComplexity.Formula.disjList (List.map φ (List.finRange k))

theorem Complexity.DescriptiveComplexity.Formula.conjFin_sat {V : Vocabulary} {n k : ℕ} (A : FinStruct V) (σ : Env A.card n) (φ : Fin k → Formula V n) : Sat A σ (conjFin φ) ↔ ∀ (i : Fin k), Sat A σ (φ i)

Finite conjunction is universal quantification over its indices.

theorem Complexity.DescriptiveComplexity.Formula.disjFin_sat {V : Vocabulary} {n k : ℕ} (A : FinStruct V) (σ : Env A.card n) (φ : Fin k → Formula V n) : Sat A σ (disjFin φ) ↔ ∃ (i : Fin k), Sat A σ (φ i)

Finite disjunction is existential quantification over its indices.