Теория алгоритмов. Зюзысов В.М. - 43 стр.

UptoLike

ВУЗ: 

ТГУ | Томск

Составители: 

Рубрика: 

Оказывается функцию, осуществляющую гёделеву нумерацию формул
элементарной арифметики, можно сделать даже примитивно-рекурсивной.
Гёделева нумерация устанавливает также счетность формул теории первого
порядка.
Заметим, что метаматематическое утверждение «∀x есть начальная часть формулы
∀x (x×S(0) = x)» отражается внутрь теории, переходя в чисто арифметическое
предложение «гёделевый номер выражения ∀x, равный 2
9
×3
11
, является делителем
гёделевого номера полной формулы».
Лемма о рефлексии
– Он целовал вас, кажется?
– Боюсь, что это так.
– Но как же вы позволили?
– Ах, он такой чудак.
Он думал, что уснула я
И всё во сне стерплю,
Иль думал, что я думала,
Что думал он: я сплю!
Ковентри Патмор «О поцелуе»
Формулы EA «умеют говорить» только о натуральных числах
. Чтобы формула Q
могла говорить «о формулах и о себе», все формулы должны быть закодированы
натуральными числами с помощью гёделевой нумерации. Пусть функция g осуществляет
гёделеву нумерацию. Если теперь для некоторой формулы A(x) и другой формулы B
удается установить, что |– A(g(B)), то можно сказать: в теории EA
доказано, что формула B
«обладает свойством A».
Теорема 22 (лемма о рефлексии). Пусть A(x) произвольная формула формальной
арифметики, имеющая единственную свободную переменную x. Тогда можно построить
замкнутую формулу B, такую, что |– B ~ A(g(B)).
Неформально говоря, для любого выразимого свойства формул, можно подобрать
замкнутую формулу, «утверждающую», что она этим
свойством обладает.
В своей знаменитой теореме о неполноте (см. ниже) К. Гёдель использовал
конструкцию, которая составляет доказательство леммы о рефлексии, однако в общем
виде он эту лемму не сформулировал. Доказательство этой леммы в различных формах
см. в [16, с. 79; 9, с. 153–154; 21, с. 128; 25, с.15–16].
Мы приведем еще один вариант доказательства. Предполагаем, что в
EA
существует счетное множество функций (операций), причем каждый функциональный
символ имеет свой код Гёделя. Если s – синтаксический объект в EA, то, ради краткости
записи, пусть #s обозначает его геделевский номер («код»), а <s> ≡ <#s> –
соответствующий терм в EA. В этих обозначениях формулировка теоремы следующая:
Пусть A(x) – формула системы EA
с единственной свободной переменной x. Тогда
существует формула B системы EA, такая, что
|–
EA
B ~ A(<B>).
(B говорит: «Я обладаю свойством A»)
Доказательство.
Введем на множестве натуральных чисел N бинарное отношение ~:
n
1
~ n
2
⇔ существуют формулы A
1
и A
2
в EA, такие, что n
1
= #A
1
, n
2
= #A
2
и |– A
1
~ A
2
. Для
теоремы достаточно показать, что для данной формулы A(x) существует такое n∈N, что
n ~ #A(<n>). (1)
Действительно, после этого взяв формулу B такую, что n = #B будем иметь |– B ~ A(<n>).
Так как <n> = <#B> ≡ <B>, то получим, что |– B ~ A(<B>).
Для доказательства (1) введем следующее определение.

Страницы