-
Notifications
You must be signed in to change notification settings - Fork 297
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(model_theory/graph): First-order language and theory of graphs (#…
…13720) Defines `first_order.language.graph`, the language of graphs Defines `first_order.Theory.simple_graph`, the theory of simple graphs Produces models of the theory of simple graphs from simple graphs and vice versa.
- Loading branch information
1 parent
1d4ed4a
commit e56b8fe
Showing
2 changed files
with
118 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,113 @@ | ||
/- | ||
Copyright (c) 2022 Aaron Anderson. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Aaron Anderson | ||
-/ | ||
import model_theory.satisfiability | ||
import combinatorics.simple_graph.basic | ||
|
||
/-! | ||
# First-Ordered Structures in Graph Theory | ||
This file defines first-order languages, structures, and theories in graph theory. | ||
## Main Definitions | ||
* `first_order.language.graph` is the language consisting of a single relation representing | ||
adjacency. | ||
* `simple_graph.Structure` is the first-order structure corresponding to a given simple graph. | ||
* `first_order.language.Theory.simple_graph` is the theory of simple graphs. | ||
* `first_order.language.simple_graph_of_structure` gives the simple graph corresponding to a model | ||
of the theory of simple graphs. | ||
-/ | ||
|
||
universes u v w w' | ||
|
||
namespace first_order | ||
namespace language | ||
open_locale first_order | ||
open Structure | ||
|
||
variables {L : language.{u v}} {α : Type w} {V : Type w'} {n : ℕ} | ||
|
||
/-! ### Simple Graphs -/ | ||
|
||
/-- The language consisting of a single relation representing adjacency. -/ | ||
protected def graph : language := | ||
language.mk₂ empty empty empty empty unit | ||
|
||
/-- The symbol representing the adjacency relation. -/ | ||
def adj : language.graph.relations 2 := unit.star | ||
|
||
/-- Any simple graph can be thought of as a structure in the language of graphs. -/ | ||
def _root_.simple_graph.Structure (G : simple_graph V) : | ||
language.graph.Structure V := | ||
Structure.mk₂ empty.elim empty.elim empty.elim empty.elim (λ _, G.adj) | ||
|
||
namespace graph | ||
|
||
instance : is_relational (language.graph) := language.is_relational_mk₂ | ||
|
||
instance : subsingleton (language.graph.relations n) := | ||
language.subsingleton_mk₂_relations | ||
|
||
end graph | ||
|
||
/-- The theory of simple graphs. -/ | ||
protected def Theory.simple_graph : language.graph.Theory := | ||
{adj.irreflexive, adj.symmetric} | ||
|
||
@[simp] lemma Theory.simple_graph_model_iff [language.graph.Structure V] : | ||
V ⊨ Theory.simple_graph ↔ | ||
irreflexive (λ x y : V, rel_map adj ![x,y]) ∧ symmetric (λ x y : V, rel_map adj ![x,y]) := | ||
by simp [Theory.simple_graph] | ||
|
||
instance simple_graph_model (G : simple_graph V) : | ||
@Theory.model _ V G.Structure Theory.simple_graph := | ||
begin | ||
simp only [Theory.simple_graph_model_iff, rel_map_apply₂], | ||
exact ⟨G.loopless, G.symm⟩, | ||
end | ||
|
||
variables (V) | ||
|
||
/-- Any model of the theory of simple graphs represents a simple graph. -/ | ||
@[simps] def simple_graph_of_structure [language.graph.Structure V] [V ⊨ Theory.simple_graph] : | ||
simple_graph V := | ||
{ adj := λ x y, rel_map adj ![x,y], | ||
symm := relations.realize_symmetric.1 (Theory.realize_sentence_of_mem Theory.simple_graph | ||
(set.mem_insert_of_mem _ (set.mem_singleton _))), | ||
loopless := relations.realize_irreflexive.1 (Theory.realize_sentence_of_mem Theory.simple_graph | ||
(set.mem_insert _ _)) } | ||
|
||
variables {V} | ||
|
||
@[simp] lemma _root_.simple_graph.simple_graph_of_structure (G : simple_graph V) : | ||
@simple_graph_of_structure V G.Structure _ = G := | ||
by { ext, refl } | ||
|
||
@[simp] lemma Structure_simple_graph_of_structure | ||
[S : language.graph.Structure V] [V ⊨ Theory.simple_graph] : | ||
(simple_graph_of_structure V).Structure = S := | ||
begin | ||
ext n f xs, | ||
{ exact (is_relational.empty_functions n).elim f }, | ||
{ ext n r xs, | ||
rw iff_eq_eq, | ||
cases n, | ||
{ exact r.elim }, | ||
{ cases n, | ||
{ exact r.elim }, | ||
{ cases n, | ||
{ cases r, | ||
change rel_map adj ![xs 0, xs 1] = _, | ||
refine congr rfl (funext _), | ||
simp [fin.forall_fin_two], }, | ||
{ exact r.elim } } } } | ||
end | ||
|
||
theorem Theory.simple_graph_is_satisfiable : | ||
Theory.is_satisfiable Theory.simple_graph := | ||
⟨@Theory.Model.of _ _ unit (simple_graph.Structure ⊥) _ _⟩ | ||
|
||
end language | ||
end first_order |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters