MATHEMATICAL SEMANTICS OF INTUITIONISTIC LOGIC
SERGEY A. MELIKHOV
Abstract. This work is a mathematician’s attempt to understand intuitionistic logic.
It can be read in two ways: as a research paper interspersed with lengthy digressions
into rethinking of standard material; or as an elementary (but highly unconventional)
introduction to first-order intuitionistic logic. For the latter purpose, no training in
formal logic is required, but a modest literacy in mathematics, such as topological
spaces and posets, is assumed.
The main theme of this work is the search for a formal semantics adequate to Kol-
mogorov’s informal interpretation of intuitionistic logic (whose simplest part is more or
less the same as the so-called BHK interpretation). This search goes beyond the usual
model theory, based on Tarski’s notion of semantic consequence, and beyond the usual
formalism of first-order logic, based on schemata. Thus we study formal semantics of
a simplified version of Paulson’s meta-logic, used in the Isabelle prover.
By interpreting the meta-logical connectives and quantifiers constructively, we get a
generalized model theory, which covers, in particular, realizability-type interpretations
of intuitionistic logic. On the other hand, by analyzing Kolmogorov’s notion of semantic
consequence (which is an alternative to Tarski’s standard notion), we get an alternative
model theory. By using an extension of the meta-logic, we further get a generalized
alternative model theory, which suffices to formalize Kolmogorov’s semantics.
On the other hand, we also formulate a modification of Kolmogorov’s interpreta-
tion, which is compatible with the usual, Tarski-style model theory. Namely, it can
be formalized by means of sheaf-valued models, which turn out to be a special case
of Palmgren’s categorical models; intuitionistic logic is complete with respect to this
semantics.
https://arxiv.org/pdf/1504.03380.pdf 
