Video Library
Most viewed videos

New in collection

You may need the following programs to see the files

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:127
Video files:27

S. Melikhov

Видео не загружается в Ваш браузер:
  1. Установите Adobe Flash Player    

  2. Проверьте с Вашим администратором, что из Вашей сети разрешены исходящие соединения на порт 8080
  3. Сообщите администратору портала о данной ошибке

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 and
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
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

SHARE: FaceBook Twitter Livejournal
Contact us:
 Terms of Use  Registration  Logotypes © Steklov Mathematical Institute RAS, 2020