

Workshop on Proof Theory, Modal Logic and Reflection Principles
October 17, 2017 17:15, Moscow, Steklov Mathematical Institute






Kolmogorov's interpretation and a formal semantics of the metalogic of intuitionistic logic
S. Melikhov^{} 
Video records: 

MP4 
982.2 Mb 

MP4 
269.2 Mb 
Number of views: 
This page:  74  Video files:  19 

Abstract:
I would like to report on a formal semantics capturing Kolmogorov's informal interpretation of intuitionistic logic in terms of problem solving.
Kolmogorov's interpretation consists of two parts: one deals with the logical connectives and, implicitly, quantifiers, and is more or less the same as the socalled BHK interpretation; and the other deals with principles and rules and hence, implicitly, with the metalogical connectives and quantifiers. The logical part has been extensively covered and discussed in the literature  albeit mostly in the terminology of Brouwer and Heyting, which forces a onceandforall choice between intuitionistic and classical logics despite their coexistence and interaction in Kolmogorov's approach. (Concerning this interaction see https://arxiv.org/abs/1312.2575 and https://arxiv.org/abs/1504.03379.)
By contrast, the metalogical part has been neglected. This is not surprising, as it turns out to be incompatible with the usual model theory, based on Tarski's notion of semantic consequence; worse yet, it is an interpretation of something that does not exist in the usual formalism of firstorder logic (but exists, for instance, in the metalogical formalism of the Isabelle prover). However, ignoring the metalogical part has the effect of throwing the baby out with the bathwater: as observed by Troelstra and van Dalen, "the BHKinterpretation in itself has no ‘explanatory power’ ", since "on a very ‘classical’ interpretation of [the informal notions of] construction and mapping," its six clauses "justify the principles of twovalued (classical) logic."
To address these issues, we develop a formal semantics of Isabelle's metalogic, or rather of its simplified version which suffices for firstorder logics without equality. In usual model theory, regarded as a particular semantics of the metalogic, the metalogical connectives and quantifiers are interpreted classically (and moreover in the twovalued way) — even though they are constructive. By interpreting them constructively, we get a generalized model theory, which covers, in particular, some realizabilitytype interpretations of intuitionistic logic.
On the other hand, Kolmogorov's interpretation of inference rules (which is a substantial part of his interpretation of intuitionistic logic, and seems to be uniquely possible in his approach) is based on a notion of semantic consequence that is alternative to Tarski's standard notion, and is incompatible even with the generalized model theory. Thus we develop an alternative model theory, which is nothing new for formulas and principles, but an entirely different interpretation of rules (and of more complex metalogical constructs). By using an extension of the metalogic, we further get a generalized alternative model theory, which suffices to formalize Kolmogorov's interpretation of rules. See https://arxiv.org/abs/1504.03380.
As a work in progress, we also develop a slightly different, "categorifed" semantics of the metalogic, which in particular yields an interpretation of the metalogic of (firstorder) intuitionistic logic that has some intrinsic similarity with Voevodsky's interpretation of MartinLöf's type theory with universes.
Language: English

