Николай Плетнев//Игровая семантика интуиционистской логики по Межирову

Докладчик: Николай Плетнев Тема: Выводимость как осмысленная стратегия: игровая семантика интуиционистской логики по Межирову Аннотация: В докладе рассматривается игровая семантика для интуиционистского пропозиционального исчисления, предложенная И. Межировым. Выводимость формулы в IPC отождествляется с наличием выигрышной стратегии у пропонента в игре на множестве подформул. Приводятся доказательства теорем корректности и полноты, опирающиеся на конечные модели Крипке. На примерах показывается, как стратегический выбор ходов отражает синтаксическую выводимость или строит контрпримеры. Отмечаются педагогические преимущества подхода и перспективы его применения в автоматизации доказательств.