On the Semantics of Intensionality

TL;DR

This paper develops a categorical framework for understanding intensionality using P-categories and introduces exposures as a new construct to unify various logical and computational devices.

Contribution

It introduces the concept of exposures within P-categories, providing a new algebraic approach to model intensionality in logic and computer science.

Findings

Exposures nearly preserve functorial structure but do not preserve PERs.

The framework unifies classic results of Kleene, G"odel, Tarski, and Rice.

Demonstrates that intensional devices like G"odel numberings can be modeled as exposures.

Abstract

In this paper we propose a categorical theory of intensionality. We first revisit the notion of intensionality, and discuss we its relevance to logic and computer science. It turns out that 1-category theory is not the most appropriate vehicle for studying the interplay of extension and intension. We are thus led to consider the P-categories of \v{C}ubri\'{c}, Dybjer and Scott, which are categories only up to a partial equivalence relation (PER). In this setting, we introduce a new P-categorical construct, that of exposures. Exposures are very nearly functors, except that they do not preserve the PERs of the P-category. Inspired by the categorical semantics of modal logic, we begin to develop their theory. Our leading examples demonstrate that an exposure is an abstraction of well-behaved intensional devices, such as G\"odel numberings. The outcome is a unifying framework in which classic results of Kleene, G\"odel, Tarski and Rice find concise, clear formulations, and where each logical device or assumption involved in their proofs can be expressed in the same algebraic manner.