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.

A binary language is recognizable if and only if it is computably enumerable

Statement

For every language L⊆{0,1}∗, the following are equivalent, where computable enumerability is taken with respect to the identity encoding of binary words:

  1. L is recognizable.
  2. L is computably enumerable.

Facts & Assumptions

Given: A language L⊆{0,1}∗.

[L1]

By Decidable and recognizable languages, recognizability means that some Turing machine accepts exactly the words of L and may diverge on nonmembers.

[L2]

By Computably enumerable sets and languages, computable enumerability means either L=∅ or L is the range of a total computable function.

Proof

technique · direct
1.1L1L2given

Assume first that L is c.e. If L=∅, then the machine that immediately rejects every input recognizes L. Otherwise choose a total computable enumerator e:N→{0,1}∗ with range L as in [L2]. On input x, search through n=0,1,2,… and compute e(n) until e(n)=x; if this occurs, accept. For x∈L the search eventually finds a witness n, and for x∉L it never accepts. Thus L is recognizable by [L1].

1.2L1L2choose

Assume conversely that L is recognizable. If L=∅, then [L2] already says that L is c.e. So assume L≠∅, and let M be a recognizer for L. By dovetailing the simulations of M over binary words in shortlex order, fix one accepted word a0∈L.

2.1L2step 1.2construct

Fix a standard total computable bijection n↦(i,t) from N onto N×N, and let wi be the ith binary word in shortlex order. Define e(n):={wi,if M accepts wi within t steps,a0,otherwise. This is a total computable function N→{0,1}∗. Every output of e lies in L, and if w∈L then w=wi for some i and M accepts wi in some finite number of steps t, so e(n)=w for the paired input with coordinates (i,t). Hence the range of e is exactly L, so [L2] shows that L is c.e.

3.1step 1.1step 2.1∎

Steps 1.1 and 2.1 prove the equivalence.

Depends on

Used by

Dependency tree · two levels

5 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