The classes with a complete problem are degrees
Lax604544.ClassesAsDegrees · concepts/Lax604544/ClassesAsDegrees.lean · lax-604544
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Each logically defined class with a complete problem is the degree of that problem: NP is the degree of SAT, coNP of TAUT, PTIME of HORN-SAT, NL of 2SAT and RE of FINSAT. Every member of the class reduces to the problem by an ordered first-order reduction, the generic reduction that reads a definition, and the class is closed under such reductions. Hardness for a complete problem is therefore hardness for the class: SAT-hardness is NP-hardness.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax904597.Problems |
| 2 | import Lax904597.Interpretations |
| 3 | import Lax904597.Relativized |
| 4 | import Lax904597.Classes |
| 5 | import Lax904597.Sat |
| 6 | import Lax799700.SubgraphIso |
| 7 | import Lax485149.Problems |
| 8 | import Lax485149.TwoSat |
| 9 | import Lax485149.ClassNL |
| 10 | import Lax535992.HornSat |
| 11 | import Lax535992.ClassPTIME |
| 12 | import Lax564036.Hierarchy |
| 13 | import Lax564036.Tautology |
| 14 | import Lax624099.ClassRE |
| 15 | import Lax624099.FiniteSatisfiability |
| 16 | import Lax604544.Degrees |
| 17 | import Lax604544.RelationIsomorphism |
| 18 | import Lax604544.GraphIsomorphism |
| 19 | import Lax604544.DagIsomorphism |
| 20 | |
| 21 | /-! |
| 22 | --- |
| 23 | title: The classes with a complete problem are degrees |
| 24 | type: theorem |
| 25 | --- |
| 26 | Each logically defined class with a complete problem is the degree of that |
| 27 | problem: NP is the degree of SAT, coNP of TAUT, PTIME of HORN-SAT, NL of |
| 28 | 2SAT and RE of FINSAT. Every member of the class reduces to the problem by |
| 29 | an ordered first-order reduction, the generic reduction that reads a |
| 30 | definition, and the class is closed under such reductions. Hardness for a |
| 31 | complete problem is therefore hardness for the class: SAT-hardness is |
| 32 | NP-hardness. |
| 33 | -/ |
| 34 | |
| 35 | namespace Lax604544.ClassesAsDegrees |
| 36 | |
| 37 | open FirstOrder FirstOrder.Language |
| 38 | open Lax904597.Problems Lax904597.Interpretations Lax904597.Relativized Lax904597.Classes |
| 39 | open Lax904597.Sat Lax799700.SubgraphIso |
| 40 | open Lax485149.Problems Lax485149.TwoSat Lax485149.ClassNL Lax535992.HornSat Lax535992.ClassPTIME |
| 41 | open Lax564036.Hierarchy Lax564036.Tautology Lax624099.ClassRE Lax624099.FiniteSatisfiability |
| 42 | open Lax604544.Degrees Lax604544.RelationIsomorphism |
| 43 | open Lax604544.GraphIsomorphism Lax604544.DagIsomorphism |
| 44 | |
| 45 | /-- NP is the degree of SAT. -/ |
| 46 | axiom NP_eq_below_sat : NP = below SAT |
| 47 | |
| 48 | /-- coNP is the degree of TAUT. -/ |
| 49 | axiom coNP_eq_below_taut : coNP = below TAUT |
| 50 | |
| 51 | /-- PTIME is the degree of HORN-SAT. -/ |
| 52 | axiom PTIME_eq_below_hornSat : PTIME = below HORNSAT |
| 53 | |
| 54 | /-- NL is the degree of 2SAT. -/ |
| 55 | axiom NL_eq_below_twoSat : NL = below TwoSAT |
| 56 | |
| 57 | /-- RE is the degree of FINSAT. -/ |
| 58 | axiom RE_eq_below_finsat : RE = below FINSAT |
| 59 | |
| 60 | end Lax604544.ClassesAsDegrees |
| 61 |
Builds on
Lax485149.ClassNLLax485149.ProblemsLax485149.TwoSatLax535992.ClassPTIMELax535992.HornSatLax564036.HierarchyLax564036.TautologyLax604544.DagIsomorphismLax604544.DegreesLax604544.GraphIsomorphismLax604544.RelationIsomorphismLax624099.ClassRELax624099.FiniteSatisfiabilityLax799700.SubgraphIsoLax904597.ClassesLax904597.InterpretationsLax904597.ProblemsLax904597.RelativizedLax904597.Sat
Used by
none
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments