Введение
Логики вычислимости – это формулировки логики, которые отражают некоторые аспекты вычислимости как фундаментальное понятие. Обычно это предполагает сочетание специальных логических связок и семантики, объясняющей, как логика должна интерпретироваться в вычислительном смысле. Вероятно, первым формальным рассмотрением логики вычислимости является интерпретация реализуемости, предложенная Стивеном Клини в 1945 году, где он дал интерпретацию интуиционистской теории чисел в терминах вычислений машины Тьюринга. Его целью было точное формализование BHK-интерпретации интуиционизма (Гейтинга – Брауэра – Колмогорова), согласно которой доказательства математических утверждений следует рассматривать как конструктивные процедуры. С развитием различных логик, таких как модальная и линейная логика, а также новых семантических моделей, таких как игровая семантика, логики вычислимости были сформулированы в нескольких контекстах. Мы упомянем два из них.
capture some aspect of computability as a basic notion. This usually involves a mix
of special logical connectives as well as a semantics that explains how the logic is to be interpreted in a computational way. Probably the first formal treatment of logic for computability is the realizability interpretation by Stephen Kleene in 1945, who gave an interpretation of intuitionistic number theory in terms of Turing machine computations. His motivation was to make precise the Heyting–Brouwer–Kolmogorov (BHK) interpretation of intuitionism, according to which proofs of mathematical statements are to be viewed as constructive procedures. With the rise of many other kinds of logic, such as modal logic and linear logic, and novel semantic models, such as game semantics, logics for computability have been formulated in several contexts. Here we mention two.
Модальная логика для вычислимости
Оригинальная интерпретация реализуемости Клини привлекла большое внимание исследователей, изучающих связь между вычислимостью и логикой. В 1982 году Мартин Хайланд расширил её на полную интуиционистскую логику высшего порядка, построив эффективный топос. В 2002 году Стив Аводей, Ларс Биркедал и Дана Скотт сформулировали модальную логику для вычислимости, которая расширила стандартную интерпретацию реализуемости двумя модальными операторами, выражающими понятие "вычислительной истинности".
Логика вычислимости Джапаридзе
"Логика вычислимости" — это имя собственное, обозначающее исследовательскую программу, начатую Джорджием Джапаридзе в 2003 году. Её целью является переосмысление логики на основе игровой теоретической семантики. Такая семантика рассматривает игры как формальные эквиваленты интерактивных вычислительных задач, а их "истинность" — как существование алгоритмических выигрышных стратегий. См. Логика вычислимости.