ГЁДЕЛЯ ИНТЕРПРЕТАЦИЯ это:

ГЁДЕЛЯ ИНТЕРПРЕТАЦИЯ

интуиционистской арифметики - специальная операция, переводящая формулы интуиционистской арифметики в формулы вида где - наборы переменных по вычислимым функциям специального вида. При этом выводимые формулы переводятся в истинные формулы в смысле нек-рои четко описанной семантики. Эта интерпретация, к-рая была использована К. Гёделем для нового доказательства непротиворечивости арифметики формальной, представляет также значительный интерес как нек-рая семантика для языка формальной арифметики.

Рассматривается бескванторная аксиоматич. теория Тс бесконечным числом типов переменных. Класс переменных данного типа определяется индуктивно, а именно: 1) - переменные типа 0, переменные для натуральных чисел; 2) пусть теория содержит переменные типов тогда теория содержит и переменные типа t, где tесть . Переменные типа tобозначаются через и рассматриваются как переменные для вычислимых в нек-ром смысле функций, перерабатывающих каждый набор функций типов соответственно в функцию типа . Язык Тсодержит термы различных типов: переменная типа является термом типа , 0 есть терм типа О, символ s, к-рый служит для обозначения функции прибавления единицы к натуральному числу, есть терм типа (0,0). Остальные термы образуются с помощью правил порождения: Черча -абстракции и примитивной рекурсии для функций произвольного типа. Атомарные формулы теории Тсуть равенства , где - термы типа 0. Формулы теории Тполучаются из атомарных с помощью логических связок исчисления высказываний . Постулатами Тявляются аксиомы и правила вывода интуиционистского исчисления высказываний, аксиомы для равенства, аксиомы Пеано для 0 и S, уравнения примитивных рекурсий, аксиома применения функции, определенной l-абстракцией, и, наконец, принцип математич. индукции, сформулированный в виде правила вывода без употребления кванторов. Через обозначим теорию Т, пополненную кванторами по переменным произвольного типа и соответствующими логическими аксиомами и правилами вывода для кванторов.

Г. и. переводит всякую формулу (а следовательно, и всякую формулу интуиционистской арифметики) в формулу вида


где - формула без кванторов, а - наборы переменных различных типов, - совокупность всех свободных переменных формулы .

Пусть F - формула интуиционистской арифметики и - ее гёделевская интерпретация. Если Fвыводима в формальной интуиционистской арифметике, то может быть построен терм теории Ттакой, что формула выводима в Т. Таким образом, непротиворечивость арифметики сводится к установлению непротиворечивости бескванторной теории Т.

Интуиционистская семантика на основе Г. и. определяется следующим образом: формула Fсчитается истинной, если найдется вычислимый терм такой, что бескванторная формула истинна при всяком вычислимом z.

Лит.:[1]Гёдель К., в сб.: Математическая теория логического вывода, М., 1967, с. 299-310. А. Г. Драгалин.


Математическая энциклопедия. — М.: Советская энциклопедия. . 1977—1985.

Смотреть что такое "ГЁДЕЛЯ ИНТЕРПРЕТАЦИЯ" в других словарях:

  • ИНТЕРПРЕТАЦИЯ — (от лат. interpretatio истолкование, разъяснение) 1) общенаучный метод с фиксированными правилами перевода формальных символов и понятий на язык содержательного знания; 2) в гуманитарном знании истолкование текстов, смыслополагающая и… …   Философская энциклопедия

  • Теорема Гёделя о неполноте — У этого термина существуют и другие значения, см. Теорема Гёделя. Теорема Гёделя о неполноте и вторая теорема Гёделя[ 1]  две теоремы математической логики о принципиальных ограничениях формальной арифметики и, как следствие, всякой… …   Википедия

  • Теоремы Гёделя о неполноте — Теоремы Гёделя о неполноте  две теоремы математической логики о принципиальных ограничениях формальной арифметики и, как следствие, всякой достаточно сильной[1] теории первого порядка. Первая теорема утверждает, что если формальная… …   Википедия

  • Метрика Гёделя — Метрика Гёделя  это точное решение уравнений Эйнштейна, полученное Куртом Гёделем в 1949 году[1]. Это решение порождается тензор энергии импульса из двух частей, первая представляет собой плотность материи однородно распределённых… …   Википедия

  • МЕТАТЕОРИЯ — (от греч. meta после, за, позади) теория, изучающая язык, структуру и свойства некоторой др. теории. Теория, свойства которой исследуются в М., называется предметной, или объектной, теорией. Наиболее развиты М. в логике и математике (металогика И …   Философская энциклопедия

  • Логика первого порядка — (исчисление предикатов)  формальное исчисление, допускающее высказывания относительно переменных, фиксированных функций и предикатов. Расширяет логику высказываний. В свою очередь является частным случаем логики высшего порядка. Содержание 1 …   Википедия

  • Исчисление предикатов — Логика первого порядка (исчисление предикатов)  формальное исчисление, допускающее высказывания относительно переменных, фиксированных функций, и предикатов. Расширяет логику высказываний. В свою очередь является частным случаем логики высшего… …   Википедия

  • Исчисления предикатов — Логика первого порядка (исчисление предикатов)  формальное исчисление, допускающее высказывания относительно переменных, фиксированных функций, и предикатов. Расширяет логику высказываний. В свою очередь является частным случаем логики высшего… …   Википедия

  • Логика предикатов — Логика первого порядка (исчисление предикатов)  формальное исчисление, допускающее высказывания относительно переменных, фиксированных функций, и предикатов. Расширяет логику высказываний. В свою очередь является частным случаем логики высшего… …   Википедия

  • Предикатная логика — Логика первого порядка (исчисление предикатов)  формальное исчисление, допускающее высказывания относительно переменных, фиксированных функций, и предикатов. Расширяет логику высказываний. В свою очередь является частным случаем логики высшего… …   Википедия


Поделиться ссылкой на выделенное

Прямая ссылка:
Нажмите правой клавишей мыши и выберите «Копировать ссылку»