Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax251941.PostCorrespondenceUndecidable

The Post correspondence problem is undecidable

concepts/Lax251941/PostCorrespondenceUndecidable.lean · lax-251941

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    Theorem

    No algorithm decides whether an instance of the Post correspondence problem has a match (Post 1946; Sipser, Theorem 5.15). It follows from the reduction of the acceptance problem for Turing machines to the Post correspondence problem (PostCorrespondenceReductionPostCorrespondenceReduction) and the undecidability of that acceptance problem (TapeAcceptanceUndecidableTapeAcceptanceUndecidable).

    Lean source view on GitHub

    1import Mathlib.Computability.Halting
    2import Lax251941.PostCorrespondence
    3
    4/-!
    5---
    6title: The Post correspondence problem is undecidable
    7type: theorem
    8---
    9No algorithm decides whether an instance of the Post correspondence problem has
    10a match (Post 1946; Sipser, Theorem 5.15). It follows from the reduction of
    11the acceptance problem for Turing machines to the Post correspondence problem
    12(`PostCorrespondenceReduction`) and the undecidability of that acceptance
    13problem (`TapeAcceptanceUndecidable`).
    14
    15# Formalization notes
    16
    17Stated for instances over the alphabet `ℕ`, in the domino form `HasMatch`, with
    18mathlib's `ComputablePred`. The index form the book *Transducers* uses is
    19`PostCorrespondenceIndexUndecidable`.
    20-/
    21
    22namespace Lax251941.PostCorrespondenceUndecidable
    23
    24open Lax251941.PostCorrespondence
    25
    26/-- The Post correspondence problem over `ℕ` is undecidable. -/
    27axiom not_computablePred_hasMatch : ¬ ComputablePred fun P : Inst ℕ => HasMatch P
    28
    29end Lax251941.PostCorrespondenceUndecidable
    30
    Show Proof

    Formalization notes

    Stated for instances over the alphabet Nℕ, in the domino form HasMatchHasMatch, with mathlib's ComputablePredComputablePred. The index form the book Transducers uses is PostCorrespondenceIndexUndecidablePostCorrespondenceIndexUndecidable.

    Builds on

    Used by

    none

    From Mathlib

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…