It states that when a semi-decidable property of partial computable functions is true on a certain partial function, one can extract a finite subfunction such that the property is still true.
Then for any partial computable function f, it holds that P contains f if and only if P contains a finite subfunction of f (i.e., a partial function defined in finitely many points, which takes the same values as f on those points).
Then for any total computable function f, there exists n such that for all total computable function g which agrees with f until n, f ∈ P ⟺ g ∈ P. The two theorems are closely related, and also relate to Rice's theorem.
Specifically: By the Rice-Shapiro theorem, it is neither semi-decidable nor co-semi-decidable whether a given program: By the Kreisel-Lacombe-Shoenfield-Tseitin theorem, it is undecidable whether a given program which is assumed to always terminate: Let P be a set of partial computable functions with semi-decidable index set.
Next, we prove that if P contains a partial computable function f, then it contains a finite subfunction of f. Let us fix a partial computable function f in P. We build a program p which takes input x and runs the following steps: Suppose that φp ∉ P. This implies that the semi-algorithm for semi-deciding P used in the first step never returns true.
Then, p computes f, and this contradicts the assumption f ∈ P. Thus, we must have φp ∈ P, and the algorithm for semi-deciding P returns true on p after a certain number of steps n. The partial function φp can only be defined on inputs x such that x ≤ n, and it returns f(x) on such inputs, thus it is a finite subfunction of f that belongs to P. It only remains to assemble the two parts of the proof.
is said to be ultimately zero if it always takes the value zero except for a finite number of points, i.e., there exists N such that for all n ≥ N, h(n) = 0.
We fix U a computable enumeration of all total functions which are ultimately zero, that is, U is such that: We can build U by standard techniques (e.g., for increasing N, enumerate ultimately zero functions which are bounded by N and zero on inputs larger than N).
Let P be as in the statement of the theorem: a set of total computable functions such that there is an algorithm which, given an index e and a promise that φe is computable, decides whether φe ∈ P. We first prove a lemma: For all total computable function f, and for all integer N, there exists an ultimately zero function h such that h agrees with f until N, and f ∈ P ⟺ h ∈ P. To prove this lemma, fix a total computable function f and an integer N, and let B be the boolean f ∈ P. Build a program p which takes input x and takes these steps: Clearly, p always terminates, i.e., φp is total.
Again, fix P as in the theorem statement, let f a total computable function and let B be the boolean "f ∈ P".
Let n be the number of steps that P takes to return B on p. We claim that n satisfies the conclusion of the theorem: for all total computable function g which agrees with f until n, it holds that f ∈ P ⟺ g ∈ P. Assume by contradiction that there exists g total computable which agrees with f until n and such that (g ∈ P) ≠ B.
Therefore, U(k) satisfies the conditions of the parallel search step in the program p, namely: U(k) agrees with f until n and (U(k) ∈ P) ≠ B.
Equip the set of all partial-recursive functions with the topology generated by these frusta as base.
The Kreisel-Lacombe-Shoenfield-Tseitin theorem has been applied to foundational problems in computational social choice (more broadly, algorithmic game theory).
For instance, Kumabe and Mihara[9][10] apply this result to an investigation of the Nakamura numbers for simple games in cooperative game theory and social choice theory.