Математическая энциклопедия - гёделя интерпретация
Связанные словари
Гёделя интерпретация
интуиционистской арифметики специальная операция, переводящая формулы интуиционистской арифметики в формулы вида где наборы переменных по вычислимым функциям специального вида. При этом выводимые формулы переводятся в истинные формулы в смысле нек-рои четко описанной семантики. Эта интерпретация, к-рая была использована К. Гёделем для нового доказательства непротиворечивости арифметики формальной, представляет также значительный интерес как нек-рая семантика для языка формальной арифметики.
Рассматривается бескванторная аксиоматич. теория Тс бесконечным числом типов переменных. Класс переменных данного типа определяется индуктивно, а именно: 1) переменные типа 0, переменные для натуральных чисел; 2) пусть теория содержит переменные типов тогда теория содержит и переменные типа t, где tесть . Переменные типа tобозначаются через и рассматриваются как переменные для вычислимых в нек-ром смысле функций, перерабатывающих каждый набор функций типов соответственно в функцию типа . Язык Тсодержит термы различных типов: переменная типа является термом типа , 0 есть терм типа О, символ s, к-рый служит для обозначения функции прибавления единицы к натуральному числу, есть терм типа (0,0). Остальные термы образуются с помощью правил порождения: Черча -абстракции и примитивной рекурсии для функций произвольного типа. Атомарные формулы теории Тсуть равенства , где термы типа 0. Формулы теории Тполучаются из атомарных с помощью логических связок исчисления высказываний . Постулатами Тявляются аксиомы и правила вывода интуиционистского исчисления высказываний, аксиомы для равенства, аксиомы Пеано для 0 и S, уравнения примитивных рекурсий, аксиома применения функции, определенной l-абстракцией, и, наконец, принцип математич. индукции, сформулированный в виде правила вывода без употребления кванторов. Через обозначим теорию Т, пополненную кванторами по переменным произвольного типа и соответствующими логическими аксиомами и правилами вывода для кванторов.
Г. и. переводит всякую формулу (а следовательно, и всякую формулу интуиционистской арифметики) в формулу вида
где формула без кванторов, а наборы переменных различных типов, совокупность всех свободных переменных формулы .
Пусть F - формула интуиционистской арифметики и ее гёделевская интерпретация. Если Fвыводима в формальной интуиционистской арифметике, то может быть построен терм теории Ттакой, что формула выводима в Т. Таким образом, непротиворечивость арифметики сводится к установлению непротиворечивости бескванторной теории Т.
Интуиционистская семантика на основе Г. и. определяется следующим образом: формула Fсчитается истинной, если найдется вычислимый терм такой, что бескванторная формула истинна при всяком вычислимом z.
Лит.:[1]Гёдель К., в сб.: Математическая теория логического вывода, М., 1967, с. 299-310. А. Г. Драгалин.
Математическая энциклопедия. — М.: Советская энциклопедия
И. М. Виноградов
1977—1985
Вопрос-ответ:
Похожие слова
Самые популярные термины
1 | 558 | |
2 | 484 | |
3 | 482 | |
4 | 474 | |
5 | 455 | |
6 | 441 | |
7 | 438 | |
8 | 435 | |
9 | 426 | |
10 | 425 | |
11 | 423 | |
12 | 413 | |
13 | 407 | |
14 | 376 | |
15 | 376 | |
16 | 373 | |
17 | 367 | |
18 | 366 | |
19 | 365 | |
20 | 363 |