TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30

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.

Eliminating useless symbols preserves the generated language

Statement

For every context-free grammar $G$ there exists a context-free grammar $G^{'}$ such that $L (G^{'}) = L (G)$ and either:

$L (G) = \emptyset$ and $G^{'}$ is the evident empty-language grammar, or
every variable of $G^{'}$ is both generating and reachable.

Facts & Assumptions

Given: A context-free grammar $G = (V, Σ, P, S)$ .

[L1]

Variables may be nullable, generating, reachable, or useful exactly as in Nullable, generating, and reachable variables.

[L2]

The generated language is $L (G) = {w \in Σ^{*} : S \Rightarrow_{G}^{*} w}$ , by The language generated by a CFG.

Proof

technique · direct

1.1

Let $T \subseteq V$ be the generating variables of $G$ , and let $P_{1}$ consist of the productions whose left-hand side lies in $T$ and whose right-hand side contains no variable outside $T$ . If $S \notin T$ , then no terminal word is derivable from $S$ , so [L2] gives $L (G) = \emptyset$ and we may take $G^{'}$ to be any fixed grammar generating the empty language. If $S \in T$ , set $G_{1} : = (T, Σ, P_{1}, S)$ .

L1L2givenconstruct

1.2

In the case $S \in T$ , let $R \subseteq T$ be the variables reachable from $S$ in $G_{1}$ , let $P_{2}$ consist of the productions in $P_{1}$ whose left-hand side lies in $R$ and whose right-hand side contains no variable outside $R$ , and set $G_{2} : = (R, Σ, P_{2}, S)$ . Every derivation beginning at $S$ stays inside $R$ by definition of reachability.

L1givenconstruct

2.1

Assume now that $S \in T$ . Any derivation of a terminal word can use only generating variables, because every variable appearing in that derivation must eventually derive a terminal subword. Conversely, every rule kept in $G_{1}$ was already a rule of $G$ . Hence $L (G_{1}) = L (G)$ .

L1L2step 1.1

3.1

Therefore deleting the unreachable variables changes no derivation from $S$ to a terminal word, while every variable remaining in $G_{2}$ is both generating and reachable. So $L (G_{2}) = L (G_{1}) = L (G)$ .

step 2.1step 1.2

4.1

Taking $G^{'} = G_{2}$ in the case $S \in T$ and the empty-language grammar in the case $S \notin T$ proves the theorem.

step 1.1step 3.1∎

Depends on

Used by

Dependency tree · two levels

4 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

Jean Gallier and Jocelyn Quaintance, Introduction to the Theory of Computation: Some Notes for CIS511 (standard reference, not scraped)