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

- один из видов неклассич. интерпретаций логических и логико математических языков. Различные интерпретации типа Р. определяются по следующей схеме. Для формул логико-математич. языка определяется отношение "объект [img: http://localhost:8080/file/041872-97.jpg] реализует замкнутую формулу F", к-рое сокращенно записывается [img: http://localhost:8080/file/041872-98.jpg]. Определение носит индуктивный характер: сначала отношение erF определяется для элементарных формул F, а затем для сложных формул в предположении, что для составляющих их более простых формул это отношение уже определено. Замкнутая формула Fназ. р е а л и з у е м о й, или истинной при данной интерпретации, если существует такой объект е, что erF. Формула F, содержащая свободные переменные x1,..., х n, считается реализуемой, если реализуема замкнутая формула [img: http://localhost:8080/file/041872-99.jpg] Впервые интерпретация такого вида, известная как рекурсивная реализуемость, была предложена С. Кли-ни (см. [1], [2]) с целью уточнения интуиционистской (конструктивной) семантики языка формальной арифметики в терминах рекурсивных функций. Другие понятия Р. являются модификациями рекурсивной Р. Интуитивный смысл отношения erF такой: объект екодирует информацию об истинности формулы F. Напр., в рекурсивной Р. натуральное число 0 реализует элементарную формулу вида s~i тогда и только тогда, когда эта формула верна (т. е. значения термов s и tсовпадают); если число ереализует дизъюнкцию [img: http://localhost:8080/file/041872-100.jpg], то по нему можно выяснить, какой ее член реализуем, и найти число, его реализующее; по числу, реализующему формулу [img: http://localhost:8080/file/041872-101.jpg], можно построить алгоритм, к-рый по любому натуральному числу пстроит реализацию формулы А(n). В качестве реализаций, т. е. объектов, реализующих формулы, чаще всего выступают натуральные числа. Однако при интуиционистской интерпретации языка математич. анализа в качестве реализаций могут использоваться и другие объекты, напр. одноместные теоретико-числовые функции (см., напр., [3]). Для формул логич. языков, напр. для пропозициональных или предикатных формул, Р. определяется обычно через понятие Р. для того или иного логико-математич. языка W. Логич. формула [img: http://localhost:8080/file/041872-102.jpg] считается реализуемой, если реализуема всякая формула языка Wполучающаяся подстановкой в [img: http://localhost:8080/file/041872-103.jpg] формул языка W вместо предикатных переменных. Интерпретации типа Р. нашли широкое применение в исследовании неклассических, прежде всего интуиционистских и конструктивных, логических и логико-математич. теорий. Имеется описание различных понятий Р. и их применений в теории доказательств для исследования интуиционистских теорий (см. [3], [4]).