On the semantics of intensionality and intensional recursion

Intensionality is a phenomenon that occurs in logic and computation. In the most general sense, a function is intensional if it operates at a level finer than (extensional) equality. This is a familiar setting for computer scientists, who often study different programs or processes that are interchangeable, i.e. extensionally equal, even though they are not implemented in the same way, so intensionally distinct. Concomitant with intensionality is the phenomenon of intensional recursion, which refers to the ability of a program to have access to its own code. In computability theory, intensional recursion is enabled by Kleene’s Second Recursion Theorem. This thesis is concerned with the crafting of a logical toolkit through which these phenomena can be studied. Our main contribution is a framework in which mathematical and computational constructions can be considered either extensionally, i.e. as abstract values, or intensionally, i.e. as fine-grained descriptions of their construction. Once this is achieved, it may be used to analyse intensional recursion. To begin, we turn to type theory. We construct a modal λ-calculus, called Intensional PCF, which supports non-functional operations at modal types. Moreover, by adding Löb's rule from provability logic to the calculus, we obtain a type-theoretic interpretation of intensional recursion. The combination of these two features is shown to be consistent through a confluence argument. Following that, we begin searching for a semantics for Intensional PCF. We argue that 1-category theory is not sufficient, and propose the use of P-categories instead. On top of this setting we introduce exposures, which are P-categorical structures that function as abstractions of well-behaved intensional devices. We produce three examples of these structures, based on Gödel numberings on Peano arithmetic, realizability theory, and homological algebra. The language of exposures leads us to a P-categorical analysis of intensional recursion, through the notion of intensional fixed points. This, in turn, leads to abstract analogues of classic intensional results in logic and computability, such as Gödel's Incompleteness Theorem, Tarski's Undefinability Theorem, and Rice's Theorem. We are thus led to the conclusion that exposures are a useful framework, which we propose as a solid basis for a theory of intensionality. In the final chapters of the thesis we employ exposures to endow Intensional PCF with an appropriate semantics. It transpires that, when interpreted in the P-category of assemblies on the PCA K1, the Löb rule can be interpreted as the type of Kleene’s Second Recursion Theorem.