Effective Operations of Type 2 in Pcas

TL;DR

This paper introduces a method to generate new partial combinatory algebras (pcas) by forcing a functional to be effective, generalizing Kleene's relative computability and enabling the study of subtoposes of the Effective Topos.

Contribution

It presents a novel construction for creating pcas relative to a fixed functional, extending the concept of computation and linking it to topos theory.

Findings

Generalizes Kleene's notion of computation relative to a functional

Provides a construction to study subtoposes of the Effective Topos

Shows equivalence of two common definitions of pcas

Abstract

We exhibit a way of "forcing a functional to be an effective operation" for arbitrary partial combinatory algebras (pcas). This gives a method of defining new pcas from old ones for some fixed functional, where the new partial functions can be viewed as computable relative to that functional. It is shown that this generalizes a notion of computation relative to a functional as defined by Kleene for the natural numbers. The construction can be used to study subtoposes of the Effective Topos. We will do this for a particular functional that forces every arithmetical set to be decidable. In this paper we also prove the convenient result that the two definitions of a pca that are common in the literature are essentially the same.