Second-order fixed points

Lax480241.SecondOrderFixedPoints · concepts/Lax480241/SecondOrderFixedPoints.lean · lax-480241

definition

Loading review…

Natural Language Statement

Definition

SO(≤, LFP) and SO(≤, PFP) are first-order logic with least and partial fixed points read one exponential up: a problem $P$ is SO(≤, LFP)-definable when an exponential expansion $X$ and an FO(≤, LFP)-definable problem $Q$ of its vocabulary are such that $P(A)$ holds exactly when $Q(X(A))$ does, for every nonempty finite structure $A$ and every linear order on it. The order-free forms use expansions whose sentences read no order, the equivalence being asked of structures carrying none.

Concept map

10 concepts; 7 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Tactic.FinCases
2	import Mathlib.Order.PiLex
3	import Mathlib.Data.Prod.Lex
4	import Mathlib.Data.Fintype.EquivFin
5	import Mathlib.ModelTheory.Order
6	import Mathlib.ModelTheory.Semantics
7	import Mathlib.ModelTheory.Complexity
8	import Mathlib.Logic.Equiv.Fin.Basic
9	import Mathlib.Data.Fintype.Lattice
10	import Mathlib.Data.Finite.Sigma
11	import Mathlib.Order.Lattice.Nat
12	import Mathlib.Data.Set.Card
13	import Mathlib.Data.Fintype.Pigeonhole
14	import Mathlib.Dynamics.FixedPoints.Basic
15	import Mathlib.ModelTheory.Syntax
16	import Mathlib.SetTheory.Cardinal.Finite
17	import Mathlib.Logic.Relation
18	import Mathlib.Algebra.BigOperators.Finprod
19	import Mathlib.Data.Set.Finite.Lemmas
20	import Mathlib.Logic.Equiv.Prod
21	import Mathlib.Algebra.Order.BigOperators.Group.Finset
22	import Mathlib.Data.Fintype.Card
23	import Lax134656.PartialFixedPoint
24	import Lax480241.Expansions
25	import Lax535992.LeastFixedPoint
26	import Lax904597.Problems
27	import Lax904597.SecondOrder
28	import Lax904597.Interpretations
29
30	/-!
31	---
32	title: Second-order fixed points
33	type: definition
34	---
35	SO(≤, LFP) and SO(≤, PFP) are first-order logic with least and partial fixed
36	points read one exponential up: a problem $P$ is SO(≤, LFP)-definable when
37	an exponential expansion $X$ and an FO(≤, LFP)-definable problem $Q$ of its
38	vocabulary are such that $P(A)$ holds exactly when $Q(X(A))$ does, for every
39	nonempty finite structure $A$ and every linear order on it. The order-free
40	forms use expansions whose sentences read no order, the equivalence being
41	asked of structures carrying none.
42	-/
43
44	namespace Lax480241.SecondOrderFixedPoints
45
46	open Lax134656.PartialFixedPoint Lax480241.Expansions Lax535992.LeastFixedPoint Lax904597.Problems
47	open Lax904597.SecondOrder
48
49	open FirstOrder
50
51	open Language Structure
52
53	variable {L : Language.{0, 0}}
54
55	/-- An order-free exponential expansion: as
56	`ExpExpansion`, except that the domain sentence and the
57	defining sentences live over the bare vocabulary expanded by copies of the
58	block, with no order symbol available. Its universe is therefore defined on a
59	structure carrying no order. -/
60	structure ExpExpansionFree (L : Language.{0, 0}) : Type 1 where
61	/-- The tags: finitely many copies of the space of block assignments. -/
62	Tag : Type
63	/-- Tags are finite, so that finite structures expand to finite
64	structures. -/
65	[tagFinite : Finite Tag]
66	/-- The block whose assignments are the points of the expanded universe. -/
67	B : SOBlock
68	/-- The vocabulary of the expanded structure. -/
69	E : Language.{0, 0}
70	/-- The expanded vocabulary is relational, as every vocabulary of this
71	library. -/
72	[eRelational : E.IsRelational]
73	/-- The domain sentence of each tag, over the bare vocabulary. -/
74	dom : Tag → (L.sum B.lang).Sentence
75	/-- The defining sentence of each relation symbol at each tuple of tags, over
76	the bare vocabulary and as many copies of the block as the symbol has
77	arguments. -/
78	relSentence : ∀ {n : ℕ}, E.Relations n → (Fin n → Tag) →
79	(L.sum (SOBlock.replicate B n).lang).Sentence
80	/-- The definable domain is inhabited. -/
81	dom_nonempty : ∀ (A : Type) [L.Structure A] [Finite A] [Nonempty A],
82	∃ (t : Tag) (ρ : B.Assignment A),
83	@Sentence.Realize _ A (SOBlock.structure₁ B (L := L) ρ) (dom t)
84
85	namespace ExpExpansionFree
86
87	variable (X : ExpExpansionFree L)
88
89	attribute [instance] tagFinite eRelational
90
91	/-- A candidate point: a tagged assignment of the block. -/
92	abbrev Point (A : Type) : Type := X.Tag × X.B.Assignment A
93
94	variable {X}
95
96	/-- The domain condition on a candidate point. -/
97	def DomHolds {A : Type} [L.Structure A] (p : X.Point A) : Prop :=
98	@Sentence.Realize _ A (SOBlock.structure₁ X.B (L := L) p.2) (X.dom p.1)
99
100	variable (X)
101
102	/-- The expanded universe: the tagged block assignments satisfying their
103	tag's domain sentence. No order on `A` is involved. -/
104	def Map (A : Type) [L.Structure A] : Type := {p : X.Point A // DomHolds p}
105
106	variable {X}
107
108	variable (X)
109
110	/-- The expanded structure. -/
111	instance mapStructure (A : Type) [L.Structure A] : X.E.Structure (X.Map A) where
112	funMap f := isEmptyElim f
113	RelMap {n} r xs :=
114	@Sentence.Realize _ A
115	(SOBlock.structure₁ (SOBlock.replicate X.B n) (L := L)
116	(SOBlock.replicateAssign X.B fun i => (xs i).1.2))
117	(X.relSentence r fun i => (xs i).1.1)
118
119	instance mapFinite (A : Type) [L.Structure A] [Finite A] : Finite (X.Map A) :=
120	inferInstanceAs (Finite {p : X.Point A // DomHolds p})
121
122	instance mapNonempty (A : Type) [L.Structure A] [Finite A] [Nonempty A] :
123	Nonempty (X.Map A) :=
124	let ⟨t, ρ, h⟩ := X.dom_nonempty A
125	⟨⟨(t, ρ), h⟩⟩
126
127	end ExpExpansionFree
128
129	open FirstOrder
130
131	open Language Structure
132
133	variable {L : Language.{0, 0}} [L.IsRelational]
134
135	/-- SO(PFP) without the order: a partial fixed point over a second-order
136	universe defined without an order, the equivalence being asked of structures
137	carrying none. -/
138	def SOPFPDefinableFree (P : DecisionProblem L) : Prop :=
139	∃ (X : ExpExpansionFree L) (Q : DecisionProblem X.E), PFPDefinable Q ∧
140	∀ (A : Type) [L.Structure A] [Finite A] [Nonempty A], P A ↔ Q (X.Map A)
141
142	open FirstOrder
143
144	open Language Structure
145
146	variable {L : Language.{0, 0}} [L.IsRelational]
147
148	/-- SO(LFP) without the order: a least fixed point over a second-order
149	universe defined without an order, the equivalence being asked of structures
150	carrying none. -/
151	def SOLFPDefinableFree (P : DecisionProblem L) : Prop :=
152	∃ (X : ExpExpansionFree L) (Q : DecisionProblem X.E), LFPDefinable Q ∧
153	∀ (A : Type) [L.Structure A] [Finite A] [Nonempty A], P A ↔ Q (X.Map A)
154
155	open FirstOrder
156
157	open Language
158
159	variable {L : Language.{0, 0}} [L.IsRelational]
160
161	/-- SO(≤, LFP): a least fixed point over a second-order universe. The
162	problem holds of `A` exactly when an FO(≤, LFP) definition holds of an
163	exponential expansion of `A`. The order the expansion's own sentences read can
164	be removed (`solfpDefinable_iff_free`), by guessing it
165	into the block. -/
166	def SOLFPDefinable (P : DecisionProblem L) : Prop :=
167	∃ (X : ExpExpansion L) (Q : DecisionProblem X.E), LFPDefinable Q ∧
168	∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A], P A ↔ Q (X.Map A)
169
170	/-- SO(≤, PFP): a partial fixed point over a second-order universe. The
171	order the expansion's own sentences read can be removed
172	(`sopfpDefinable_iff_free`), by guessing it into the
173	block. -/
174	def SOPFPDefinable (P : DecisionProblem L) : Prop :=
175	∃ (X : ExpExpansion L) (Q : DecisionProblem X.E), PFPDefinable Q ∧
176	∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A], P A ↔ Q (X.Map A)
177
178	end Lax480241.SecondOrderFixedPoints
179

Builds on

Used by

From Mathlib

Discussion

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

Loading discussion…

Lax Lean Archive

Second-order fixed points

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments