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.
Myhill's isomorphism theorem for creative sets
Statement
Work with the fixed machine-coding acceptable numbering of The fixed machine coding gives an acceptable numbering. If are creative, then there exists a computable permutation of such that In particular, every creative set is computably isomorphic to the diagonal halting set .
Facts & Assumptions
Given: Creative sets .
A creative set is c.e. and has productive complement. For the fixed acceptable machine coding, the productive-function normalization recorded in Productive and creative sets permits a total computable one-one productive witness.
The diagonal halting set is creative, by The nonhalting set is productive and the halting set is creative.
The recursion theorem with parameters gives a uniform fixed-point map for total computable binary transformers, by The recursion theorem with parameters.
Proof
Every c.e. set one-one reduces to . If , let be the code of a machine that ignores its actual input, enumerates , and halts exactly when appears. Add to its finite description an unreachable chain of states whose length encodes . This does not change its behaviour, and the fixed injective machine coding makes total computable and one-one. Thus
Let be creative, put , and choose a normalized total one-one productive function from [L1]. The fixed coding supplies a total computable padding map : it builds a machine simulating program and adds an unreachable state chain encoding the pair . Hence , and is one-one in the pair. Apply [L3] to the transformer that, from , returns an index whose domain is if program halts on , and is empty otherwise. We obtain a total computable satisfying this fixed-point equation. Put Then , and therefore , is one-one, and padding gives If and , productivity applied to would force , a contradiction. If , then , so productivity gives . Therefore and is a one-one computable reduction .
Applying step 1.1 to and then step 1.2 to gives a one-one reduction by composition. Reversing the roles of and gives .
Let witness and let witness . Build finite membership-preserving partial bijections by stages. At a domain stage, choose the least and start with . While , set and . This search must leave the finite range: otherwise a repeated and injectivity of would eventually put the original unused in . Pair with the first unused . Each passage through and preserves and reflects membership, so the new pair does too.
At the alternating range stage, choose the least and start with . While , set and . The symmetric injectivity argument finds an unused after finitely many steps. Pair that with ; again all traversed maps preserve and reflect membership. Thus every stage effectively extends the finite membership-preserving partial bijection.
Let . The alternating least-unused choices put every natural number eventually into both its domain and range, so is a bijection. It is computable because, on input , one simulates stages until is paired. Every stage preserves , hence this equivalence holds for all .
So is a computable permutation sending onto . Taking and using [L2] gives the final clause.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
13 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
- Robert I. Soare, Turing Computability: Theory and Applications (standard reference, not scraped)