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).

Bounding the certificate by the instance is what keeps a second-order class inside NP: a Σ₁ sentence guesses relations over A itself, so the search space is exponential in |A|. 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).

The vocabulary is relational, as every vocabulary of a DescriptiveComplexity.DecisionProblem is, so invented values carry no structure at all until the certificate's relations put some on them.

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 N : Type} : A ⊕ N → Prop

The original elements of a universe extended by invented values. The invented values are an arbitrary type, so that the same predicate reads an extension by a set of them and not only by an initial segment.

Equations

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

@[instance_reducible]

def DescriptiveComplexity.extBase (L : FirstOrder.Language) [L.IsRelational] (A : Type) [L.Structure 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]

instance DescriptiveComplexity.extStructure (L : FirstOrder.Language) [L.IsRelational] (A : Type) [L.Structure 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

theorem DescriptiveComplexity.relMap_ext_iff {L : FirstOrder.Language} {A : Type} {m : ℕ} [L.IsRelational] [L.Structure 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.IsRelational] [L.Structure 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.IsRelational] [L.Structure 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'] (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.

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} [L.IsRelational] (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} [L.IsRelational] {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.

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) [L.IsRelational] (A : Type) [L.Structure 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) [L.IsRelational] (A : Type) [L.Structure 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.sorealize_guardNoNew_iff {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} (φ : (soLang L [B]).Sentence) (A : Type) [instA : L.Structure A] (m : ℕ) : SORealize (newLang L) (A ⊕ Fin m) [B] ((soLangEmbed [B] (newLang L)).onSentence (noNewSentence L) ⊓ (soLangLift [B] L (newLang L) FirstOrder.Language.LHom.sumInl).onSentence φ) true ↔ IsEmpty (Fin m) ∧ SORealize L A [B] φ true

The guarded sentence, read over an extended universe: it holds exactly when nothing was invented and the original sentence holds over the instance itself. This is the whole content of inventing nothing, and it is what both DescriptiveComplexity.SigmaSODefinable.toNew and its bounded twin read.

theorem DescriptiveComplexity.SigmaSODefinable.toNew {L : FirstOrder.Language} [L.IsRelational] {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.