TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-12

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The modified Post correspondence problem is undecidable

Statement

The modified Post correspondence problem is undecidable.

Facts & Assumptions

Given: The language of modified-PCP instances with a match.

[L1]

From every machine-input pair $(M, w)$ one can compute a modified-PCP instance $P_{M, w}$ such that $P_{M, w}$ has a match if and only if $M$ accepts $w$ , by Accepting computation histories can be encoded by modified-PCP domino matches.

[L2]

The Turing-machine acceptance problem is undecidable, by The Turing-machine acceptance problem is undecidable.

[L3]

If $A \leq_{m} B$ and $B$ is decidable, then $A$ is decidable, by Computable many-one reductions transfer decidability and recognizability backward.

Proof

technique · direct

1.1

Define a map $f$ on coded machine-input pairs by $f (⟨ M, w ⟩) : = P_{M, w} .$ By [L1], this map is total and computable and satisfies $⟨ M, w ⟩ \in A_{T M} ⟺ f (⟨ M, w ⟩) \in MPCP .$ Thus $A_{T M} \leq_{m} MPCP$ .

L1givenconstruct

2.1

If modified PCP were decidable, then [L3] and step 1.1 would imply that $A_{T M}$ is decidable. This contradicts [L2].

L2L3step 1.1contradiction

3.1

Therefore modified PCP is undecidable.

step 2.1discharge-contradiction: a decider for modified PCP would decide $A_{TM}$∎

Depends on

Used by

Dependency tree · two levels

12 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

MIT OpenCourseWare, Lecture 10: Computation History Method (standard reference, not scraped)
John Watrous, Introduction to the Theory of Computing (standard reference, not scraped)