Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

FO(≤) ⊊ FO(DTC): EVEN is a deterministic walk

Lax945089.FirstOrderBelowTransitiveClosure · concepts/Lax945089/FirstOrderBelowTransitiveClosure.lean · lax-945089

proven

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

    Theorem

    EVEN is FO(DTC) definable, hence FO(TC) definable, in NL and in PTIME: one deterministic walk along the order, stepping to the successor and flipping a bit, decides the parity of the universe. Since EVEN is not FO(≤\le) definable, the inclusion of FO(≤\le) in FO(TC) is strict, with no complexity-theoretic assumption.

    Concept map
    27 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 5 statements. Each proof establishes one of them relative to its assumptions.

    1 even_dtcDefinable proven

    2 even_mem_NL proven

    3 even_mem_PTIME proven

    4 even_tcDefinable proven

    5 exists_tcDefinable_not_foDefinable proven

    Lean source view on GitHub

    1import Mathlib.ModelTheory.Order
    2import Mathlib.Order.Defs.LinearOrder
    3import Lax904597.Problems
    4import Lax904597.Interpretations
    5import Lax904597.Relativized
    6import Lax904597.SecondOrder
    7import Lax904597.Classes
    8import Lax485149.Problems
    9import Lax485149.FirstOrderDefinability
    10import Lax485149.TransitiveClosure
    11import Lax485149.DeterministicTransitiveClosure
    12import Lax485149.ClassNL
    13import Lax485149.ClassL
    14import Lax535992.InflationaryFixedPoint
    15import Lax535992.ClassPTIME
    16import Lax134656.PartialFixedPoint
    17import Lax895169.ArithmeticLogic
    18import Lax945089.OrderFreeFirstOrder
    19import Lax945089.EhrenfeuchtGames
    20import Lax945089.PebbleGames
    21import Lax945089.Even
    22import Lax945089.Parity
    23import Lax945089.TransitiveClosureReductions
    24
    25/-!
    26---
    27title: FO(≤) ⊊ FO(DTC): EVEN is a deterministic walk
    28type: theorem
    29---
    30EVEN is FO(DTC) definable, hence FO(TC) definable, in NL and in PTIME: one
    31deterministic walk along the order, stepping to the successor and flipping
    32a bit, decides the parity of the universe. Since EVEN is not FO(≤\le)
    33definable, the inclusion of FO(≤\le) in FO(TC) is strict, with no
    34complexity-theoretic assumption.
    35-/
    36
    37namespace Lax945089.FirstOrderBelowTransitiveClosure
    38
    39open FirstOrder FirstOrder.Language
    40open Lax904597.Problems Lax904597.Interpretations Lax904597.Relativized Lax904597.SecondOrder
    41open Lax904597.Classes
    42open Lax485149.Problems Lax485149.FirstOrderDefinability Lax485149.TransitiveClosure
    43open Lax485149.DeterministicTransitiveClosure Lax485149.ClassNL Lax485149.ClassL
    44open Lax535992.InflationaryFixedPoint Lax535992.ClassPTIME
    45open Lax134656.PartialFixedPoint Lax895169.ArithmeticLogic
    46open Lax945089.OrderFreeFirstOrder Lax945089.EhrenfeuchtGames Lax945089.PebbleGames
    47open Lax945089.Even Lax945089.Parity
    48open Lax945089.TransitiveClosureReductions
    49
    50/-- EVEN is FO(DTC) definable. -/
    51axiom even_dtcDefinable : DTCDefinable EVEN
    52
    53/-- EVEN is FO(TC) definable. -/
    54axiom even_tcDefinable : TCDefinable EVEN
    55
    56/-- EVEN is in NL. -/
    57axiom even_mem_NL : NL.Mem EVEN
    58
    59/-- EVEN is in PTIME. -/
    60axiom even_mem_PTIME : PTIME.Mem EVEN
    61
    62/-- Some FO(TC) definable problem is not FO(≤) definable. -/
    63axiom exists_tcDefinable_not_foDefinable :
    64 ∃ P : DecisionProblem Language.empty, TCDefinable P ∧ ¬FODefinable P
    65
    66end Lax945089.FirstOrderBelowTransitiveClosure
    67
    Show ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…