The modern theory of computability is based on the works of Church, Markov and Turing who, starting from quite different models of computation, arrived at the same class of computable functions. The purpose of this paper is the show how the main results of the Church-Markov-Turing theory of computable functions may quickly be derived and understood without recourse to the largely irrelevant theories of recursive functions, Markov algorithms, or Turing machines. We do this by ignoring the problem of what constitutes a computable function and concentrating on the central feature of the Church-Markov-Turing theory: that the set of computable partial functions can be effectively enumerated. In this manner we are led directly to the heart of the theory of computability without having to fuss about what a computable function is.

The spirit of this approach is similar to that of [RGRS]. A major difference is that we operate in the context of constructive mathematics in the sense of Bishop [BSH1], so all functions are computable by definition, and the phrase “you can find” implies “by a finite calculation.” In particular if P is some property, then the statement “for each m there is n such that P(m, n)” means that we can construct a (computable) function θ such that P(m, θ(m)) for all m. Church's thesis has a different flavor in an environment like this where the notion of a computable function is primitive.

One point of such a treatment of Church's thesis is to make available to Bishopstyle constructivists the Markovian counterexamples of Russian constructivism and recursive function theory. The lack of serious candidates for computable functions other than recursive functions makes it quite implausible that a Bishopstyle constructivist could refute Church's thesis, or any consequence of Church's thesis. Hence counterexamples such as Specker's bounded increasing sequence of rational numbers that is eventually bounded away from any given real number [SPEC] may be used, as Brouwerian counterexamples are, as evidence of the unprovability of certain assertions.

If C1, …, Ck are members of a certain class of suitable categories (which contains those arising from models with dimension), C = C1 × … × Ck, C′ is a suitable category, F: C → C′ is a partial recursive combinatorial functor satisfying a certain property (which, if C = C1, is that F is nonconstant) and ∈ C, then (1) if F is regressive so is as is each i, and (2) if F is Dedekind then each i is Dedekind.

Under a weak set-theoretic assumption we interpret second-order logic in the monadic theory of order.

A many-one degree is functional if it contains the index set of some class of partial recursive functions but does not contain an index set of a class of r.e. sets. We give a natural embedding of the r.e. m-degrees into the functional degrees of 0′. There are many functional degrees in 0′ in the sense that every partial-order can be embedded. By generalizing, we show there are many functional degrees in every complete Turing degree.

There is a natural tie between the studies of index sets and partial-many-one reducibility. Every partial-many-one degree contains one or two index sets.

The Sikorski Extension Theorem [6] states that, for any Boolean algebra A and any complete Boolean algebra B, any homomorphism of a subalgebra of A into B can be extended to the whole of A. That is,

Inj: Any complete Boolean algebra is injective (in the category of Boolean algebras).

The proof of Inj uses the axiom of choice (AC); thus the implication AC → Inj can be proved in Zermelo-Fraenkel set theory (ZF). On the other hand, the Boolean prime ideal theorem

BPI: Every Boolean algebra contains a prime ideal (or, equivalently, an ultrafilter)

may be equivalently stated as:

The two element Boolean algebra 2 is injective,

and so the implication Inj → BPI can be proved in ZF.

In [3], Luxemburg surmises that this last implication cannot be reversed in ZF. It is the main purpose of this paper to show that this surmise is correct. We shall do this by showing that Inj implies that BPI holds in every Boolean extension of the universe of sets, and then invoking a recent result of Monro [5] to the effect that BPI does not yield this conclusion.