Неразрешимость логики первого порядка (стр. 5 из 7)
Мы требуем при этом, чтобы последовательность целых чисел p1,…, р,…, pv была возрастающей; р может совпадать с р1 или с рv Заметим, что формула (4) является описанием времени 0.
Предположим теперь, что машина, получив на входе число n, в конце концов останавливается. Тогда для некоторых s, i, p и j машина в момент s окажется в состоянии qi, считывая при этом клетку с номером р, содержащую символ aj, причем в программе машинной нет команды для комбинации qiaj.
Предположим, далее, что из множества формул Д следует некоторое описание G времени s. Поскольку I– модель для Д, формула G должно быть истинным в I. Поэтому G должно содержать в качестве конъюнктивных членов формулы 0(s)Qi0(p) и 0(s)Aj0(p) а потому из G должна следовать формула
$t $x (t Qix
t Ai x),входящее одним из дизъюнктивных членов в H. Поэтому Н будет следовать из Д.
Остается лишь показать, что для всякого неотрицательного s, если только машина не останавливается до момента s, из Д следует некоторое описание времени s. Докажем это индукцией по s.
Основание индукции. Пусть s = 0. Множество Д содержит, а потому и влечет за собой предложение (4), являющееся описанием времени 0.
Шаг индукции. Предположим, что выделенное курсивом предложение верно (для s). Предположим, далее, что наша машина не остановилась до момента s + 1. Это значит, что она не остановилась ни до момента s, ни в самый момент s. Тогда из Д следует некоторое описание (8) времени s. Нужно доказать, что из Д следует и некоторое описание времени s+1.
Поскольку I– модель для Д, формула (8) истинна в I. Поэтому в момент s машина находится в состоянии qi, считывая при этом некоторую клетку (с номером р), в которой записан символ aj. Поскольку машина в момент s не остановилась, в ее программе должна присутствовать команда одного из видов
(a)qiaj → ak С qm
(б)qiaj → ajП qm
(в)qiaj → ajЛ qm
Если имеется команда типа (а), то одна из формул множества Д есть
"x "y "t ((t Qi x
t Aj x) → (t' Qk x t Ap x (y ≠ x → (t A0y → t'A0y … tAny → t'Any))))Она вместе с (5), (6) и (8) влечет за собой формулу
0 (s+1) Qi0 (p)
0 (s+1) Aj10 (p1) … 0 (s+1) Aj0 (p) … 0 (s+1) Ajv0 (pv) "y ((y ≠ 0 (p1) … y ≠ 0 (p) … y ≠ 0 (pv)) → 0 (s+1) A0y),являющуюсяописаниемвремени s + 1.
Еcли имеется команда типа (б), то одна из формул множества Д есть
"x "y "t ((t Qi x
t Ajx) → (t' Qkx' (t A0y → t'A0y) … (tAny → t'Any)))Из этого предложения, объединенного с (5), (6) и (8), следует, что для некоторого символа
,0(s+1)Qi0(p+1)
0(s+1) 
… 0(s+1)Aj0(p+1) … 0(s+1) 
"y ((y ≠ 
… y ≠ 0(p+1) … y ≠ 
) → 0(s+1)A0y),а это предложение является описанием времени s + 1.
Если имеется стрелка типа (в), то одна из формул множества Д есть
"x "y "t ((t Qix'
t Ajx') → (t' Qkx (t A0y → t'A0y) … (tAny → t'Any)))Тогда существует такой символ aq, что из последней формулы, объединенной с (5), (6), (8), следует
0(s+1)Qi0(p-1)
0(s+1) 
… 0(s+1)Aj 0(p-1) … 0(s+1) 
"y((y
y 
0(p-1) … y 
) → 0(s+1)A0 y)а это предложение является описанием времени s + 1.
Во всех трех случаях множество Д имеет следствием некоторое описание времени s + 1, и тем самым неразрешимость логики первого порядка доказана.
Доказательство неразрешимости логики первого порядка методом Геделя
Для доказательства неразрешимости логики первого порядка достаточно продемонстрировать, как по данной машине Т с входным значением n (то есть когда машина находится на самой левой единице в сплошной последовательности из nединиц при пустых символах в остальных клетках ленты) построить такие предложение Iи конечное множество предложений Г, что машина Т при входном значении
останавливается тогда и только тогда, когда Г ├ I.