Курс Т. Л. Яворской "Логики свидетельств"

Просьба ко всем участникам, в том числе смотрящим видеозаписи,
зарегистрироваться по ссылке: https://forms.gle/sajeQ8in28EaDoqH9.

В курсе будут описаны логики свидетельств и изложены основные результаты, полученные для них. Логики свидетельств были введены С.Н. Артемовым в 1995. Пропозициональные логики свидетельств формулируются в стандартном пропозициональном языке, обогащенном термами для обозначений свидетельств истинности формулы. При замене явных свидетельских термов модальностью, выражающей их существование, логика свидетельств превращается в некоторую модальную логику. В этом смысле логики свидетельств можно рассматривать как явные аналоги модальных логик. Мы опишем логики свидетельств, соответствующие некоторым известным модальным логикам и семантику для них, и докажем теорему о реализации соответствующих им модальных логик, т.е. тот факт, что для всякой теоремы $F$ модальной логики $L$ из некоторого списка найдется такой способ приписывания свидетельских термов вхождениям модальностей в эту формулу, при котором $F$ становится теоремой логики свидетельств $J(L)$.

Более подробно мы остановимся на логика доказательств $LP$ (С.Н. Артемовым, 1995 г.), с которой начались исследования в этой области. Мы покажем что аналогом логики $LP$ является модальная логика $S4$ и построим перевод пропозициональной интуиционистской логики в $LP$. Далее, для $LP$ мы опишем арифметическую семантику, в которой пропозициональные переменные соответствуют предложениям формальной арифметики, а свидетельские термы - кодам арифметических доказательств. Мы докажем теорему о полноте $LP$ относительно этой семантики, что вместе с результатами о реализации $S4$ и интуиционистской логики в $LP$ позволит описать доказуемостную семантику для них.

Помимо этого, мы опишем логики свидетельств первого порядка, семантику для них, докажем теоремы о полноте относительно этой семантики и о реализации модальных логик первого порядка. Также мы опишем различные варианты арифметической семантики логик свидетельств первого порядка.