Geometric Modality and Weak Exponentials

TL;DR

This paper introduces weak exponential objects and modal spaces to address non-geometric and impredicative issues in constructive logic, leading to new modal logics and topological semantics.

Contribution

It proposes a formalization of predicative function spaces and a geometric approach to implications using modal spaces, advancing the foundations of constructive logic.

Findings

Development of weak exponential objects for predicative function spaces

Introduction of modal spaces for geometric implications

Construction of new modal propositional logics with topological semantics

Abstract

The intuitionistic implication and hence the notion of function space in constructive disciplines is both non-geometric and impredicative. In this paper we try to solve both of these problems by first introducing weak exponential objects as a formalization for predicative function spaces and then by proposing modal spaces as a way to introduce a natural family of geometric predicative implications based on the interplay between the concepts of time and space. This combination then leads to a brand new family of modal propositional logics with predicative implications and then to topological semantics for these logics and some weak modal and sub-intuitionistic logics, as well. Finally, we will lift these notions and the corresponding relations to a higher and more structured level of modal topoi and modal type theory.