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

- один из видов неклассич. интерпретаций логических и логико математических языков. Различные интерпретации типа Р. Определяются по следующей схеме. Для формул логико-математич. Языка определяется отношение "объект реализует замкнутую формулу 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. В. Е. Плиско.