Семинар 7. Теоретико-игровая семантика

В математической логике и теории вычислимости часто оказывается плодотворным взгляд на формулу как игру, в которой один игрок пытается доказать истинность формулы, а второй — эту формулу опровергнуть. Доклад посвящён одной из реализаций этого подхода, а именно — теоретико-игровой семантике (также называемой GTS, от game-theoretic semantics).
В первой части доклада будет дано определение GTS для классической логики первого порядка, и доказаны некоторые её основные свойства, а также будет показано, что истинность формулы в GTS совпадает с истинностью в привычной семантике Тарского. Затем мы обсудим связь GTS с понятием сколемизации функции.
Во второй части доклада будет обсуждаться GTS для расширения классической логики первого порядка, называемого IF-FOCL (где IF — от independence friendly). Мы рассмотрим, как появление игр с неполной информацией в теоретико-игровой семантике для IF-FOCL приводит к существенным отличиям от теоретико-игровой семантики для FOCL.
Доклад основан на материале книги Mann, A.L., Sandu, G. and Sevenster, M. Independence-Friendly Logic: A Game-Theoretic Approach.