План лекций (очень подробный), страница 4

мулу a на место переменной x; если в данной ветви вообще нет термов

без переменных, то в w включается одна произвольная константа; после

построения w упомянутое кванторное правило применяется до тех пор, по-

ка все термы из w не будут подставлены в a на место x; 3) после всех

построений возникает новая висячая вершина; в соответствующей ей сек-

венции пометка с рассмотренной формулы снимается, а пометки на форму-

лах, не изменяемых описанными применениями правил, сохраняются; затем

построение продолжается в соответствии с 1) или 2).

Т4. Исчисление g полно (Если А - замкнутая формула, то |= a =>

|-g a). Д. Если в систематически построенном дереве вывода секвенции

->a все ветви заканчиваются аксиомами, получен вывод. Иначе есть (ко-

нечная или бесконечная) ветвь, не заканчивающаяся аксиомой, и по ней

можно построить (конечный или бесконечный) контрпример к формуле a.

В некоторых случаях описываемый в теореме метод построения конт-

рпримера дает бесконечный контрпример к формуле a, но другим способом

можно построить конечный контрпример к этой же формуле. Тем не менее,

существуют формулы, с одной стороны, не являющиеся общезначимыми, а

с другой стороны, истинные во всех конечных интерпретациях (не имеющие

конечных контрпримеров). Пусть f1 = їr(x,x); f2 =

r(x,y)&r(y,z)>r(x,z); f = a.f1 & a.f2 > a.xe.y r(x,y). У формулы f су-

ществует бесконечная модель (натуральный ряд с отношением строгого по-

рядка), но все конечные интерпретации являются контрпримерами. Поэтому

у формулы їf нет ни одного конечного контрпримера, но есть бесконеч-

ный (т.е. формула не общезначима).

$4. Полнота и корректность исчисления натурального вывода.

Т5. Исчисление n корректно (|-n a => |=a). Д.: добавляем к g-ис-

числению три правила вывода и доказываем, что их применения (сверху

вниз) сохраняют общезначимость.

l->r,f1 f1,l->r l->r l->r

(сечение) ----------------- (утончение) ------- -------

l->r l->r,f1 f1,l->r

Каждую формулу a в n-выводе заменяем на секвенцию b1,...,bn->a,

где b1,...bn - все гипотезы, от которых a зависит; все формулы Б "сти-

раем". Показываем, что в полученном "выводе" каждое применение "прави-

ла" можно заменить на совокупность применений секвенциальных правил (с

учетом дополнительных). Из корректности g-исчисления следует коррект-

ность n-исчисления.

Т6. Исчисление n полно (|= a => |-n a). Д. Модифицируем исчисле-

ние g: все секвенции вида a1,...,an->b1,...,bm превратим в

a1,...,an,їb1,...,їbm->Б и соответствующим образом изменим правила вы-

вода. После добавления правил

Б,l->Б їa->

----------- и -----

f1,їf1,l->Б ->a

получим исчисление gm с единственной аксиомой Б,l->Б, такое что каждо-

му g-выводу секвенции ->a соответствует gm-вывод этой же секвенции.

Если формула общезначима, то по Т4 существует ее g-вывод. Сопоставим

"готовому" gm-выводу строящую его последовательность применений правил

поиска вывода в этом исчислении (они соответствуют контрприменениям

gm-правил), а каждому такому правилу - последовательность применений

правил поиска n-вывода. Т.к. в исходном gm-выводе все ветви заканчива-

ются аксиомами, при построении этого вывода по правилам поиска вывода

каждый подвывод закончится ситуацией Б |- Б. Поэтому и поиск вывода в

n-исчислении завершится построением вывода.

Ключевые слова к $$2-4: исчисление натурального вывода = нату-

ральное исчисление = исчисление n; исчисление секвенций = секвенциаль-

ное исчисление = генценовское исчисление = исчисление g; вывод=доказа-

тельство; гипотеза, исключение гипотез; аксиома; правило вывода; пра-

вило поиска вывода; корректность/полнота исчисления.

$5. Эквивалентные преобразования формул.

Отношение является отношением эквивалентности, если оно рефлек-

сивно, симметрично и транзитивно. Рассмотрим 3 отношения эквивалент-

ности логических формул: 1) |= (a>b) & (b>a) (собственно эквивалент-

ность), 2) |=a <=> |=b (одновременная общезначимость), 3) a |= Б <=> b

|= Б (одновременная невыполнимость).

Формула a называется невыполнимой (противоречивой), если a|=Б.

Т7 связывает эквивалентность 1 с эквивалентностями 2 и 3.

Т7. Если формулы a и b собственно эквивалентны, то они одновре-

менно общезначимы и одновременно невыполнимы. Д. следует из определе-

ний.

Замечание. Обратное не верно.

Т8-11 относятся к собственно эквивалентности (эквивалентности в

смысле 1).

Т8. Следующие пары формул эквивалентны в смысле 1): 1) a>b и

їavb; 2) їїa и a; 3) aob и boa; 4) ao(boc) и (aob)oc; 5) ao(b*c) и

(aob)*(aoc); 6) ї(aob) и їa*їb; 7) qxa и a (если a не содержит x сво-

бодно); 8) qxa(x) и qya(y); 9) їqxa и gxїa; 10) qx(aob) и (qxa)ob (ес-

ли b не содержит x свободно); 11) a.x(b&c) и (a.xb & a.xc); 12)

e.x(bvc) и (e.xb v e.xc). Обозначения: если o = &, то * = v, и наобо-

рот; если q=a., то g=e., и наоборот. Д.: построение g-выводов.

Т9 (о замене эквивалентных подформул). Если формулы a и b эквива-

лентны в смысле 1, и формула cb получается из ca заменой подформулы a

на подформулу b, то формулы ca и cb эквивалентны в этом же смысле. Д.:

индукция по глубине расположения подформулы a в формуле ca; построение

g-выводов.

Формула находится в предваренной нормальной форме (пнф), если

имеет вид q1x1...qnxn b, где b - формула без кванторов (при этом выра-

жение q1x1...qnxn называется кванторной приставкой).

Т10. Любую формулу можно привести к пнф (Для любой формулы a су-

ществует формула b в пнф, эквивалентная ей в смысле 1). Д. следует из

Т8-9.

Формула находится в конъюнктивной нормальной форме (кнф), если

имеет вид a1&...&an (n>=1), где ai - дизъюнкт, т.е. b1v...vbm (m>=1),

где bj - литера, т.е. c или їС, где С - атомарная формула.

Т11. Любую формулу без кванторов можно привести к кнф. (Для любой

формулы без кванторов a существует формула b в кнф, эквивалентная a в

смысле 1). Д. следует из Т8-9.

Т12-13 относятся к одновременной общезначимости и одновременной

невыполнимости (эквивалентностям в смыслах 2 и 3).

Т12. При замыкании формулы кванторами общности сохраняется общез-

начимость и невыполнимость (|=f <=> |=a.f; f|=Б <=> a.f|=Б). Д. следу-

ет из Т2.

Пусть a=q1x1...qnxn b - формула в пнф (n>=0). Тогда формула С на-

зывается скулемовской нормальной формой (снф) формулы a, если она по-

лучена из a следующими преобразованиями: если qi - квантор существова-

ния, а qj1,...,qjm (m>=0) - все кванторы общности, предшествующие qi в

последовательности q1,...,qn, то qixi удаляется из кванторной пристав-

ки, а в формуле b каждое вхождение переменной xi заменяется на терм