Guessing what the invented values mean

To read a problem over an exponential expansion as one with value invention, the invented values have to be the expansion's points, and a point is an assignment of a block: a relation over the instance. So the sentence guesses a meaning relation M, one more argument than the relation it names: M v x⃗ says that the invented value v names a relation holding of x⃗.

Three of the four conditions on that guess are ordinary first-order statements about the extended universe:

• DescriptiveComplexity.meanShaped – M relates an invented value to original elements and nothing else;
• DescriptiveComplexity.meanInj – distinct invented values name distinct relations;
• DescriptiveComplexity.meanEmpty – some invented value names the empty relation.

The fourth is what buys the one thing a sentence cannot say, that the guess is onto:

• DescriptiveComplexity.meanFlip – for every invented value and every tuple, some invented value names the same relation with that tuple flipped.

With injectivity, those last two make the meanings enumerate every relation, by DescriptiveComplexity.bijective_of_flipClosedP – a counting argument in Lean, not a condition in the logic. That is where the bound of an exponentially-bounded invention is spent.

The block and its atoms

@[reducible, inline]

abbrev DescriptiveComplexity.meanBlock (a : ℕ) : SOBlock

The block guessing the meanings: one relation of arity one more than the relation being named.

Equations

• DescriptiveComplexity.meanBlock a = { ι := Unit, ιFinite := ⋯, arity := fun (x : Unit) => a + 1 }

def DescriptiveComplexity.meanSym (a : ℕ) : (meanBlock a).lang.Relations (a + 1)

The meaning relation, as a symbol.

Equations

• DescriptiveComplexity.meanSym a = ⟨(), ⋯⟩

@[reducible, inline]

abbrev DescriptiveComplexity.meanHost (L : FirstOrder.Language) (a : ℕ) : FirstOrder.Language

The vocabulary a meaning guess is written in.

Equations

• DescriptiveComplexity.meanHost L a = (DescriptiveComplexity.newLang L).sum (DescriptiveComplexity.meanBlock a).lang

noncomputable def DescriptiveComplexity.oldAtomM (L : FirstOrder.Language) (a : ℕ) {α : Type} (x : α) : (meanHost L a).Formula α

The atom old x.

Equations

• DescriptiveComplexity.oldAtomM L a x = FirstOrder.Language.Relations.formula (Sum.inl (Sum.inr FirstOrder.Language.oldSym)) fun (x_1 : Fin 1) => FirstOrder.Language.var x

noncomputable def DescriptiveComplexity.meanAtom (L : FirstOrder.Language) (a : ℕ) {α : Type} (v : α) (w : Fin a → α) : (meanHost L a).Formula α

The atom M v x⃗: the invented value v names a relation holding of x⃗.

Equations

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

The four guards

noncomputable def DescriptiveComplexity.meanShaped (L : FirstOrder.Language) (a : ℕ) : (meanHost L a).Sentence

The meaning relation is shaped: it relates an invented value to original elements, and nothing else.

Equations

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

noncomputable def DescriptiveComplexity.meanEmpty (L : FirstOrder.Language) (a : ℕ) : (meanHost L a).Sentence

Some invented value names the empty relation.

Equations

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

noncomputable def DescriptiveComplexity.meanInj (L : FirstOrder.Language) (a : ℕ) : (meanHost L a).Sentence

Distinct invented values name distinct relations.

Equations

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

noncomputable def DescriptiveComplexity.meanFlip (L : FirstOrder.Language) (a : ℕ) : (meanHost L a).Sentence

The meanings are closed under flipping one tuple: for every invented value and every tuple of original elements, some invented value names the same relation with that tuple flipped. This is what makes the guess onto.

Equations

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

noncomputable def DescriptiveComplexity.meanGuard (L : FirstOrder.Language) (a : ℕ) : (meanHost L a).Sentence

The whole guard: the four conditions together.

Equations

• DescriptiveComplexity.meanGuard L a = DescriptiveComplexity.meanShaped L a ⊓ DescriptiveComplexity.meanEmpty L a ⊓ DescriptiveComplexity.meanInj L a ⊓ DescriptiveComplexity.meanFlip L a

The guards, realized

def DescriptiveComplexity.meaningOf {a : ℕ} {A : Type} {m : ℕ} (ρ : (meanBlock a).Assignment (A ⊕ Fin m)) : A ⊕ Fin m → (Fin a → A ⊕ Fin m) → Prop

The relation an element names, read off the guess.

Equations

• DescriptiveComplexity.meaningOf ρ v w = ρ () fun (i : Fin (a + 1)) => Fin.cases v w i

def DescriptiveComplexity.meanAt {a : ℕ} {A : Type} {m : ℕ} (ρ : (meanBlock a).Assignment (A ⊕ Fin m)) (i : Fin m) : (Fin a → A) → Prop

The relation an invented value names, at original arguments.

Equations

• DescriptiveComplexity.meanAt ρ i w = DescriptiveComplexity.meaningOf ρ (Sum.inr i) fun (j : Fin a) => Sum.inl (w j)

@[instance_reducible]

noncomputable def DescriptiveComplexity.meanStruc {L : FirstOrder.Language} [L.IsRelational] {a : ℕ} {A : Type} [L.Structure A] {m : ℕ} (ρ : (meanBlock a).Assignment (A ⊕ Fin m)) : (meanHost L a).Structure (A ⊕ Fin m)

The host structure: the extended structure expanded by the guess.

Equations

• DescriptiveComplexity.meanStruc ρ = (DescriptiveComplexity.newLang L).sumStructure (DescriptiveComplexity.meanBlock a).lang (A ⊕ Fin m)

theorem DescriptiveComplexity.realize_oldAtomM {L : FirstOrder.Language} [L.IsRelational] {a : ℕ} {A : Type} [L.Structure A] {m : ℕ} (ρ : (meanBlock a).Assignment (A ⊕ Fin m)) {α : Type} (x : α) (v : α → A ⊕ Fin m) : (oldAtomM L a x).Realize v ↔ IsOld (v x)

theorem DescriptiveComplexity.realize_meanAtom {L : FirstOrder.Language} [L.IsRelational] {a : ℕ} {A : Type} [L.Structure A] {m : ℕ} (ρ : (meanBlock a).Assignment (A ⊕ Fin m)) {α : Type} (x : α) (w : Fin a → α) (v : α → A ⊕ Fin m) : (meanAtom L a x w).Realize v ↔ meaningOf ρ (v x) fun (i : Fin a) => v (w i)

theorem DescriptiveComplexity.realize_meanShaped {L : FirstOrder.Language} [L.IsRelational] {a : ℕ} {A : Type} [L.Structure A] {m : ℕ} (ρ : (meanBlock a).Assignment (A ⊕ Fin m)) : (A ⊕ Fin m) ⊨ meanShaped L a ↔ ∀ (v : A ⊕ Fin m) (w : Fin a → A ⊕ Fin m), meaningOf ρ v w → ¬IsOld v ∧ ∀ (i : Fin a), IsOld (w i)

theorem DescriptiveComplexity.realize_meanEmpty {L : FirstOrder.Language} [L.IsRelational] {a : ℕ} {A : Type} [L.Structure A] {m : ℕ} (ρ : (meanBlock a).Assignment (A ⊕ Fin m)) : (A ⊕ Fin m) ⊨ meanEmpty L a ↔ ∃ (v : A ⊕ Fin m), ¬IsOld v ∧ ∀ (w : Fin a → A ⊕ Fin m), ¬meaningOf ρ v w

theorem DescriptiveComplexity.realize_meanInj {L : FirstOrder.Language} [L.IsRelational] {a : ℕ} {A : Type} [L.Structure A] {m : ℕ} (ρ : (meanBlock a).Assignment (A ⊕ Fin m)) : (A ⊕ Fin m) ⊨ meanInj L a ↔ ∀ (v u : A ⊕ Fin m), ¬IsOld v → ¬IsOld u → (∀ (w : Fin a → A ⊕ Fin m), meaningOf ρ v w ↔ meaningOf ρ u w) → v = u

theorem DescriptiveComplexity.realize_meanFlip {L : FirstOrder.Language} [L.IsRelational] {a : ℕ} {A : Type} [L.Structure A] {m : ℕ} (ρ : (meanBlock a).Assignment (A ⊕ Fin m)) : (A ⊕ Fin m) ⊨ meanFlip L a ↔ ∀ (v : A ⊕ Fin m) (y : Fin a → A ⊕ Fin m), ¬IsOld v → (∀ (i : Fin a), IsOld (y i)) → ∃ (u : A ⊕ Fin m), ¬IsOld u ∧ ∀ (w : Fin a → A ⊕ Fin m), meaningOf ρ u w ↔ (meaningOf ρ v w ↔ ¬∀ (i : Fin a), w i = y i)

theorem DescriptiveComplexity.xor_iff_iff_not (p q : Prop) : Xor p q ↔ (p ↔ ¬q)

theorem DescriptiveComplexity.bijective_meanAt {a : ℕ} {A : Type} {m : ℕ} (ρ : (meanBlock a).Assignment (A ⊕ Fin m)) [Finite A] (hshaped : ∀ (v : A ⊕ Fin m) (w : Fin a → A ⊕ Fin m), meaningOf ρ v w → ¬IsOld v ∧ ∀ (i : Fin a), IsOld (w i)) (hempty : ∃ (v : A ⊕ Fin m), ¬IsOld v ∧ ∀ (w : Fin a → A ⊕ Fin m), ¬meaningOf ρ v w) (hinj : ∀ (v u : A ⊕ Fin m), ¬IsOld v → ¬IsOld u → (∀ (w : Fin a → A ⊕ Fin m), meaningOf ρ v w ↔ meaningOf ρ u w) → v = u) (hflip : ∀ (v : A ⊕ Fin m) (y : Fin a → A ⊕ Fin m), ¬IsOld v → (∀ (i : Fin a), IsOld (y i)) → ∃ (u : A ⊕ Fin m), ¬IsOld u ∧ ∀ (w : Fin a → A ⊕ Fin m), meaningOf ρ u w ↔ (meaningOf ρ v w ↔ ¬∀ (i : Fin a), w i = y i)) : Function.Bijective (meanAt ρ)

The guard makes the meanings a bijection: with the four conditions, the invented values name every a-ary relation of the instance, each exactly once. This is where the counting of DescriptiveComplexity.SecondOrderNewCount is spent.

theorem DescriptiveComplexity.bijective_meanAt_of_guard {L : FirstOrder.Language} [L.IsRelational] {a : ℕ} {A : Type} [L.Structure A] {m : ℕ} (ρ : (meanBlock a).Assignment (A ⊕ Fin m)) [Finite A] : (A ⊕ Fin m) ⊨ meanGuard L a → Function.Bijective (meanAt ρ)

The whole guard, realized, and what it buys: the invented values name every a-ary relation of the instance, each exactly once.