Lax Lean Archive

The complement of a decision problem

Lax485149.Complement · concepts/Lax485149/Complement.lean · lax-485149

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    The complement PcP^c of a decision problem PP over a relational vocabulary has as yes-instances the structures that are no-instances of PP. It is a decision problem: a property and its negation are invariant under the same isomorphisms.

    Concept map
    2 concepts; 25 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax904597.Problems
    2
    3/-!
    4---
    5title: The complement of a decision problem
    6type: definition
    7---
    8The complement PcP^c of a decision problem PP over a relational vocabulary
    9has as yes-instances the structures that are no-instances of PP. It is a
    10decision problem: a property and its negation are invariant under the same
    11isomorphisms.
    12-/
    13
    14namespace Lax485149.Complement
    15
    16open Lax904597.Problems
    17
    18open FirstOrder
    19
    20open Language
    21
    22/-- The complement of a decision problem: its yes-instances are the
    23no-instances of `P`. -/
    24def DecisionProblem.compl {L : Language.{0, 0}} [L.IsRelational]
    25 (P : DecisionProblem L) :
    26 DecisionProblem L where
    27 Holds := fun A inst => ¬@DecisionProblem.Holds L _ P A inst
    28 iso_invariant := fun e => not_congr (P.iso_invariant e)
    29
    30end Lax485149.Complement
    31
    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…