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.
Every computably enumerable set is the domain of a partial computable function
Statement
Let be a computably enumerable subset of an effectively encoded set . Then there exists a partial computable function whose domain is exactly .
Facts & Assumptions
Given: A c.e. set .
By Computably enumerable sets and languages, either or there exists a total computable enumerator with range .
By Computable and partial computable functions, a partial computable function is one produced by a machine that halts exactly on its domain.
Proof
If , take the nowhere-defined partial function from to the one-point set . Its machine diverges on every input, so [L2] shows that its domain is exactly .
Suppose now that , and let be the total computable enumerator from [L1]. Define a machine on an input code that computes the outputs one after another until it first sees the codeword , at which point it halts and outputs . If with , some index satisfies , so the machine eventually halts on . If , no enumerated value has code , so the machine never halts on . Thus [L2] gives a partial computable function whose domain is exactly .
In either case, is the domain of a partial computable function.
Depends on
Used by
Nothing in the library uses this result yet.
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)
- John Watrous, Introduction to the Theory of Computing, Lecture 18: Further discussion of computability (standard reference, not scraped)