Alphabeta Math
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 inclusions in the language-class ladder are proper

Statement

For every fixed finite alphabet Σ with at least two symbols, the containments in The regular, context-free, decidable, and recognizable language-class ladder are all strict: regularcontext-freedecidablecomputably enumerable.

Facts & Assumptions

Given: The classes from The regular, context-free, decidable, and recognizable language-class ladder over a finite alphabet Σ containing distinct symbols a,b.

[L1]

Every regular language satisfies the pumping property from The pumping lemma for regular languages.

[L2]

Membership in a context-free language is decidable, by Context-free-language membership is decidable.

[L3]

Every context-free language satisfies the pumping property from The pumping lemma for context-free languages.

Proof

technique · direct
1.1

If a language is regular, choose a DFA D recognizing it. Make one CFG whose variables are the states of D, whose start variable is the start state, whose productions are qaδ(q,a) for each transition, and whose accepting states also have productions qε. Then the grammar generates exactly the words accepted by D. Hence every regular language is context-free.

givenconstruct
1.2

Every decidable language is recognizable by running its decider and accepting exactly when the decider accepts. Thus decidablecomputably enumerable.

givenconstruct
2.1

The language Lab:={anbn:n0} is context-free, for example via the grammar SaSbε. It is not regular: if it were regular, [L1] would give a pumping length p, but apbp cannot be pumped inside the first p symbols without changing the number of a's and leaving the number of b's fixed. Therefore regularcontext-free.

L1step 1.1
2.2

Relabel the binary alphabet of ATM injectively by the two chosen symbols a,bΣ. This computable letter-by-letter bijection preserves recognizability and decidability. By [L5] and [L6], the relabeled language over Σ is computably enumerable but not decidable. Therefore decidablecomputably enumerable.

L5L6step 1.2construct
3.1

Every context-free language is decidable by [L2], so context-freedecidable.

L2step 2.1
4.1

The language Laba:={anbnan:n0} is decidable by checking the three blocks and comparing their lengths. It is not context-free: if p were a pumping length from [L3], then a pumping window of length at most p in apbpap could meet at most two consecutive blocks and could not meet both a-blocks. Pumping a nonempty part therefore changes at least one of the three required counts without changing all three equally, or destroys the block order. This contradicts [L3]. Hence context-freedecidable.

L3step 3.1algebra
5.1

Steps 2.1, 4.1, and 2.2 prove that all three containments are strict over the fixed alphabet Σ.

step 2.1step 4.1step 2.2

Depends on

Used by

Dependency tree · two levels

25 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