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 partial function is partial recursive if and only if it is Turing computable

Statement

Let f:NN be a partial function, with inputs and outputs encoded by their canonical binary numerals. Then f is partial recursive if and only if f is Turing computable under those encodings.

Facts & Assumptions

Given: A partial function f:NN.

[L1]

A machine computes a partial function when it halts with the required encoded output on the domain and diverges off the domain, by Partial functions computed by a machine under fixed encodings.

[L2]

Partial recursive functions are closed under composition and unbounded minimization and contain the primitive recursive functions, by Unbounded minimization and partial recursive functions.

[L3]

Every partial recursive function has a normal-form expression f(x)=U(μsτT(e,x,s)) for some code e, by Kleene normal form for partial recursive functions.

[L5]

The predicate T, its primitive-recursive numeric zero-test τT, and the function U encode halting computation histories and their outputs arithmetically, by Kleene's T-predicate and output function.

Proof

technique · direct
1.1

Assume first that f is partial recursive. By [L3], choose e with f(x)=U(μsτT(e,x,s)) whenever f(x) is defined. Every primitive-recursive function is Turing computable: the initial functions have immediate machines, machine composition realizes composition, and a finite loop realizes primitive recursion. Hence machines compute the primitive-recursive functions τT and U from [L5]. A machine can therefore search successively through s=0,1,2,, evaluate τT(e,x,s), and at the first zero compute U(s) and halt with its binary numeral. If there is no successful s, the search continues forever. By [L1], this machine computes f.

L1L3L5givenconstruct
1.2

Conversely, assume that f is Turing computable. Then by [L1] there is a machine code e whose halting computations on input x produce exactly the values of f(x). By [L5], the characteristic function of the relation T(e,x,s) is primitive recursive, so the total search function ge(x,s) that returns 0 exactly when T(e,x,s) holds and 1 otherwise is primitive recursive. By [L2], the partial search me(x):=μsge(x,s) is therefore partial recursive, and composing with the primitive recursive output map U shows that xU(me(x)) is partial recursive as well. Its domain and values agree with f because me(x) exists exactly when the machine coded by e has a halting history on x, and then [L5] says that U(me(x)) is exactly the machine's output. Hence f is partial recursive.

L1L2L5givenconstruct
2.1

Steps 1.1 and 1.2 prove both implications, so f is partial recursive if and only if it is Turing computable.

step 1.1step 1.2

Depends on

Used by

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