Second-order definability with bounded alternation

Lax904597.SecondOrder · concepts/Lax904597/SecondOrder.lean · lax-904597

definition

Loading review…

Natural Language Statement

Definition

A second-order quantifier block is a finite family of relation variables with given arities. A first-order sentence over the vocabulary expanded by $k$ blocks, read with the blocks quantified alternately, is a $\Sigma_k$ sentence when the first block is existential and a $\Pi_k$ sentence when it is universal; a decision problem is $\Sigma_k$ - or $\Pi_k$ -definable when such a sentence defines it on nonempty finite structures. No object-level second-order syntax is needed: a block is instantiated by an assignment of actual relations, which turns it into a structure over the block's own vocabulary, and only the first-order kernel is an object-level sentence.

$\Sigma_1$ -definability is existential second-order logic, and by Fagin's theorem the $\Sigma_1$ -definable problems are exactly NP. This is how NP is defined in this submission: as $\Sigma_1$ -definability, with no machine model.

Concept map

2 concepts; 4 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.ModelTheory.Semantics
2	import Lax904597.Problems
3
4	/-!
5	---
6	title: Second-order definability with bounded alternation
7	type: definition
8	---
9	A second-order quantifier block is a finite family of relation variables
10	with given arities. A first-order sentence over the vocabulary expanded by
11	$k$ blocks, read with the blocks quantified alternately, is a $\Sigma_k$
12	sentence when the first block is existential and a $\Pi_k$ sentence when it
13	is universal; a decision problem is $\Sigma_k$ - or $\Pi_k$ -definable when
14	such a sentence defines it on nonempty finite structures. No object-level
15	second-order syntax is needed: a block is instantiated by an assignment of
16	actual relations, which turns it into a structure over the block's own
17	vocabulary, and only the first-order kernel is an object-level sentence.
18
19	$\Sigma_1$ -definability is existential second-order logic, and by Fagin's
20	theorem the $\Sigma_1$ -definable problems are exactly NP. This is how NP is
21	defined in this submission: as $\Sigma_1$ -definability, with no machine
22	model.
23	-/
24
25	namespace Lax904597.SecondOrder
26
27	open FirstOrder FirstOrder.Language Lax904597.Problems
28
29	/-- A second-order quantifier block: finitely many relation variables, with
30	given arities. The index type is arbitrary rather than an initial segment of
31	`ℕ`, so that constructions on blocks can build their natural index types. -/
32	structure SOBlock : Type 1 where
33	/-- The index type of the relation variables of the block. -/
34	ι : Type
35	/-- A block has finitely many relation variables. -/
36	[ιFinite : Finite ι]
37	/-- The arity of each relation variable. -/
38	arity : ι → ℕ
39
40	attribute [instance] SOBlock.ιFinite
41
42	/-- The relational vocabulary of a block: one relation symbol per relation
43	variable. -/
44	def SOBlock.lang (B : SOBlock) : Language :=
45	⟨fun _ => Empty, fun n => {i : B.ι // B.arity i = n}⟩
46
47	instance instIsRelationalLang (B : SOBlock) : IsRelational B.lang :=
48	fun _ => ⟨fun f => Empty.elim f⟩
49
50	/-- An assignment of actual relations on a universe `A` to the relation
51	variables of a block. -/
52	def SOBlock.Assignment (B : SOBlock) (A : Type) : Type :=
53	∀ i : B.ι, (Fin (B.arity i) → A) → Prop
54
55	/-- The structure over the block's vocabulary determined by an assignment. -/
56	@[reducible]
57	def SOBlock.structure (B : SOBlock) {A : Type} (ρ : B.Assignment A) :
58	B.lang.Structure A where
59	funMap f := isEmptyElim f
60	RelMap := fun {_} r x => ρ r.1 fun j => x (Fin.cast r.2 j)
61
62	/-- The base vocabulary expanded by the vocabularies of a list of blocks. -/
63	def soLang (L : Language.{0, 0}) : List SOBlock → Language.{0, 0}
64	\| [] => L
65	\| B :: Bs => soLang (L.sum B.lang) Bs
66
67	/-- Alternating second-order satisfaction: the sentence obtained from the
68	first-order kernel `φ` by quantifying the blocks `Bs` alternately,
69	existentially first when `pol` is `true`, holds in the `L`-structure `A`. -/
70	def SORealize (L : Language.{0, 0}) (A : Type) [inst : L.Structure A] :
71	∀ (Bs : List SOBlock), (soLang L Bs).Sentence → Bool → Prop
72	\| [], φ, _ => @Sentence.Realize L A inst φ
73	\| B :: Bs, φ, true =>
74	∃ ρ : B.Assignment A,
75	@SORealize (L.sum B.lang) A (@sumStructure L B.lang A inst (B.structure ρ))
76	Bs φ false
77	\| B :: Bs, φ, false =>
78	∀ ρ : B.Assignment A,
79	@SORealize (L.sum B.lang) A (@sumStructure L B.lang A inst (B.structure ρ))
80	Bs φ true
81
82	variable {L : Language.{0, 0}}
83
84	/-- A decision problem is `Σₖ`-definable if, on nonempty finite structures, it
85	is defined by a second-order sentence with `k` alternating blocks of
86	second-order quantifiers, starting existentially. -/
87	def SigmaSODefinable [L.IsRelational] (k : ℕ) (P : DecisionProblem L) : Prop :=
88	∃ Bs : List SOBlock, Bs.length = k ∧
89	∃ φ : (soLang L Bs).Sentence,
90	∀ (A : Type) [L.Structure A] [Finite A] [Nonempty A], P A ↔ SORealize L A Bs φ true
91
92	/-- A decision problem is `Πₖ`-definable if, on nonempty finite structures, it
93	is defined by a second-order sentence with `k` alternating blocks of
94	second-order quantifiers, starting universally. -/
95	def PiSODefinable [L.IsRelational] (k : ℕ) (P : DecisionProblem L) : Prop :=
96	∃ Bs : List SOBlock, Bs.length = k ∧
97	∃ φ : (soLang L Bs).Sentence,
98	∀ (A : Type) [L.Structure A] [Finite A] [Nonempty A], P A ↔ SORealize L A Bs φ false
99
100	end Lax904597.SecondOrder
101