A joint logic of problems and propositions

TL;DR

This paper introduces a formal logical system, QHC, that unifies the treatment of propositions and problems, extending intuitionistic and classical logic with a new, comprehensive framework.

Contribution

It constructs a formal system, QHC, that combines the logic of problems and propositions, unifying Kolmogorov's problem interpretation with proof interpretations in a conservative extension.

Findings

QHC is a conservative extension of QH and QC.

The axioms formalize Kolmogorov's problem interpretation.

The system unifies intuitionistic and classical logic approaches.

Abstract

In a 1985 commentary to his collected works, Kolmogorov informed the reader that his 1932 paper 'On the interpretation of intuitionistic logic' "was written in hope that with time, the logic of solution of problems [i.e., intuitionistic logic] will become a permanent part of a [standard] course of logic. A unified logical apparatus was intended to be created, which would deal with objects of two types - propositions and problems." We construct such a formal system as well as its predicate version, QHC, which is a conservative extension of both the intuitionistic predicate calculus QH and the classical predicate calculus QC. The axioms of QHC are obtained as a result of a simultaneous formalization of two well-known alternative explanations of intiuitionistic logic: 1) Kolmogorov's problem interpretation (with familiar refinements by Heyting and Kreisel) and 2) the proof interpretation by Orlov and Heyting, as clarified and extended by G\"odel.