Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 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.

CFG ambiguity is undecidable

Statement

The CFG ambiguity problem is undecidable.

Facts & Assumptions

Given: A PCP instance (u1,v1),…,(un,vn).

[L1]

A grammar is ambiguous exactly when some word in its language has two distinct leftmost derivations, by Ambiguous grammars, unambiguous grammars, and inherently ambiguous languages.

[L2]

A PCP match is a nonempty index sequence with equal top and bottom concatenations, by The Post correspondence problem.

[L4]

If A≤mB and B is decidable, then A is decidable, by Computable many-one reductions transfer decidability and recognizability backward.

Proof

technique · direct
1.1L2givenconstruct

Choose fresh terminal symbols ι1,…,ιn disjoint from the PCP alphabet, and build one grammar with start symbol S and two branches: S→T∣B, T→uiTιi∣uiιi,B→viBιi∣viιi(1≤i≤n). A leftmost derivation from T yields exactly the words ui1⋯uikιik⋯ιi1, and a derivation from B yields the analogous words with the vi. The fresh reversed suffix uniquely determines the entire index sequence, so each branch is unambiguous.

2.1L1L2step 1.1

If i1,…,ik is a PCP match, then the word ui1⋯uikιik⋯ιi1=vi1⋯vikιik⋯ιi1 has one leftmost derivation beginning with S⇒T and another beginning with S⇒B. Hence the grammar is ambiguous by [L1].

2.2L1L2step 1.1

Conversely, if the grammar is ambiguous, [L1] gives a word with two distinct leftmost derivations. Step 1.1 proves that neither the T branch nor the B branch has two derivations of one word, so one derivation begins with S⇒T and the other with S⇒B. The common terminal word has the form ui1⋯uikιik⋯ιi1=vj1⋯vjmιjm⋯ιj1. Freshness and unique parsing of the reversed suffix force k=m and ir=jr for every r, so i1,…,ik is a PCP match.

3.1L3L4step 2.1step 2.2contradiction

Steps 2.1 and 2.2 show that the constructed grammar is ambiguous if and only if the original PCP instance has a match. If CFG ambiguity were decidable, then [L4] and this equivalence would make PCP decidable, contradicting [L3].

4.1step 3.1discharge-contradiction: an ambiguity decider would decide PCP∎

Therefore CFG ambiguity is undecidable.

Depends on

Used by

Nothing in the library uses this result yet.

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