Популярное видео

Новые поступления

Для просмотра файлов Вам могут потребоваться

Workshop on Proof Theory, Modal Logic and Reflection Principles
17 октября 2017 г. 17:15–17:50, Москва, Математический институт им. В.А. Стеклова РАН

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

S. Melikhov
MP4 982.2 Mb
MP4 269.2 Mb

Количество просмотров:
Эта страница:112

S. Melikhov

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

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

Аннотация: 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.

Язык доклада: английский

ОТПРАВИТЬ: FaceBook Twitter Livejournal
Обратная связь:
 Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2019