nothing to prove
Definition
A finite simple graph is a structure of the language of graphs, with the single binary relation interpreted as adjacency. A graph class transduces another if the corresponding classes of graph structures are related by a first-order transduction.
Lean source view on GitHub
| 1 | import Lax5.GraphClasses |
| 2 | import Lax5.Transductions |
| 3 | import Mathlib.ModelTheory.Graph |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Graph transductions |
| 8 | type: definition |
| 9 | --- |
| 10 | A finite simple graph is a structure of the language of graphs, with the |
| 11 | single binary relation interpreted as adjacency. A graph class |
| 12 | transduces another if the corresponding classes of graph structures are |
| 13 | related by a first-order transduction. |
| 14 | |
| 15 | # Formalization notes |
| 16 | |
| 17 | Graphs enter as structures via mathlib's `SimpleGraph.structure`. The |
| 18 | target structures of a graph transduction are therefore honest graph |
| 19 | structures — symmetric and irreflexive — so the interpreting formula |
| 20 | must define the output adjacency exactly. This matches the common |
| 21 | convention of interpreting by an arbitrary formula `φ` and keeping the |
| 22 | pairs `u ≠ v` with `φ(u,v) ∧ φ(v,u)`: that symmetrized condition is |
| 23 | itself a formula, so both conventions define the same transduces |
| 24 | relation on graph classes. |
| 25 | -/ |
| 26 | |
| 27 | namespace Lax5.GraphTransductions |
| 28 | |
| 29 | open FirstOrder Lax5.GraphClasses |
| 30 | |
| 31 | /-- The members of a graph class, as structures of the language of |
| 32 | graphs: adjacency interprets the binary relation. -/ |
| 33 | def structureClass (C : GraphClass) : |
| 34 | Transductions.StructureClass Language.graph := |
| 35 | fun n S => ∃ G : SimpleGraph (Fin n), C n G ∧ S = G.structure |
| 36 | |
| 37 | /-- `C` transduces `D` as graph classes: the corresponding classes of |
| 38 | graph structures are related by a first-order transduction. -/ |
| 39 | def Transduces (C D : GraphClass) : Prop := |
| 40 | Transductions.Transduces (structureClass C) (structureClass D) |
| 41 | |
| 42 | end Lax5.GraphTransductions |
| 43 |
Formalization notes
Graphs enter as structures via mathlib's SimpleGraph.structure. The
target structures of a graph transduction are therefore honest graph
structures — symmetric and irreflexive — so the interpreting formula
must define the output adjacency exactly. This matches the common
convention of interpreting by an arbitrary formula φ and keeping the
pairs u ≠ v with φ(u,v) ∧ φ(v,u): that symmetrized condition is
itself a formula, so both conventions define the same transduces
relation on graph classes.