The quantitative logic ΣQSO(FO)

Lax366625.SecondOrderCounting · concepts/Lax366625/SecondOrderCounting.lean · lax-366625

definition

Loading review…

Natural Language Statement

Definition

The terms of ΣQSO(FO), after Arenas, Muñoz, and Riveros, are built from first-order formulas, read as $1$ when they hold and $0$ otherwise, and from constants, by addition, multiplication, sums and products over tuples of elements, and sums over the assignments of a block of relation variables. Their value on a structure is computed accordingly. A counting problem $C$ over $L$ is ΣQSO(FO)-definable when some closed term over $L \cup \{\le\}$ has value $C(A)$ on every nonempty finite $L$ -structure $A$ , for every linear order on $A$ .

Concept map

6 concepts; 12 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Algebra.BigOperators.Finprod
2	import Mathlib.Data.Fintype.Lattice
3	import Mathlib.ModelTheory.Order
4	import Mathlib.ModelTheory.Semantics
5	import Mathlib.ModelTheory.Complexity
6	import Mathlib.Tactic.FinCases
7	import Mathlib.SetTheory.Cardinal.Finite
8	import Mathlib.Order.PiLex
9	import Mathlib.Data.Prod.Lex
10	import Mathlib.Data.Fintype.EquivFin
11	import Mathlib.Logic.Equiv.Fin.Basic
12	import Mathlib.Data.Finite.Sigma
13	import Mathlib.Order.Lattice.Nat
14	import Mathlib.Data.Set.Card
15	import Mathlib.Data.Fintype.Pigeonhole
16	import Mathlib.Dynamics.FixedPoints.Basic
17	import Mathlib.ModelTheory.Syntax
18	import Mathlib.Algebra.Order.BigOperators.Group.Finset
19	import Mathlib.Data.Fintype.Card
20	import Lax366625.CountingProblems
21	import Lax904597.SecondOrder
22
23	/-!
24	---
25	title: The quantitative logic ΣQSO(FO)
26	type: definition
27	---
28	The terms of ΣQSO(FO), after Arenas, Muñoz, and Riveros, are built from
29	first-order formulas, read as $1$ when they hold and $0$ otherwise, and from
30	constants, by addition, multiplication, sums and products over tuples of
31	elements, and sums over the assignments of a block of relation variables.
32	Their value on a structure is computed accordingly. A counting problem $C$
33	over $L$ is ΣQSO(FO)-definable when some closed term over
34	$L \cup \{\le\}$ has value $C(A)$ on every nonempty finite $L$ -structure
35	$A$ , for every linear order on $A$ .
36	-/
37
38	namespace Lax366625.SecondOrderCounting
39
40	open Lax366625.CountingProblems Lax904597.SecondOrder
41
42	open FirstOrder
43
44	open Language Structure
45
46	/-- The terms of ΣQSO(FO) over the vocabulary `L`, with free first-order
47	variables in `α`. A first-order quantifier binds a block of `n` variables at
48	once, the variables `Sum.inr i` of `α ⊕ Fin n`; a second-order sum binds the
49	relation variables of a block, the term under it being over the vocabulary
50	expanded by the block. -/
51	inductive SQTerm : Language.{0, 0} → Type → Type 1
52	/-- A formula: `1` when it holds, `0` when it does not. -/
53	\| ind {L : Language.{0, 0}} {α : Type} (φ : L.Formula α) : SQTerm L α
54	/-- A constant. -/
55	\| const {L : Language.{0, 0}} {α : Type} (s : ℕ) : SQTerm L α
56	/-- A sum. -/
57	\| add {L : Language.{0, 0}} {α : Type} (s t : SQTerm L α) : SQTerm L α
58	/-- A product. -/
59	\| mul {L : Language.{0, 0}} {α : Type} (s t : SQTerm L α) : SQTerm L α
60	/-- `Σx̄. t`: the sum over the `n`-tuples of elements. -/
61	\| sum {L : Language.{0, 0}} {α : Type} (n : ℕ) (t : SQTerm L (α ⊕ Fin n)) : SQTerm L α
62	/-- `Πx̄. t`: the product over the `n`-tuples of elements. -/
63	\| prod {L : Language.{0, 0}} {α : Type} (n : ℕ) (t : SQTerm L (α ⊕ Fin n)) : SQTerm L α
64	/-- `ΣX̄. t`: the sum over the assignments of a block of relation
65	variables. -/
66	\| sosum {L : Language.{0, 0}} {α : Type} (B : SOBlock) (t : SQTerm (L.sum B.lang) α) :
67	SQTerm L α
68
69	namespace SQTerm
70
71	open Classical in
72	/-- The value of a term in a structure, under a valuation. -/
73	noncomputable def eval : ∀ {L : Language.{0, 0}} {α : Type}, SQTerm L α →
74	∀ (A : Type) [L.Structure A], (α → A) → ℕ
75	\| _, _, ind φ, _, _, v => if φ.Realize v then 1 else 0
76	\| _, _, const s, _, _, _ => s
77	\| _, _, add s t, A, _, v => s.eval A v + t.eval A v
78	\| _, _, mul s t, A, _, v => s.eval A v * t.eval A v
79	\| _, _, sum _ t, A, _, v => ∑ᶠ w : Fin _ → A, t.eval A (Sum.elim v w)
80	\| _, _, prod _ t, A, _, v => ∏ᶠ w : Fin _ → A, t.eval A (Sum.elim v w)
81	\| L, _, sosum B t, A, inst, v =>
82	∑ᶠ ρ : B.Assignment A, @eval (L.sum B.lang) _ t A (@sumStructure L _ A inst (B.structure ρ)) v
83
84	/-- The value of a closed term. -/
85	noncomputable def value {L : Language.{0, 0}} (t : SQTerm L Empty) (A : Type) [L.Structure A] : ℕ :=
86	t.eval A default
87
88	end SQTerm
89
90	open FirstOrder
91
92	open Language Structure
93
94	variable {L : Language.{0, 0}} [L.IsRelational]
95
96	/-- A counting problem is ΣQSO(FO)-definable when, on nonempty finite
97	ordered structures, it is the value of a closed term of ΣQSO(FO) over the
98	ordered expansion, whatever the linear order. -/
99	def SQDefinable (C : CountingProblem L) : Prop :=
100	∃ t : SQTerm (L.sum Language.order) Empty,
101	∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A], C A = t.value A
102
103	end Lax366625.SecondOrderCounting
104

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

The quantitative logic ΣQSO(FO)

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments