Documentation

Mathlib.ModelTheory.Graph

First-Order Structures in Graph Theory #

This file defines first-order languages, structures, and theories in graph theory.

Main Definitions #

Simple Graphs #

source
🔶 coverage
inductive FirstOrder.Language.graphRel :
ℕ → Type

The type of relations for the language of graphs, consisting of a single binary relation adj.

Instances For
    source
    🔸 coverage
    def FirstOrder.Language.instDecidableEqGraphRel.decEq {a✝ : ℕ} (x✝ x✝¹ : graphRel a✝) :
    Decidable (x✝ = x✝¹)
    Instances For
      source
      🔸 coverage
      @[implicit_reducible]
      instance FirstOrder.Language.instDecidableEqGraphRel {a✝ : ℕ} :
      DecidableEq (graphRel a✝)
      source
      🔸 coverage
      def FirstOrder.Language.graph :
      Language

      The language consisting of a single relation representing adjacency.

      Instances For
        source
        🔸 coverage
        @[implicit_reducible]
        instance FirstOrder.Language.instIsRelationalGraph :
        Language.graph.IsRelational
        source
        🔸 coverage
        @[reducible, inline]
        abbrev FirstOrder.Language.adj :
        Language.graph.Relations 2

        The symbol representing the adjacency relation.

        Instances For
          source
          🔸 coverage
          @[implicit_reducible]
          def SimpleGraph.structure {V : Type u} (G : SimpleGraph V) :
          FirstOrder.Language.graph.Structure V

          Any simple graph can be thought of as a structure in the language of graphs.

          Instances For
            source
            📐 coverage
            instance FirstOrder.Language.graph.instSubsingleton {n : ℕ} :
            Subsingleton (Language.graph.Relations n)
            source
            🔸 coverage
            def FirstOrder.Language.Theory.simpleGraph :
            Language.graph.Theory

            The theory of simple graphs.

            Instances For
              source
              📐 coverage
              @[simp]
              theorem FirstOrder.Language.Theory.simpleGraph_model_iff {V : Type u} [Language.graph.Structure V] :
              V ⊨ Theory.simpleGraph ↔ (Std.Irrefl fun (x y : V) => Structure.RelMap adj ![x, y]) ∧ Symmetric fun (x y : V) => Structure.RelMap adj ![x, y]
              source
              📐 coverage
              instance FirstOrder.Language.simpleGraph_model {V : Type u} (G : SimpleGraph V) :
              V ⊨ Theory.simpleGraph
              source
              🔸 coverage
              def FirstOrder.Language.simpleGraphOfStructure (V : Type u) [Language.graph.Structure V] [V ⊨ Theory.simpleGraph] :
              SimpleGraph V

              Any model of the theory of simple graphs represents a simple graph.

              Instances For
                source
                📐 coverage
                @[simp]
                theorem FirstOrder.Language.simpleGraphOfStructure_adj (V : Type u) [Language.graph.Structure V] [V ⊨ Theory.simpleGraph] (x y : V) :
                (simpleGraphOfStructure V).Adj x y = Structure.RelMap adj ![x, y]
                source
                📐 coverage
                @[simp]
                theorem SimpleGraph.simpleGraphOfStructure {V : Type u} (G : SimpleGraph V) :
                FirstOrder.Language.simpleGraphOfStructure V = G
                source
                📐 coverage
                @[simp]
                theorem FirstOrder.Language.structure_simpleGraphOfStructure {V : Type u} [S : Language.graph.Structure V] [V ⊨ Theory.simpleGraph] :
                (simpleGraphOfStructure V).structure = S
                source
                📐 coverage
                theorem FirstOrder.Language.Theory.simpleGraph_isSatisfiable :
                Theory.simpleGraph.IsSatisfiable