Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Доказательство. Для произвольной формулы А обозначим через h{A) выражение, получающееся в результате следующего преобразования формулы А: в А спускаются все кванторы и термы (вместе с соответствующими скобками и запятыми). Например, h (\/xjA^j (xj, х2)^ А\ ( хз )) qctb A^ i =^А\ , h( —I \/xiA xj J^ p A 3(^02) —^A 2(^3) ссть — A 2 ^^A ^^ p A 2 • По существу h{A) всегда является пропозициональной формой, в которой роль пропозициональных букв играют символы А у. Ясно, что имеют место h( —A)= -4 г(А), h(A^B)=h(A)^h(B). Также покажем, что для всякой аксиомы А, получаемой по какой-нибудь из схем ^7-^5, h{A) является тавтологией. Для А1,А2,АЗ это очевидно. Всякий частный случай А4 VxiAfx^j^Aft) преобразуется операцией h в тавтологию вида В^В, а всякий частный случай А5 Vxi(A^B)^(A^VxiB) в тавтологию вида (C^D)^(C^D). Далее: 1) пусть h{A) и h{A^B)=h{A)^h{B) - тавтологии, тогда h{B) - тоже тавтология; 2) если h{A) - тавтология, то h{ VxjA) - тавтология, ибо результаты применения операции h к ^ и к VxiA совпадают. Итак, из случаев 1) и 2) следует, что применение правил вывода MP и Gen сохраняет то свойство формул, что применение к ним функции h снова приводит к тавтологии. Теперь докажем, что если А теорема, то h{A) - тавтология. Пусть формула А есть теорема теории Ki, т.е. существует ее вывод в Kf. В],В2...,Вп, где Вп=А и каждое из В( (1< i< п) является либо аксиомой либо непосредственным следствием по MP либо по Gen из предыдущих формул этой последовательности. Тогда /г(Д) является тавтологией для любого i, в частности, тавтология h{Bn)=h{B). Если бы существовала формула В в К] такая, что |- 5 и |— S (выводимо В и —15), то по доказанному h{B) и h{ —B)= —h{B) были бы тавтологиями, что невозможно. Значит, не существует формулы В такой, что |- 5 и |- —В, следовательно, всякое исчисление предикатов первого порядка непротиворечиво. Что и требовалось доказать. О полноте исчисления предикатов первого порядка (теории Kj). Как было ранее замечено, в дедуктивных теориях вводят различные понятия полноты. Исчисление предикатов 1-го порядка называется полной в широком смысле, если каждая логическая общезначимая формула является теоремой. Иногда такую теорию считают полной, не добавляя слов «в широком смысле». 127