Аннотация:
Доклад посвящен семантике гибридной логики первого порядка, в языке которой присутствуют и свидетельские термы, и модальность. Особенность таких логик в том, что язык позволяет выразить как утверждение "$t$ является свидетельством формулы $F$, содержащей свободную переменную $x$", так и "для данного значения $x$, $t$ является свидетельством формулы $F(x)$". В первом утверждении переменная $x$ связанная, во втором свободная. Естественным представляется добавить в язык аналогичную конструкцию и для модальности (так называемые связывающие модальности). Мы определим логику, которая комбинирует логику свидетельств первого порядка FOLP и модальную логику S4 первого порядка со связывающими модальностями. Для этой логики определим модели в стиле моделей Фиттинга для FOLP, сформулируем теоремы о полноте и корректности относительно этой семантики и коротко обсудим основную идею доказательства. Мы используем эту семантику для доказательства невыводимости некоторых принципов и покажем, при каких требованиях мы можем гарантировать существование модели, отвечающей им.
|
