Relativization of a formula to a unary predicate

Restricting every quantifier of a first-order formula to the elements satisfying a unary relation symbol (DescriptiveComplexity.relativizeTo), so that the formula, read in a structure M, says exactly what it says in the part of M that the symbol marks (DescriptiveComplexity.realize_relativizeTo).

The part must be closed under the function symbols of the language, so that it carries a structure at all; the statement therefore takes the marked part as a FirstOrder.Language.Substructure whose carrier the symbol defines. Marking by a symbol rather than by an arbitrary formula is what the users below need, and keeps the guard a one-line atom.

Where this is used

Value invention (DescriptiveComplexity.SecondOrderNew) puts the instance A and m invented values in one universe A ⊕ Fin m. A formula about A – in particular a defining formula of an interpretation being pulled back – must then be read with its quantifiers restricted to the original elements, which is exactly relativization to the predicate old. The specialization DescriptiveComplexity.relOld and its correctness DescriptiveComplexity.realize_relOld package that instance: the old part of A ⊕ Fin m is a substructure (function symbols return original elements by DescriptiveComplexity.extBase) isomorphic to A (DescriptiveComplexity.oldSubEquiv).

The same machinery is what a relativized membership pullback – the domain-formula item of ROADMAP.md §3 – would want.

Relativization to a unary relation symbol

def DescriptiveComplexity.lastGuard {L : FirstOrder.Language} {α : Type} (R : L.Relations 1) (n : ℕ) : L.BoundedFormula α (n + 1)

The guard “the last bound variable satisfies R”.

Equations

• DescriptiveComplexity.lastGuard R n = R.boundedFormula₁ (FirstOrder.Language.var (Sum.inr (Fin.last n)))

def DescriptiveComplexity.relativizeTo {L : FirstOrder.Language} {α : Type} (R : L.Relations 1) {n : ℕ} : L.BoundedFormula α n → L.BoundedFormula α n

Relativization: the formula obtained by restricting every quantifier to the elements satisfying the unary relation symbol R. Atoms are left untouched, so this is a purely syntactic guard insertion.

Equations

• DescriptiveComplexity.relativizeTo R FirstOrder.Language.BoundedFormula.falsum = FirstOrder.Language.BoundedFormula.falsum
• DescriptiveComplexity.relativizeTo R (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = FirstOrder.Language.BoundedFormula.equal t₁ t₂
• DescriptiveComplexity.relativizeTo R (FirstOrder.Language.BoundedFormula.rel r ts) = FirstOrder.Language.BoundedFormula.rel r ts
• DescriptiveComplexity.relativizeTo R (φ.imp ψ) = (DescriptiveComplexity.relativizeTo R φ).imp (DescriptiveComplexity.relativizeTo R ψ)
• DescriptiveComplexity.relativizeTo R φ.all = ((DescriptiveComplexity.lastGuard R x✝).imp (DescriptiveComplexity.relativizeTo R φ)).all

theorem DescriptiveComplexity.relativizeTo_of_isQF {L : FirstOrder.Language} {α : Type} {R : L.Relations 1} {n : ℕ} {φ : L.BoundedFormula α n} (h : φ.IsQF) : relativizeTo R φ = φ

Guards are inserted at quantifiers only, so relativization is the identity on a quantifier-free formula. Not a simp lemma: simp has no way to discharge the IsQF side condition on its own, so it would only ever fire when passed the hypothesis explicitly.

theorem DescriptiveComplexity.realize_lastGuard {L : FirstOrder.Language} {α M : Type} [L.Structure M] {R : L.Relations 1} {n : ℕ} (v : α → M) (xs : Fin (n + 1) → M) : (lastGuard R n).Realize v xs ↔ FirstOrder.Language.Structure.RelMap R ![xs (Fin.last n)]

theorem DescriptiveComplexity.realize_relativizeTo {L : FirstOrder.Language} {α M : Type} [L.Structure M] {R : L.Relations 1} (S : L.Substructure M) (hS : ∀ (x : M), x ∈ S ↔ FirstOrder.Language.Structure.RelMap R ![x]) {n : ℕ} (φ : L.BoundedFormula α n) (v : α → ↥S) (xs : Fin n → ↥S) : ((relativizeTo R φ).Realize (fun (a : α) => ↑(v a)) fun (i : Fin n) => ↑(xs i)) ↔ φ.Realize v xs

Relativization is correct: the relativized formula, read in M at arguments taken from the substructure the symbol R defines, says what the original formula says in that substructure.

Relativization to the original elements of an extended universe

def DescriptiveComplexity.oldSub (L : FirstOrder.Language) (A : Type) [L.Structure A] [Nonempty A] (m : ℕ) : (newLang L).Substructure (A ⊕ Fin m)

The original elements of the extended universe form a substructure: by DescriptiveComplexity.extBase, function symbols take their values among the original elements.

Equations

• DescriptiveComplexity.oldSub L A m = { carrier := {x : A ⊕ Fin m | DescriptiveComplexity.IsOld x}, fun_mem := ⋯ }

theorem DescriptiveComplexity.mem_oldSub_iff (L : FirstOrder.Language) (A : Type) [L.Structure A] [Nonempty A] (m : ℕ) (x : A ⊕ Fin m) : x ∈ oldSub L A m ↔ IsOld x

noncomputable def DescriptiveComplexity.oldSubEquiv (L : FirstOrder.Language) (A : Type) [L.Structure A] [Nonempty A] (m : ℕ) : (newLang L).Equiv (↥(oldSub L A m)) A

The substructure of original elements is the instance itself, over the extended vocabulary (where every element is marked as original).

Equations

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

def DescriptiveComplexity.relOld {L : FirstOrder.Language} {γ : Type} (φ : L.Formula γ) : (newLang L).Formula γ

The relativization of an L-formula to the original elements of an extended universe: an L-formula becomes a formula over the extended vocabulary, with every quantifier restricted to the elements marked old.

Equations

• DescriptiveComplexity.relOld φ = DescriptiveComplexity.relativizeTo (Sum.inr FirstOrder.Language.oldSym) (FirstOrder.Language.LHom.sumInl.onFormula φ)

theorem DescriptiveComplexity.realize_relOld {L : FirstOrder.Language} {A : Type} [L.Structure A] [Nonempty A] {m : ℕ} {γ : Type} (φ : L.Formula γ) (v : γ → A) : ((relOld φ).Realize fun (g : γ) => Sum.inl (v g)) ↔ φ.Realize v

Relativizing to the original elements is correct: read in the extended universe at original arguments, the relativized formula says what the original formula says in the instance.