Реализуемость

Один из видов неклассич. интерпретаций логических и логико математических языков. Различные интерпретации типа Р. определяются по следующей схеме. Для формул логико-математич. языка определяется отношение "объект реализует замкнутую формулу F", к-рое сокращенно записывается . Определение носит индуктивный характер: сначала отношение erF определяется для элементарных формул F, а затем для сложных формул в предположении, что для составляющих их более простых формул это отношение уже определено. Замкнутая формула Fназ. р е а л и з у е м о й, или истинной при данной интерпретации, если существует такой объект е, что erF. Формула F, содержащая свободные переменные x1, . . ., х n, считается реализуемой, если реализуема замкнутая формула Впервые интерпретация такого вида, известная как рекурсивная реализуемость, была предложена С. Кли-ни (см. [1], [2]) с целью уточнения интуиционистской (конструктивной) семантики языка формальной арифметики в терминах рекурсивных функций. Другие понятия Р. являются модификациями рекурсивной Р. Интуитивный смысл отношения erF такой: объект екодирует информацию об истинности формулы F. Напр., в рекурсивной Р. натуральное число 0 реализует элементарную формулу вида s~i тогда и только тогда, когда эта формула верна (т. е. значения термов s и tсовпадают); если число ереализует дизъюнкцию , то по нему можно выяснить, какой ее член реализуем, и найти число, его реализующее; по числу, реализующему формулу , можно построить алгоритм, к-рый по любому натуральному числу пстроит реализацию формулы А(n). В качестве реализаций, т. е. объектов, реализующих формулы, чаще всего выступают натуральные числа. Однако при интуиционистской интерпретации языка математич. анализа в качестве реализаций могут использоваться и другие объекты, напр. одноместные теоретико-числовые функции (см., напр., [3]). Для формул логич. языков, напр. для пропозициональных или предикатных формул, Р. определяется обычно через понятие Р. для того или иного логико-математич. языка W. Логич. формула считается реализуемой, если реализуема всякая формула языка Wполучающаяся подстановкой в формул языка W вместо предикатных переменных. Интерпретации типа Р. нашли широкое применение в исследовании неклассических, прежде всего интуиционистских и конструктивных, логических и логико-математич. теорий. Имеется описание различных понятий Р. и их применений в теории доказательств для исследования интуиционистских теорий (см. [3], [4]). Лит.:[1] К 1 е е n е S. С., "J. Symbolic Logic", 1945, V. 10, р. 109-24; [2] К л и н и С. К., Введение в метаматематику, пер. с англ., М., 1957; [3] К л и и и С., В е с л и Р., Основания интуиционистской математики..., пер. с англ., М., 1978; [4] Д р а г а л и н А. Г., Математический интуиционизм. Введение в теорию доказательств, М., 1979. В. Е. Плиско.