A joint logic of problems and propositions, a modified BHK-interpretation and proof-relevant topological models of intuitionistic logic

ABSTRACT. \documentclass{llncs}

\title{A joint logic of problems and propositions, a modified BHK-interpretation and proof-relevant topological models of intuitionistic logic} \author{Sergey A. Melikhov} \institute{Steklov Mathematical Institute (Moscow)}

\usepackage{amscd,amsmath,amssymb,verbatim} \usepackage{stmaryrd} \usepackage{cmll}

\begin{document}

\maketitle

In a 1985 commentary to his collected works, Kolmogorov remarked that his 1932 paper (``Zur Deutung der intuitionistischen Logik'') ``was written in hope that with time, the logic of solution of problems will become a permanent part of [a standard] course of logic. Creation of a unified logical apparatus dealing with objects of two types --- propositions and problems --- was intended.'' We describe such a formal system, QHC, which is a conservative extension of both the intuitionistic predicate calculus, QH, and the classical predicate calculus, QC. Moreover: \begin{itemize} \item The only new connectives $\wn$ and $\oc$ of QHC induce a Galois connection (i.e., a pair of adjoint functors) between the Lindenbaum algebras of QH and QC, regarded as posets.

\item Kolmogorov's double negation translation of propositions into problems extends to a retraction of QHC onto QH.

\item G\"odel's provability translation of problems into modal propositions extends to a retraction of QHC onto its QC+($\wn\oc$) fragment, which can be identified with the modal logic QS4. \end{itemize}

This leads to a new paradigm that views intuitionistic logic not as an alternative to classical logic that criminalizes some of its principles, but as an extension package that upgrades classical logic without removing it. The purpose of the upgrade is proof-relevance, or ``categorification''; thus, if the classical conjunction and disjunction are to be modeled by intersection and union (of sets), the intuitionistic conjunction and disjunction will be modeled by product and disjoint union (of sheaves of sets). More formally, we describe a family of sheaf-valued models of QH, inspired by dependent type theory (not to be confused with the well-known {\it open set-valued} sheaf models of QH), which can be regarded as proof-relevant analogues of classical topological models of Tarski et al., and which extend to models of QHC. We also give an interpretation of some of these models in terms of stable solutions of algebraic equations; this can be seen as a proof-relevant counterpart of Novikov's classical interpretation of some Tarski models in terms of weighting of masses.

The new paradigm also suggests a rethink of the Brouwer--Heyting--Kolmogorov interpretation of QH. Traditional ways to understand intuitionistic logic (semantically) have been rooted either in philosophy --- with emphasis on the development of knowledge (Brouwer, Heyting, Kripke) or in computer science --- with emphasis on effective operations (Kleene, Markov, Martin-L\"of). Our ``modified BHK interpretation'' is rooted in the usual mathematical ideas of canonicity and stability; it emphasizes simply the order of quantifiers, developing Kolmogorov's original approach. This interpretation is compatible with two complete classes models of QH: (i) Tarski topological models and (ii) set-theoretic models of Medvedev--Skvortsov and L\"auchli; as well as with (iii) our sheaf-valued models.

\end{document}