Videolibrary
RUS  ENG    JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB  
Video Library
Archive
Most viewed videos

Search
RSS
New in collection






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


Kolmogorov's interpretation and a formal semantics of the meta-logic of intuitionistic logic

S. Melikhov
Video records:
MP4 982.2 Mb
MP4 269.2 Mb

Number of views:
This page:238
Video files:46

S. Melikhov



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 so-called BHK interpretation; and the other deals with principles and rules and hence, implicitly, with the meta-logical 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 once-and-for-all 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 meta-logical 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 first-order logic (but exists, for instance, in the meta-logical formalism of the Isabelle prover). However, ignoring the meta-logical part has the effect of throwing the baby out with the bathwater: as observed by Troelstra and van Dalen, "the BHK-interpretation 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 two-valued (classical) logic."
To address these issues, we develop a formal semantics of Isabelle's meta-logic, or rather of its simplified version which suffices for first-order logics without equality. In usual model theory, regarded as a particular semantics of the meta-logic, the meta-logical connectives and quantifiers are interpreted classically (and moreover in the two-valued way) — even though they are constructive. By interpreting them constructively, we get a generalized model theory, which covers, in particular, some realizability-type 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 meta-logical constructs). By using an extension of the meta-logic, 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 meta-logic, which in particular yields an interpretation of the meta-logic of (first-order) intuitionistic logic that has some intrinsic similarity with Voevodsky's interpretation of Martin-Löf's type theory with universes.

Language: English
 
  Contact us:
 Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2024