A joint logic of problems and propositions
Sergey A. Melikhov
TL;DR
QHC presents a unified two-sorted logic that combines intuitionistic and classical predicate theories with a joint interpretation of problems and propositions. Through Box, negneg, ∇, and Diamond syntactic translations, it embeds into QS4, QH, and QC, respectively, while preserving sorts and yielding conservative extensions. The work analyzes a spectrum of principles (H-, K-, R-, D-, and related rules), proving which are derivable or independent and exploring their implications via topological models. It also introduces several semantic frameworks (interior-based, regularization-based, subset/sheaf-valued, and dense-image models) that illuminate the logical structure and suggest applications to algebra, geometry, and arithmetic, including a path toward a QHCλ-realizability interpretation.
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ödel.