Documentation

Complexity.Logics.SecondOrder.IndependentSet

Independent set, clique and vertex cover are existential second-order definable #

A sizedGraph structure has an independent set of the target size exactly when some set S of vertices and some binary relation F satisfy: F is a bijection from S onto the size relation, and no two distinct vertices of S are adjacent. This is an existential second-order sentence (Cslib.Logic.FO.sizedGraph.independentSetSentence), so the class sizedGraph.IndependentSet is existential second-order definable [Fag74], Immerman, Chapter 7; so are clique and vertex cover, which are quantifier-free reducible to it.

Main definitions #

Main results #

References #

source
@[reducible, inline]
abbrev Cslib.Logic.FO.sizedGraph.independentSetArity :
Fin 2 → ℕ

The arities of the relation variables: a unary S and a binary F.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.Logic.FO.sizedGraph.independentSetLanguage :
    FirstOrder.Language

    The language of the independent-set sentence.

    Instances For
      source
      @[reducible, inline]
      abbrev Cslib.Logic.FO.sizedGraph.adjSym :
      independentSetLanguage.Relations 2

      The edge relation, among the symbols of the independent-set sentence.

      Instances For
        source
        @[reducible, inline]
        abbrev Cslib.Logic.FO.sizedGraph.sizeSym :
        independentSetLanguage.Relations 1

        The size relation, among the symbols of the independent-set sentence.

        Instances For
          source
          @[reducible, inline]
          abbrev Cslib.Logic.FO.sizedGraph.setSym :
          independentSetLanguage.Relations 1

          The relation variable S, the independent set.

          Instances For
            source
            @[reducible, inline]
            abbrev Cslib.Logic.FO.sizedGraph.bijSym :
            independentSetLanguage.Relations 2

            The relation variable F, a bijection from S onto the size relation.

            Instances For
              source
              def Cslib.Logic.FO.sizedGraph.independentSetMatrix :
              independentSetLanguage.Sentence

              The first-order part of the independent-set sentence: F is a bijection from S onto the size relation, and S is independent.

              Instances For
                source
                def Cslib.Logic.FO.sizedGraph.independentSetSentence :
                ESO.Sentence sizedGraph

                The independent-set sentence ∃ S F, F is a bijection from S onto size ∧ S is independent.

                Instances For
                  source
                  theorem Cslib.Logic.FO.sizedGraph.realize_independentSetSentence {M : Type u_1} [sizedGraph.Structure M] [Finite M] :
                  independentSetSentence.Realize M ↔ ∃ (s : Set M), s.ncard = {x : M | FirstOrder.Language.Structure.RelMap sizedGraph.size ![x]}.ncard ∧ s.Pairwise fun (x y : M) => ¬FirstOrder.Language.Structure.RelMap sizedGraph.adj ![x, y]

                  The independent-set sentence holds exactly in the structures with an independent set of the target size.

                  source
                  theorem Cslib.Logic.FO.sizedGraph.definable_IndependentSet :
                  ESO.Definable IndependentSet

                  Independent set is existential second-order definable.

                  source
                  theorem Cslib.Logic.FO.sizedGraph.definable_Clique :
                  ESO.Definable Clique

                  Clique is existential second-order definable, as it reduces to independent set.

                  source
                  theorem Cslib.Logic.FO.sizedGraph.definable_VertexCover :
                  ESO.Definable VertexCover

                  Vertex cover is existential second-order definable, as it reduces to independent set.