We prove a generalization of Alex Heller's existence theorem for recursion categories; this generalization was suggested by work of Di Paola and Montagna on syntactic P-recursion categories arising from consistent extensions of Peano Arithmetic, and by the examples of recursion categories of coalgebras. Let B=BX be a uniformly generated isotypical B#-subcategory of an iteration category C, where X is an isotypical object of C. We give calculations for the existence of a weak Turing morphism in the Turing completion Tur of (...) B when C is separated; i.e., when connected domains in C are jointly epimorphic. Our proof generalizes as follows. Let D be a separated iteration category and let L : C → D be an iteration functor; i.e., a functor which preserves domains, coproducts, zero morphisms and the iteration operator; it is crucial for the generalization that an iteration functor need not preserve products. If L is faithful, then Tur is a recursion category. (shrink)

The purpose of this note is to observe a generalization of the concept "computable in..." to arbitrary partial combinatory algebras. For every partial combinatory algebra (pca) A and every partial endofunction on A, a pca A[f] is constructed such that in A[f], the function f is representable by an element; a universal property of the construction is formulated in terms of Longley's 2-category of pcas and decidable applicative morphisms. It is proved that there is always a geometric inclusion from the (...) realizability topos on A[f] into the one on A and that there is a meaningful preorder on the partial endofunctions on A which generalizes Turing reducibility. (shrink)

Dominical categories are categories in which the notions of partial morphisms and their domains become explicit, with the latter being endomorphisms rather than subobjects of their sources. These categories form the basis for a novel abstract formulation of recursion theory, to which the present paper is devoted. The abstractness has of course its usual concomitant advantage of generality: it is interesting to see that many of the fundamental results of recursion theory remain valid in contexts far removed from their classic (...) manifestations. A principal reason for introducing this new formulation is to achieve an algebraization of the generalized incompleteness theorem, by providing a category-theoretic development of the concepts and tools of elementary recursion theory that are inherent in demonstrating the theorem.Dominical recursion theory avoids the commitment to sets and partial functions which is characteristic of other formulations, and thus allows for an intrinsic recursion theory within such structures as polyadic algebras. It is worthy of notice that much of elementary recursion theory can be developedwithout referencetoelements.By Gödel's generalized incompleteness theorem for consistent arithmetical systemTwe mean any statement of the following sort: if every recursive set is definable inT, thenTis essentially undecidable [41]; or if all recursive functions are definable inT, thenTis essentially undecidable [41]; or if every recursive set is definable inT, thenT0andR0 are recursively inseparable [39]; or if all re sets are representable inT, thenT0is creative [28], [39]; or ifTis a Rosser theory, thenT0andR0are effectively inseparable [39]. (shrink)

In this book the authors reconcile two different viewpoints of the foundations of mathematics, namely mathematical logic and category theory. In Part I, they show that typed lambda-calculi, a formulation of higher order logic, and cartesian closed categories are essentially the same. In Part II, it is demonstrated that another formulation of higher order logic is closely related to topos theory. Part III is devoted to recursive functions. Numerous applications of the close relationship between traditional logic and the algebraic language (...) of category theory are given. The authors have included an introduction to category theory and develop the necessary logic as required, making the book essentially self-contained. Detailed historical references are provided throughout, and each section concludes with a set of exercises. Thus it is well-suited for graduate courses and research in mathematics and logic. Researchers in theoretical computer science, artificial intelligence and mathematical linguistics will also find this an accessible introduction to a subject of increasing application to these disciplines. (shrink)

The classical forms of both modified realizability and relative realizability are naturally described in terms of the Sierpinski topos. The paper puts these two observations together and explains abstractly the existence of the geometric morphisms and logical functors connecting the various toposes at issue. This is done by advancing the theory of triposes over internal partial combinatory algebras and by employing a novel notion of elementary map.

This work is a step toward the development of a logic for types and computation that includes not only the usual spaces of mathematics and constructions, but also spaces from logic and domain theory. Using realizability, we investigate a configuration of three toposes that we regard as describing a notion of relative computability. Attention is focussed on a certain local map of toposes, which we first study axiomatically, and then by deriving a modal calculus as its internal logic. The resulting (...) framework is intended as a setting for the logical and categorical study of relative computability. (shrink)