Existential second-order logic with value invention

The logic ∃SO[new] defining the class RE of recursively enumerable problems: existential second-order logic whose relation variables range over a universe extended by finitely many invented values, in the style of the object-creating query languages of ([Abiteboul–Hull–Vianu 1995] [AHV95], ch. 18).

Every class defined so far in this library bounds its certificate by the instance: a Σ₁ sentence guesses relations over A itself, so the search space is exponential in |A| and the class sits inside NP. Value invention removes exactly that bound and nothing else: the certificate is a finite extension A ⊕ Fin m of the universe – with m unbounded – together with relations over it, checked by a fixed first-order kernel. The witness is still a finite object and the kernel is still decidable on a finite structure, so the yes-instances are those found by an unbounded search over finite witnesses: this is a logical definition of recursive enumerability, with no machine model. (The converse inclusion, RE ⊆ ∃SO[new], is the Trakhtenbrot-style encoding of an accepting run into invented values; it lives with the machine bridge, not here.)

The extended structure

An instance A and a number m of invented values determine an extended structure over the vocabulary DescriptiveComplexity.newLang L, the base vocabulary L together with one unary predicate old:

• its universe is A ⊕ Fin m;
• the symbols of L hold exactly where they hold in A, on original elements only – invented values are related to nothing (DescriptiveComplexity.extBase);
• old marks the original elements (DescriptiveComplexity.IsOld).

A vocabulary with function symbols additionally needs a value on invented arguments; DescriptiveComplexity.oldPart reads them as an arbitrary original element. Every vocabulary in this library is relational, where the convention is invisible; it is only there so that ∃SO[new]-definability is defined for every L, as the membership predicate of a DescriptiveComplexity.ComplexityClass must be.

Main definitions and results

• DescriptiveComplexity.SigmaSONewDefinable: definability by an ∃SO[new] sentence – one existential second-order block over the extended universe and a first-order kernel, reusing the alternation machinery of DescriptiveComplexity.SecondOrder at a one-block list;
• DescriptiveComplexity.extEquiv: extended structures are functorial in the base isomorphism, so ∃SO[new] expresses isomorphism-invariant properties;
• DescriptiveComplexity.sigmaSONewDefinable_congr: definability depends only on the finite instances of a problem;
• DescriptiveComplexity.SigmaSODefinable.toNew: Σ₁ ⊆ ∃SO[new], by inventing nothing – the kernel is guarded by DescriptiveComplexity.noNewSentence, “every element is original”, which pins the number of invented values to zero. As a statement about classes this is DescriptiveComplexity.NP_subset_RE.

No alternation hierarchy is built on top of ∃SO[new], deliberately: alternating second-order blocks over a finite extended universe are still checked by an unbounded search over finite witnesses, so the levels would collapse into RE rather than stack. (That collapse is a semantic remark, not a theorem here: proving it inside the logic needs the same encoding as the inclusion RE ⊆ ∃SO[new].)

inductive FirstOrder.Language.oldRel : ℕ → Type

Relation symbols of the language marking the original elements inside an extended universe.

• old : oldRel 1

  old x: the element x comes from the original structure, i.e. it is not an invented value.

def FirstOrder.Language.instDecidableEqOldRel.decEq {a✝ : ℕ} (x✝ x✝¹ : oldRel a✝) : Decidable (x✝ = x✝¹)

Equations

• FirstOrder.Language.instDecidableEqOldRel.decEq FirstOrder.Language.oldRel.old FirstOrder.Language.oldRel.old = isTrue FirstOrder.Language.instDecidableEqOldRel.decEq._proof_1

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqOldRel {a✝ : ℕ} : DecidableEq (oldRel a✝)

Equations

• FirstOrder.Language.instDecidableEqOldRel = FirstOrder.Language.instDecidableEqOldRel.decEq

def FirstOrder.Language.oldMark : Language

The one-symbol relational language marking, inside a universe extended with invented values, the elements of the original structure.

Equations

• FirstOrder.Language.oldMark = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.oldRel }

instance FirstOrder.Language.instIsRelationalOldMark : Language.oldMark.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.oldSym : Language.oldMark.Relations 1

The symbol marking the original elements.

Equations

• FirstOrder.Language.oldSym = FirstOrder.Language.oldRel.old

@[reducible, inline]

abbrev DescriptiveComplexity.newLang (L : FirstOrder.Language) : FirstOrder.Language

The vocabulary of extended structures: the base vocabulary together with the unary predicate old marking the elements of the original structure.

Equations

• DescriptiveComplexity.newLang L = L.sum FirstOrder.Language.oldMark

The extended universe

def DescriptiveComplexity.IsOld {A : Type} {m : ℕ} : A ⊕ Fin m → Prop

The original elements of a universe extended by invented values.

Equations

• DescriptiveComplexity.IsOld (Sum.inl val) = True
• DescriptiveComplexity.IsOld (Sum.inr val) = False

noncomputable def DescriptiveComplexity.oldPart (A : Type) [Nonempty A] (m : ℕ) : A ⊕ Fin m → A

The original-element part of an element of the extended universe, reading an invented value as an arbitrary original element. It only serves to give function symbols an interpretation on invented arguments; every vocabulary in this library is relational, where the choice is invisible.

Equations

• DescriptiveComplexity.oldPart A m = Sum.elim id fun (x : Fin m) => Classical.arbitrary A

@[instance_reducible]

noncomputable def DescriptiveComplexity.extBase (L : FirstOrder.Language) (A : Type) [L.Structure A] [Nonempty A] (m : ℕ) : L.Structure (A ⊕ Fin m)

The base structure carried by the extended universe: a relation symbol holds of a tuple exactly when all its entries are original elements and it holds of them in A. Invented values are related to nothing.

Equations

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

@[instance_reducible]

def DescriptiveComplexity.oldMarkStructure (A : Type) (m : ℕ) : FirstOrder.Language.oldMark.Structure (A ⊕ Fin m)

The interpretation of the marking predicate on the extended universe.

Equations

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

@[instance_reducible]

noncomputable instance DescriptiveComplexity.extStructure (L : FirstOrder.Language) (A : Type) [L.Structure A] [Nonempty A] (m : ℕ) : (newLang L).Structure (A ⊕ Fin m)

The extended structure: the instance A together with m invented values, over the vocabulary DescriptiveComplexity.newLang L.

Equations

• DescriptiveComplexity.extStructure L A m = L.sumStructure FirstOrder.Language.oldMark (A ⊕ Fin m)

@[simp]

theorem DescriptiveComplexity.isOld_inl {A : Type} {m : ℕ} (a : A) : IsOld (Sum.inl a)

@[simp]

theorem DescriptiveComplexity.not_isOld_inr {A : Type} {m : ℕ} (i : Fin m) : ¬IsOld (Sum.inr i)

theorem DescriptiveComplexity.isOld_iff {A : Type} {m : ℕ} {x : A ⊕ Fin m} : IsOld x ↔ ∃ (a : A), x = Sum.inl a

@[simp]

theorem DescriptiveComplexity.oldPart_inl {A : Type} {m : ℕ} [Nonempty A] (a : A) : oldPart A m (Sum.inl a) = a

theorem DescriptiveComplexity.relMap_ext_iff {L : FirstOrder.Language} {A : Type} {m : ℕ} [L.Structure A] [Nonempty A] {k : ℕ} (r : L.Relations k) (x : Fin k → A ⊕ Fin m) : FirstOrder.Language.Structure.RelMap (Sum.inl r) x ↔ ∃ (y : Fin k → A), (∀ (i : Fin k), x i = Sum.inl (y i)) ∧ FirstOrder.Language.Structure.RelMap r y

@[simp]

theorem DescriptiveComplexity.relMap_ext_inl {L : FirstOrder.Language} {A : Type} {m : ℕ} [L.Structure A] [Nonempty A] {k : ℕ} (r : L.Relations k) (y : Fin k → A) : (FirstOrder.Language.Structure.RelMap (Sum.inl r) fun (i : Fin k) => Sum.inl (y i)) ↔ FirstOrder.Language.Structure.RelMap r y

On original elements, the extended structure is the original one.

@[simp]

theorem DescriptiveComplexity.relMap_ext_old {L : FirstOrder.Language} {A : Type} {m : ℕ} [L.Structure A] [Nonempty A] (x : Fin 1 → A ⊕ Fin m) : FirstOrder.Language.Structure.RelMap (Sum.inr FirstOrder.Language.oldSym) x ↔ IsOld (x 0)

Functoriality in the base structure

def DescriptiveComplexity.extEquiv {L : FirstOrder.Language} {A A' : Type} {m m' : ℕ} [L.IsRelational] [L.Structure A] [L.Structure A'] [Nonempty A] [Nonempty A'] (e : L.Equiv A A') (σ : Fin m ≃ Fin m') : (newLang L).Equiv (A ⊕ Fin m) (A' ⊕ Fin m')

Extended structures are functorial in the base structure: an isomorphism of instances and a bijection of the invented values induce an isomorphism of the extended structures.

Stated for relational vocabularies, the only ones the library uses: on a vocabulary with function symbols the junk interpretation of DescriptiveComplexity.oldPart on invented arguments need not be equivariant.

Equations

• DescriptiveComplexity.extEquiv e σ = { toEquiv := e.sumCongr σ, map_fun' := ⋯, map_rel' := ⋯ }

Definability

SORealize is reused at the one-block list [B], so that an ∃SO[new] sentence is literally an ∃SO sentence – over the extended vocabulary, read in the extended structure.

theorem DescriptiveComplexity.sorealize_singleton {L : FirstOrder.Language} (A : Type) [inst : L.Structure A] (B : SOBlock) (φ : (soLang L [B]).Sentence) : SORealize L A [B] φ true ↔ ∃ (ρ : B.Assignment A), A ⊨ φ

Unfolding of alternating satisfaction at a single existential block.

def DescriptiveComplexity.SigmaSONewDefinable {L : FirstOrder.Language} (P : DecisionProblem L) : Prop

Definability in ∃SO[new], existential second-order logic with value invention: on nonempty finite structures, P A holds exactly when, for some number m of invented values, the relation variables of the block B can be assigned relations over the extended universe A ⊕ Fin m satisfying the first-order kernel φ in the extended structure.

The number m of invented values is unbounded, which is precisely what takes the notion beyond Σ₁ (DescriptiveComplexity.SigmaSODefinable, where the certificate lives over A itself): a witness is a finite object, but no function of |A| bounds its size.

Equations

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

theorem DescriptiveComplexity.sigmaSONewDefinable_congr {L : FirstOrder.Language} {P Q : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ Q.Holds A) : SigmaSONewDefinable P ↔ SigmaSONewDefinable Q

∃SO[new]-definability only depends on the finite instances of a problem.

theorem DescriptiveComplexity.sorealize_new_iso {L : FirstOrder.Language} [L.IsRelational] {A A' : Type} [L.Structure A] [L.Structure A'] [Nonempty A] [Nonempty A'] (e : L.Equiv A A') (B : SOBlock) (φ : (soLang (newLang L) [B]).Sentence) (m : ℕ) : SORealize (newLang L) (A ⊕ Fin m) [B] φ true ↔ SORealize (newLang L) (A' ⊕ Fin m) [B] φ true

An ∃SO[new] sentence expresses an isomorphism-invariant property: what it says of an instance is transported by DescriptiveComplexity.extEquiv.

Inventing nothing

The Σ₁ sentences are the ∃SO[new] sentences that invent nothing: the kernel is guarded by DescriptiveComplexity.noNewSentence, which forces the extended universe to be the original one.

noncomputable def DescriptiveComplexity.noNewSentence (L : FirstOrder.Language) : (newLang L).Sentence

The sentence “nothing was invented”: every element of the universe is an original element.

Equations

• DescriptiveComplexity.noNewSentence L = FirstOrder.Language.Formula.iAlls (Fin 1) (DescriptiveComplexity.oldF✝ L (Sum.inr 0))

theorem DescriptiveComplexity.realize_noNewSentence (L : FirstOrder.Language) (A : Type) [L.Structure A] [Nonempty A] (m : ℕ) : (A ⊕ Fin m) ⊨ noNewSentence L ↔ ∀ (x : A ⊕ Fin m), IsOld x

@[instance_reducible]

def DescriptiveComplexity.allOldMarkStructure (A : Type) : FirstOrder.Language.oldMark.Structure A

The mark of the original elements on the original universe itself: every element is original.

Equations

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

@[instance_reducible]

def DescriptiveComplexity.allOldStructure (L : FirstOrder.Language) (A : Type) [L.Structure A] : (newLang L).Structure A

The instance itself, over the extended vocabulary: nothing is invented, so every element is marked as original.

Equations

• DescriptiveComplexity.allOldStructure L A = L.sumStructure FirstOrder.Language.oldMark A

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

With no invented values, the extended structure is the instance itself.

Equations

• DescriptiveComplexity.extEquivNoNew L A m = { toEquiv := (Equiv.sumEmpty A (Fin m)).symm, map_fun' := ⋯, map_rel' := ⋯ }

Σ₁ ⊆ ∃SO[new]

theorem DescriptiveComplexity.SigmaSODefinable.toNew {L : FirstOrder.Language} {P : DecisionProblem L} (h : SigmaSODefinable 1 P) : SigmaSONewDefinable P

Existential second-order definability implies ∃SO[new]-definability: an ∃SO sentence becomes an ∃SO[new] sentence when guarded by “nothing was invented”. Once RE is a complexity class, this is the inclusion NP ⊆ RE.