Guessing a point of an expanded universe

The translation lemma (DescriptiveComplexity.ExpExpansion.exists_translate) – an FO sentence over an expansion is a second-order sentence over the base – peels one quantifier at a time into one second-order block. What that block has to hold is a point of the expanded universe: a tag together with an assignment of the expansion's block.

The assignment half is what a block quantifier already ranges over. The tag half is the problem: everywhere else in this development a tag is static, chosen at formula-construction time (relSentence is indexed by a tuple of tags, ordSentence compares two of them by trichotomy). A quantified point chooses its tag at evaluation time, so the tag has to become part of the guessed object.

The encoding: extend the block by one arity-0 relation variable per tag (DescriptiveComplexity.SOBlock.withTag). An arity-0 variable is a bit – the same observation DescriptiveComplexity.PSpace's docstring makes about finite control in an SO(TC) walk – so a tag is a bit vector, and DescriptiveComplexity.SOBlock.tagGuardF is the sentence saying exactly one bit is set. Its correctness (DescriptiveComplexity.SOBlock.realize_tagGuardF) says the guard holds of an assignment exactly when that assignment is a tagged assignment, which is the form the peeling step consumes.

Nothing here depends on the expansion, only on a block and a finite tag type.

noncomputable def DescriptiveComplexity.finEnum (T : Type) [Finite T] : List T

An enumeration of a finite type, as a list. (SOBlock.ivars is this list at a block's index type; fold the two together when the translation lands.)

Equations

• DescriptiveComplexity.finEnum T = Finset.univ.toList

theorem DescriptiveComplexity.mem_finEnum {T : Type} [Finite T] (t : T) : t ∈ finEnum T

The block extended by tag bits

@[reducible, inline]

abbrev DescriptiveComplexity.SOBlock.withTag (B : SOBlock) (T : Type) [Finite T] : SOBlock

A block extended with one arity-0 relation variable per tag. An arity-0 variable is a bit, so an assignment of this block is an assignment of B together with a bit vector naming a tag.

An abbrev deliberately: with a semireducible def in between, instance search cannot see that the arity of a tag variable is 0, and Fin 0 → A stops being recognized as a subsingleton.

Equations

• B.withTag T = { ι := T ⊕ B.ι, ιFinite := ⋯, arity := Sum.elim (fun (x : T) => 0) B.arity }

def DescriptiveComplexity.SOBlock.tagAssign {B : SOBlock} {T : Type} [Finite T] {A : Type} (t : T) (ρ : B.Assignment A) : (B.withTag T).Assignment A

The assignment of the extended block carrying a given tag and a given assignment: the bit of t' says t' = t.

Equations

• DescriptiveComplexity.SOBlock.tagAssign t ρ (Sum.inl t') = fun (x : Fin ((B.withTag T).arity (Sum.inl t')) → A) => t' = t
• DescriptiveComplexity.SOBlock.tagAssign t ρ (Sum.inr j) = ρ j

instance DescriptiveComplexity.SOBlock.instIsEmptyTagArity {B : SOBlock} {T : Type} [Finite T] {t : T} : IsEmpty (Fin ((B.withTag T).arity (Sum.inl t)))

A tag variable has arity 0, so its argument tuple is the empty one. Stated as an instance because Fin ((B.withTag T).arity (Sum.inl t)) is not syntactically Fin 0, and the Subsingleton/Inhabited facts the correctness proof needs are found through it.

def DescriptiveComplexity.SOBlock.dropTag {B : SOBlock} {T : Type} [Finite T] {A : Type} (σ : (B.withTag T).Assignment A) : B.Assignment A

The assignment an extended assignment carries, forgetting the tag bits.

Equations

• DescriptiveComplexity.SOBlock.dropTag σ j = σ (Sum.inr j)

@[simp]

theorem DescriptiveComplexity.SOBlock.dropTag_tagAssign {B : SOBlock} {T : Type} [Finite T] {A : Type} (t : T) (ρ : B.Assignment A) : dropTag (tagAssign t ρ) = ρ

The exactly-one guard

noncomputable def DescriptiveComplexity.SOBlock.tagBitF {L : FirstOrder.Language} (B : SOBlock) (T : Type) [Finite T] (t : T) : (L.sum (B.withTag T).lang).Formula Empty

The atom “the bit of the tag t is set”.

Equations

• B.tagBitF T t = FirstOrder.Language.Relations.formula (Sum.inr ⟨Sum.inl t, ⋯⟩) Fin.elim0

noncomputable def DescriptiveComplexity.SOBlock.tagGuardF {L : FirstOrder.Language} (B : SOBlock) (T : Type) [Finite T] : (L.sum (B.withTag T).lang).Sentence

Exactly one tag bit is set: the sentence saying that an assignment of the extended block names a tag.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.SOBlock.realize_tagBitF {L : FirstOrder.Language} {B : SOBlock} {T : Type} [Finite T] {A : Type} [L.Structure A] (σ : (B.withTag T).Assignment A) (t : T) : (B.tagBitF T t).Realize default ↔ σ (Sum.inl t) default

theorem DescriptiveComplexity.SOBlock.realize_tagGuardF {L : FirstOrder.Language} {B : SOBlock} {T : Type} [Finite T] {A : Type} [L.Structure A] (σ : (B.withTag T).Assignment A) : A ⊨ B.tagGuardF T ↔ ∃ (t : T) (ρ : B.Assignment A), σ = tagAssign t ρ

The guard says the assignment is a tagged one.