Existential second-order logic with value invention

Lax624099.ValueInvention · concepts/Lax624099/ValueInvention.lean · lax-624099

definition

Loading review…

Natural Language Statement

Definition

Existential second-order logic with value invention, $\exists$ SO[new], is existential second-order logic whose relation variables range over the universe of the structure extended by finitely many invented values, in the style of the object-creating query languages of Abiteboul, Hull and Vianu (1995), chapter 18. An instance $A$ and a number $m$ of invented values give the extended structure on the disjoint union of $A$ and $m$ new elements, over the vocabulary of $A$ together with one unary predicate marking the original elements: the symbols of $A$ hold on original elements exactly where they hold in $A$ , and invented values are related to nothing. A decision problem is $\exists$ SO[new]-definable when, for one existential second-order block and one first-order kernel, a nonempty finite structure is a yes-instance exactly when for some number of invented values the block's relation variables can be assigned relations over the extended universe satisfying the kernel in the extended structure. The number of invented values is unbounded, which is what takes the notion beyond existential second-order logic; a witness is still a finite object.

Concept map

3 concepts; 19 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Data.Fintype.Lattice
2	import Mathlib.ModelTheory.Order
3	import Mathlib.ModelTheory.Semantics
4	import Mathlib.ModelTheory.Complexity
5	import Mathlib.Tactic.FinCases
6	import Lax904597.Problems
7	import Lax904597.SecondOrder
8
9	/-!
10	---
11	title: Existential second-order logic with value invention
12	type: definition
13	---
14	Existential second-order logic with value invention, $\exists$ SO[new], is
15	existential second-order logic whose relation variables range over the
16	universe of the structure extended by finitely many invented values, in the
17	style of the object-creating query languages of Abiteboul, Hull and Vianu
18	(1995), chapter 18. An
19	instance $A$ and a number $m$ of invented values give the extended structure
20	on the disjoint union of $A$ and $m$ new elements, over the vocabulary of $A$
21	together with one unary predicate marking the original elements: the symbols
22	of $A$ hold on original elements exactly where they hold in $A$ , and invented
23	values are related to nothing. A decision problem is $\exists$ SO[new]-definable
24	when, for one existential second-order block and one first-order kernel, a
25	nonempty finite structure is a yes-instance exactly when for some number of
26	invented values the block's relation variables can be assigned relations over
27	the extended universe satisfying the kernel in the extended structure. The
28	number of invented values is unbounded, which is what takes the notion beyond
29	existential second-order logic; a witness is still a finite object.
30	-/
31
32	namespace Lax624099.ValueInvention
33
34	open Lax904597.Problems Lax904597.SecondOrder
35
36	open FirstOrder
37
38	open FirstOrder.Language
39
40	/-- Relation symbols of the language marking the original elements inside an
41	extended universe. -/
42	inductive oldRel : ℕ → Type
43	/-- `old x`: the element `x` comes from the original structure, i.e., it is
44	not an invented value. -/
45	\| old : oldRel 1
46	deriving DecidableEq
47
48	/-- The one-symbol relational language marking, inside a universe extended
49	with invented values, the elements of the original structure. -/
50	def oldMark : Language :=
51	⟨fun _ => Empty, oldRel⟩
52
53	instance instIsRelationalOldMark : IsRelational oldMark :=
54	fun _ => ⟨fun f => Empty.elim f⟩
55
56	open FirstOrder
57
58	open Language Structure
59
60	/-- The vocabulary of extended structures: the base vocabulary together with
61	the unary predicate `old` marking the elements of the original structure. -/
62	abbrev newLang (L : Language.{0, 0}) : Language := L.sum oldMark
63
64	section Extended
65
66	/-- The original elements of a universe extended by invented values. The
67	invented values are an arbitrary type, so that the same predicate reads an
68	extension by a set of them and not only by an initial segment. -/
69	def IsOld {A N : Type} : A ⊕ N → Prop
70	\| Sum.inl _ => True
71	\| Sum.inr _ => False
72
73	/-- The base structure carried by the extended universe: a relation symbol
74	holds of a tuple exactly when all its entries are original elements and it
75	holds of them in `A`. Invented values are related to nothing. -/
76	@[reducible]
77	def extBase (L : Language.{0, 0}) [L.IsRelational] (A : Type) [L.Structure A] (m : ℕ) :
78	L.Structure (A ⊕ Fin m) where
79	funMap f := isEmptyElim f
80	RelMap {_k} r x := ∃ y, (∀ i, x i = Sum.inl (y i)) ∧ RelMap r y
81
82	/-- The interpretation of the marking predicate on the extended universe. -/
83	@[reducible]
84	def oldMarkStructure (A : Type) (m : ℕ) : oldMark.Structure (A ⊕ Fin m) where
85	RelMap \| .old => fun x => IsOld (x 0)
86
87	/-- The extended structure: the instance `A` together with `m` invented
88	values, over the vocabulary `DescriptiveComplexity.newLang L`. -/
89	instance extStructure (L : Language.{0, 0}) [L.IsRelational] (A : Type) [L.Structure A]
90	(m : ℕ) : (newLang L).Structure (A ⊕ Fin m) :=
91	@sumStructure L oldMark (A ⊕ Fin m) (extBase L A m) (oldMarkStructure A m)
92
93	end Extended
94
95	section Definability
96
97	variable {L : Language.{0, 0}}
98
99	/-- Definability in `∃SO[new]`, existential second-order logic with value
100	invention: on nonempty finite structures, `P A` holds exactly when, for some
101	number `m` of invented values, the relation variables of the block `B` can be
102	assigned relations over the extended universe `A ⊕ Fin m` satisfying the
103	first-order kernel `φ` in the extended structure.
104
105	The number `m` of invented values is unbounded, which is precisely what takes
106	the notion beyond `Σ₁` (`DescriptiveComplexity.SigmaSODefinable`, where the
107	certificate lives over `A` itself): a witness is a finite object, but no
108	function of `\|A\|` bounds its size. -/
109	def SigmaSONewDefinable [L.IsRelational] (P : DecisionProblem L) : Prop :=
110	∃ B : SOBlock, ∃ φ : (soLang (newLang L) [B]).Sentence,
111	∀ (A : Type) [L.Structure A] [Finite A] [Nonempty A],
112	P A ↔ ∃ m : ℕ, SORealize (newLang L) (A ⊕ Fin m) [B] φ true
113
114	end Definability
115
116	end Lax624099.ValueInvention
117

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Existential second-order logic with value invention

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments