Completeness for a degree is mutual reducibility
Lax604544.DegreeOfAProblem · concepts/Lax604544/DegreeOfAProblem.lean · lax-604544
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Every problem is complete for its own degree. A problem is complete for the degree of if and only if reduces to by an ordered first-order reduction and reduces to by a relativized ordered first-order reduction. And two problems that reduce to each other by ordered first-order reductions have the same degree.
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: Completeness for a degree is mutual reducibility |
| 24 | type: theorem |
| 25 | --- |
| 26 | Every problem is complete for its own degree. A problem is |
| 27 | complete for the degree of if and only if reduces to by an |
| 28 | ordered first-order reduction and reduces to by a relativized |
| 29 | ordered first-order reduction. And two problems that reduce to each other |
| 30 | by ordered first-order reductions have the same degree. |
| 31 | -/ |
| 32 | |
| 33 | namespace Lax604544.DegreeOfAProblem |
| 34 | |
| 35 | open FirstOrder FirstOrder.Language |
| 36 | open Lax904597.Problems Lax904597.Interpretations Lax904597.Relativized Lax904597.Classes |
| 37 | open Lax904597.Sat Lax799700.SubgraphIso |
| 38 | open Lax485149.Problems Lax485149.TwoSat Lax485149.ClassNL Lax535992.HornSat Lax535992.ClassPTIME |
| 39 | open Lax564036.Hierarchy Lax564036.Tautology Lax624099.ClassRE Lax624099.FiniteSatisfiability |
| 40 | open Lax604544.Degrees Lax604544.RelationIsomorphism |
| 41 | open Lax604544.GraphIsomorphism Lax604544.DagIsomorphism |
| 42 | |
| 43 | /-- A problem is complete for its own degree. -/ |
| 44 | axiom below_complete_self : ∀ {L₀ : Language.{0, 0}} [L₀.IsRelational] (Q₀ : DecisionProblem L₀), |
| 45 | (below Q₀).Complete Q₀ |
| 46 | |
| 47 | /-- Completeness for the degree of `Q₀` is mutual reducibility with `Q₀`. -/ |
| 48 | axiom complete_below_iff : |
| 49 | ∀ {L₀ : Language.{0, 0}} [L₀.IsRelational] {L : Language.{0, 0}} [L.IsRelational] |
| 50 | {Q₀ : DecisionProblem L₀} (P : DecisionProblem L), |
| 51 | (below Q₀).Complete P ↔ |
| 52 | Nonempty (OrderedFOReduction P Q₀) ∧ Nonempty (RelOrderedFOReduction Q₀ P) |
| 53 | |
| 54 | /-- Mutually reducible problems have the same degree. -/ |
| 55 | axiom below_congr : |
| 56 | ∀ {L₀ : Language.{0, 0}} [L₀.IsRelational] {L₁ : Language.{0, 0}} [L₁.IsRelational] |
| 57 | {Q₀ : DecisionProblem L₀} {Q₁ : DecisionProblem L₁}, |
| 58 | Nonempty (OrderedFOReduction Q₀ Q₁) → Nonempty (OrderedFOReduction Q₁ Q₀) → below Q₀ = below Q₁ |
| 59 | |
| 60 | end Lax604544.DegreeOfAProblem |
| 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