Intuitionistic First-Order Logic: Categorical Semantics via the Curry-Howard Isomorphism

TL;DR

This paper introduces a novel point-free categorical semantics for first-order intuitionistic logic, extending traditional models and providing a computational interpretation aligned with the Curry-Howard isomorphism.

Contribution

It presents a new sound and complete point-free semantics for first-order intuitionistic logic, unifying categorical and computational perspectives.

Findings

Semantics extends Heyting categories, topos theory, and Kripke models.

Provides a semantics for the lambda-calculus consistent with the logic.

Applicable to all first-order intuitionistic theories and some minimal systems.

Abstract

This reports introduces a novel sound and complete semantics for first order intuitionistic logic, in the framework of category theory and by the computational interpretation of the logic based on the so-called Curry-Howard isomorphism. Aside, a sound and complete semantics for the corresponding lambda-calculus is derived, too. This semantics extends, in a way, the more traditional meanings given by Heyting categories, the topos-theoretic interpretation, and Kripke models. The feature which justifies the introduction of this novel semantics is the fact that it is 'point-free', i.e., there is no universe whose elements are used to interpret the logical terms. In other words, terms do not denote individuals of some collection but, instead, they denote the 'glue' which keeps together the interpretations of statements, similarly to what happens in formal topology. Since the proposed semantics can be trivially extended to all the first-order logical theories based on the intuitionistic system (and, with some care, to minimal systems as well), the semantics covers also all the predicative theories, even if some peculiar aspects of these theories should be remarked.