From proofs to residuated categories

This work addresses the identity of proofs problem, which asks when two proofs represent the same argument. Closely related questions arise across disciplines: in computer science, when two algorithms represent the same program, and in mathematics, when two structures are essentially the same. Category theory, a general framework for studying mathematical structures and their relationships, provides a unifying setting for these questions. Through the Curry–Howard correspondence, proofs, programs, and categorical structures can be understood as fundamentally equivalent, allowing these issues to be studied in a common mathematical language. Understanding proof identity has broad applications, including modeling reasoning, language, and resource-sensitive interaction in multiagent systems, where agents coordinate actions and manage shared resources. This motivates the development of general and modular mathematical foundations for analyzing when proofs should be considered the same. To this end, we introduce labelled proper display calculi whose natural semantics are given by residuated categories, and we establish a general cut-elimination result. We then construct the free category generated by such a calculus, in which formulas serve as objects and equivalence classes of proofs as morphisms. This construction ensures that proof equivalence behaves as a categorical congruence, that logical rules correspond to natural and functorial operations, and that structural rules give rise to adjunctions; moreover, the resulting structure is shown to be residuated. We further develop a normalization procedure for proofs, proving that it terminates and yields unique normal forms. This induces a category, called the Prawitz–Lambek category, whose morphisms arise from normalization equivalence. We show that this category is equivalent to the previously constructed free category, thereby linking syntactic normalization and categorical structure. Finally, we introduce an algorithm that translates proofs into diagrammatic representations, providing a new way to visualize proof structures. We conjecture that this approach generalizes to a wide class of displayable logics and that recent advances in algebraic proof theory and correspondence theory can be lifted to the categorical level, enabling systematic treatment of axiomatic extensions.