Lax Lean Archive

The Post correspondence problem is undecidable

Lax251941.PostCorrespondenceUndecidable · 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.

    Natural Language Statement

    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).

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

    Each proof establishes this claim relative to its assumptions.

    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

    Discussion

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

    Loading discussion…