Documentation

DescriptiveComplexity.Problems.CliqueFamily.Membership

Clique is existential second-order definable #

The membership half of the NP-completeness of Clique: the clique threshold property is Σ₁-definable in the sense of DescriptiveComplexity.SecondOrder (DescriptiveComplexity.clique_sigmaSODefinable). The single existential block guesses two relations – a unary one, the clique itself, and a binary one, an injection of the marked set into the clique – and the first-order kernel checks that the unary relation is a clique and that the binary relation is total on the marked set, lands in the clique, and is injective. On (finite) structures this is equivalent to the existence of an embedding of the marked set into a clique, i.e., to DescriptiveComplexity.HasLargeClique.

Since NP is defined as Σ₁-definability, this is the statement Clique ∈ NP; see DescriptiveComplexity.Problems.CliqueFamily for the NP-completeness theorems of the whole clique family.

source
@[reducible, inline]
abbrev DescriptiveComplexity.kMarkedSym :
cliqueSOLang.Relations 1

The marked symbol over the sum.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev DescriptiveComplexity.cliqueSOLang :
    FirstOrder.Language

    The vocabulary of the kernel: the instance expanded by the block.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev DescriptiveComplexity.kCliqueSym :
      cliqueSOLang.Relations 1

      The clique symbol over the sum.

      Equations
      Instances For
        source
        @[instance_reducible]
        instance DescriptiveComplexity.instFintypeCliqueGuessBlockIx :
        Fintype CliqueGuessBlockIx
        Equations
        • One or more equations did not get rendered due to their size.
        source
        inductive DescriptiveComplexity.CliqueGuessBlockIx :
        Type

        The relation variables of the block.

        Instances For
          source
          @[reducible, inline]
          abbrev DescriptiveComplexity.kInjSym :
          cliqueSOLang.Relations 2

          The inj symbol over the sum.

          Equations
          Instances For
            source
            def DescriptiveComplexity.kInjRel :
            cliqueGuessBlock.lang.Relations 2

            The inj relation variable.

            Equations
            Instances For
              source
              def DescriptiveComplexity.kCliqueRel :
              cliqueGuessBlock.lang.Relations 1

              The clique relation variable.

              Equations
              Instances For
                source
                @[reducible, inline]
                abbrev DescriptiveComplexity.kAdjSym :
                cliqueSOLang.Relations 2

                The adj symbol over the sum.

                Equations
                Instances For
                  source
                  def DescriptiveComplexity.cliqueGuessBlock :
                  SOBlock

                  The single existential block of the Σ₁ definition of Clique: a unary relation variable, the clique, and a binary one, an injection of the marked set into the clique.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[instance_reducible]
                    instance DescriptiveComplexity.instDecidableEqCliqueGuessBlockIx :
                    DecidableEq CliqueGuessBlockIx
                    Equations
                    source
                    noncomputable def DescriptiveComplexity.cliqueKernel :
                    cliqueSOLang.Sentence

                    The first-order kernel of the Σ₁ definition of Clique: the guessed unary relation is a clique – any two distinct members are adjacent – and the guessed binary relation maps every marked element to some clique member, injectively.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      theorem DescriptiveComplexity.clique_sigmaSODefinable :
                      SigmaSODefinable 1 Clique

                      Clique is Σ₁-definable: existentially guess the clique and an injection of the marked set into it, then check both first-order. Since NP is defined as Σ₁-definability, this is the membership half of the NP-completeness of Clique.