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

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

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

Программа

Лектор
Яворская Татьяна Леонидовна

Финансовая поддержка
Курс проводится при финансовой поддержке Минобрнауки России (грант на создание и развитие МЦМУ МИАН, соглашение № 075-15-2022-265).

Организации
Математический институт им. В.А. Стеклова Российской академии наук, г. Москва
Математический центр мирового уровня «Математический институт им. В.А. Стеклова Российской академии наук» (МЦМУ МИАН)