Lax3.FirstOrder

First-order logic on graphs

concepts/Lax3/FirstOrder.lean · lax-3

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

A first-order formula over graphs is built from two atoms — two vertices are adjacent, two vertices are equal — by negation, conjunction, and quantification over vertices. A formula holds in a graph under an assignment of vertices to its free variables, by the usual reading of the connectives and the quantifier. The quantifier rank of a formula is the nesting depth of its quantifiers.

This is the input logic of the model-checking problem this submission is about: a statement of that problem is allowed to mention first-order sentences and graphs, and nothing else. The distance logic of $Lax3.DistFO$ — first-order logic with distance atoms and local quantification — is the logic the algorithm manipulates internally; it is a different syntax with the same expressive power, introduced there because it admits a finer rank measure. Keeping the two apart is the point: a theorem stated for $FO$ cannot be weakened by any convenience built into $DistFO$ .

Lean source view on GitHub

1	import Mathlib.Combinatorics.SimpleGraph.Basic
2	import Mathlib.Data.Fin.Tuple.Basic
3
4	/-!
5	---
6	title: First-order logic on graphs
7	type: definition
8	---
9	A first-order formula over graphs is built from two atoms — two
10	vertices are adjacent, two vertices are equal — by negation,
11	conjunction, and quantification over vertices. A formula holds in a
12	graph under an assignment of vertices to its free variables, by the
13	usual reading of the connectives and the quantifier. The quantifier
14	rank of a formula is the nesting depth of its quantifiers.
15
16	This is the input logic of the model-checking problem this submission
17	is about: a statement of that problem is allowed to mention first-order
18	sentences and graphs, and nothing else. The distance logic of
19	`Lax3.DistFO` — first-order logic with distance atoms and local
20	quantification — is the logic the algorithm manipulates internally; it
21	is a different syntax with the same expressive power, introduced there
22	because it admits a finer rank measure. Keeping the two apart is the
23	point: a theorem stated for `FO` cannot be weakened by any convenience
24	built into `DistFO`.
25
26	# Formalization notes
27
28	Free variables are counted rather than named: `FO k` is the type of
29	formulas with `k` free variables, and the quantifier turns a formula
30	with one more free variable into a formula with one fewer. Satisfaction
31	is therefore a total function of a formula and an environment
32	`Fin k → Fin n`, one entry per free variable: there is no partial
33	valuation, no default value for an unassigned variable and no
34	well-formedness side condition. A sentence is a formula of `FO 0`, so
35	being closed is a property of the type rather than a predicate to
36	check. The price is that variables are de Bruijn positions rather than
37	names; the alternative, named variables, needs capture-avoiding
38	substitution inside the trusted definition, which is a considerably
39	worse object to audit than an index. This is the pattern of submission
40	Lax11's MSO concept, minus the set variables.
41
42	Variables are levels, not indices: the quantifier extends the
43	environment at its last position (`Fin.snoc`), so the outermost bound
44	variable of a formula is `0` and the innermost is the last. Nothing in
45	the definition shifts an index.
46
47	Only negation, conjunction and existential quantification are
48	constructors. Disjunction, implication and universal quantification are
49	the usual abbreviations, written out where they are used: each of them
50	as a constructor would add a case to the definition of satisfaction and
51	buy nothing that is not already there.
52
53	Graphs here are uncolored — the signature is one binary symmetric
54	relation. Colors are a device of the algorithm, not of the problem
55	statement: they record intermediate information (which vertices were
56	isolated, which distance profile a vertex has) that the input never
57	carries. The logic that has them is `Lax3.DistFO`, over the colored
58	graphs of `Lax3.ColoredGraphs`.
59	-/
60
61	namespace Lax3.FirstOrder
62
63	/-- Formulas of first-order logic over the adjacency signature, with
64	`k` free variables. Variables are `Fin k`, and the quantifier binds the
65	new last index. -/
66	inductive FO : ℕ → Type
67	/-- The vertices `i` and `j` are adjacent. -/
68	\| adj {k : ℕ} (i j : Fin k) : FO k
69	/-- The vertices `i` and `j` are equal. -/
70	\| eq {k : ℕ} (i j : Fin k) : FO k
71	/-- Negation. -/
72	\| not {k : ℕ} (φ : FO k) : FO k
73	/-- Conjunction. -/
74	\| and {k : ℕ} (φ ψ : FO k) : FO k
75	/-- There is a vertex satisfying `φ`, bound at the last index. -/
76	\| ex {k : ℕ} (φ : FO (k + 1)) : FO k
77
78	/-- The quantifier rank: the nesting depth of quantifiers. -/
79	def rank : {k : ℕ} → FO k → ℕ
80	\| _, .adj _ _ => 0
81	\| _, .eq _ _ => 0
82	\| _, .not φ => rank φ
83	\| _, .and φ ψ => max (rank φ) (rank ψ)
84	\| _, .ex φ => rank φ + 1
85
86	variable {n : ℕ}
87
88	/-- Satisfaction of a formula in the graph `G` under the environment
89	`m`, which assigns a vertex to each free variable. -/
90	def Sat (G : SimpleGraph (Fin n)) : {k : ℕ} → (Fin k → Fin n) → FO k → Prop
91	\| _, m, .adj i j => G.Adj (m i) (m j)
92	\| _, m, .eq i j => m i = m j
93	\| _, m, .not φ => ¬ Sat G m φ
94	\| _, m, .and φ ψ => Sat G m φ ∧ Sat G m ψ
95	\| _, m, .ex φ => ∃ v : Fin n, Sat G (Fin.snoc m v) φ
96
97	end Lax3.FirstOrder
98

Formalization notes

Free variables are counted rather than named: $FO k$ is the type of formulas with $k$ free variables, and the quantifier turns a formula with one more free variable into a formula with one fewer. Satisfaction is therefore a total function of a formula and an environment $Fin k → Fin n$ , one entry per free variable: there is no partial valuation, no default value for an unassigned variable and no well-formedness side condition. A sentence is a formula of $FO 0$ , so being closed is a property of the type rather than a predicate to check. The price is that variables are de Bruijn positions rather than names; the alternative, named variables, needs capture-avoiding substitution inside the trusted definition, which is a considerably worse object to audit than an index. This is the pattern of submission Lax11's MSO concept, minus the set variables.

Variables are levels, not indices: the quantifier extends the environment at its last position ( $Fin.snoc$ ), so the outermost bound variable of a formula is $0$ and the innermost is the last. Nothing in the definition shifts an index.

Only negation, conjunction and existential quantification are constructors. Disjunction, implication and universal quantification are the usual abbreviations, written out where they are used: each of them as a constructor would add a case to the definition of satisfaction and buy nothing that is not already there.

Graphs here are uncolored — the signature is one binary symmetric relation. Colors are a device of the algorithm, not of the problem statement: they record intermediate information (which vertices were isolated, which distance profile a vertex has) that the input never carries. The logic that has them is $Lax3.DistFO$ , over the colored graphs of $Lax3.ColoredGraphs$ .

Builds on

none

Used by

Lax3.ModelChecking

From Mathlib

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive

First-order logic on graphs

Flags

Flag this concept