First-order logic on colored graphs
Lax185574.FirstOrderLogic · concepts/Lax185574/FirstOrderLogic.lean · lax-185574
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
First-order formulas speak about the vertices of a graph. Their atoms say that two vertices are adjacent, that they are equal, or that a vertex has a color. Formulas are closed under negation, conjunction and existential quantification over vertices. The other connectives and the universal quantifier are expressed by these as usual.
A formula has free variables x₀, …, x_{n−1} for some n, and its quantifier ∃ binds the next variable xₙ. A sentence has no free variables and no colors, and says that the sentence φ holds in the graph G.
Concept map
Lean source view on GitHub
| 1 | import Lax185574.Graphs |
| 2 | import Mathlib.Data.Fin.Tuple.Basic |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: First-order logic on colored graphs |
| 7 | type: definition |
| 8 | --- |
| 9 | First-order formulas speak about the vertices of a graph. Their atoms |
| 10 | say that two vertices are adjacent, that they are equal, or that a |
| 11 | vertex has a color. Formulas are closed under negation, conjunction and |
| 12 | existential quantification over vertices. The other connectives and the |
| 13 | universal quantifier are expressed by these as usual. |
| 14 | |
| 15 | A formula has free variables x₀, …, x_{n−1} for some n, and its |
| 16 | quantifier ∃ binds the next variable xₙ. A *sentence* has no free |
| 17 | variables and no colors, and `G ⊨ φ` says that the sentence φ holds in |
| 18 | the graph G. |
| 19 | |
| 20 | # Formalization notes |
| 21 | |
| 22 | The colors are the elements of a type `K`. Sentences use the empty type |
| 23 | of colors. A coloring of a graph assigns to each color the set of |
| 24 | vertices that have it, and the sets of different colors may overlap. |
| 25 | |
| 26 | The type of a formula records how many free variables it may use, so a |
| 27 | formula cannot refer to a variable that is not bound or assigned. |
| 28 | Variables are numbered by the order in which they are introduced (de |
| 29 | Bruijn levels), so a variable keeps its number under a quantifier, and |
| 30 | `Fin.snoc a v` extends the assignment `a` of x₀, …, x_{n−1} by the vertex |
| 31 | `v` for xₙ. |
| 32 | -/ |
| 33 | |
| 34 | namespace Lax185574.FirstOrderLogic |
| 35 | |
| 36 | open Lax185574.Graphs |
| 37 | |
| 38 | /-- First-order formulas on graphs with colors from `K`, whose free |
| 39 | variables are among `x₀, …, x_{n-1}`. -/ |
| 40 | inductive Formula (K : Type) : ℕ → Type |
| 41 | /-- `xᵢ` and `xⱼ` are adjacent. -/ |
| 42 | | adj {n : ℕ} (i j : Fin n) : Formula K n |
| 43 | /-- `xᵢ` and `xⱼ` are equal. -/ |
| 44 | | eq {n : ℕ} (i j : Fin n) : Formula K n |
| 45 | /-- Negation. -/ |
| 46 | | not {n : ℕ} (φ : Formula K n) : Formula K n |
| 47 | /-- Conjunction. -/ |
| 48 | | and {n : ℕ} (φ ψ : Formula K n) : Formula K n |
| 49 | /-- `∃ xₙ φ`: some vertex can be assigned to `xₙ` so that `φ` holds. -/ |
| 50 | | ex {n : ℕ} (φ : Formula K (n + 1)) : Formula K n |
| 51 | /-- `xᵢ` has the color `c`. -/ |
| 52 | | color {n : ℕ} (c : K) (i : Fin n) : Formula K n |
| 53 | |
| 54 | /-- The formula `φ` holds in the graph `G` with the coloring `col`, when |
| 55 | the free variable `xᵢ` is assigned the vertex `a i`. -/ |
| 56 | def Formula.Holds {K : Type} (G : Graph) (col : K → Set (Fin G.n)) : |
| 57 | {n : ℕ} → Formula K n → (Fin n → Fin G.n) → Prop |
| 58 | | _, .adj i j, a => G.Adj (a i) (a j) |
| 59 | | _, .eq i j, a => a i = a j |
| 60 | | _, .not φ, a => ¬ φ.Holds G col a |
| 61 | | _, .and φ ψ, a => φ.Holds G col a ∧ ψ.Holds G col a |
| 62 | | _, .ex φ, a => ∃ v : Fin G.n, φ.Holds G col (Fin.snoc a v) |
| 63 | | _, .color c i, a => a i ∈ col c |
| 64 | |
| 65 | /-- A sentence: a formula without colors and without free variables. -/ |
| 66 | abbrev Sentence : Type := Formula Empty 0 |
| 67 | |
| 68 | /-- The sentence `φ` holds in the graph `G`. -/ |
| 69 | def Models (G : Graph) (φ : Sentence) : Prop := |
| 70 | φ.Holds G Empty.elim Fin.elim0 |
| 71 | |
| 72 | @[inherit_doc] scoped infix:50 " ⊨ " => Models |
| 73 | |
| 74 | end Lax185574.FirstOrderLogic |
| 75 |
Formalization notes
The colors are the elements of a type . Sentences use the empty type of colors. A coloring of a graph assigns to each color the set of vertices that have it, and the sets of different colors may overlap.
The type of a formula records how many free variables it may use, so a formula cannot refer to a variable that is not bound or assigned. Variables are numbered by the order in which they are introduced (de Bruijn levels), so a variable keeps its number under a quantifier, and extends the assignment of x₀, …, x_{n−1} by the vertex for xₙ.
Builds on
From Mathlib
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments