Новиков Ф.А. Дискретная математика для программистов (860615), страница 32
Текст из файла (страница 32)
Положим A{t) : = А(...х...){t//x}. Имеем: s*(A{t)) = ТФ=> 5*(Л(Ж)) = Т,где si имеет значение s*(t) на месте х. Если s*(Vx (А(ж))) = Т и терм t свободендля ж в Л, то s*(A(t)) — Т. Следовательно, формула Vx (А(ж)) —> A(t) выполненапа всех последовательностях в произвольной интерпретации.•ДОКАЗАТЕЛЬСТВОЗАМЕЧАНИЕМожно показать, что формула A(t) —> ЗГЕ (А) (х), где терм t свободен для переменной хв формуле А, общезначима.4.4.4. Непротиворечивость и полнотачистого исчисления предикатовНам потребуется следующее преобразование h формулы исчисления предикатов в формулу исчисления высказываний: в формуле опускаются все кванторыи термы вместе с соответствующими скобками и запятыми, остаются предикатные символы (которые рассматриваются как пропозициональные переменные) исвязки.ПримерЛ,(Vx ( Р ( х ) ^ З у (Q(x,y))))=P^Q.Такое преобразование как бы «забывает» всё, что связано с исчислением предикатов, оставляя только пропозициональную структуру, которая является формулойисчисления высказываний.Нетрудно видеть, что h(-*A) — -h(A)ТЕОРЕМА 1и h(A —> В) = h(A) —> h(B).Формальная теория X непротиворечива.Рассмотрим пропозициональную структуру аксиом исчисленияпредикатов X, то есть применим к аксиомам преобразование h.
Ясно, что всеполучеипые формулы суть тавтологии, поскольку аксиомы А\,А 2 ,Аз сами посебе совпадают со своими пропозициональными структурами, которыеявляются тавтологиями, а для аксиом исчисления предикатов имеемДОКАЗАТЕЛЬСТВОh(Pi)= h(Vx(А(Ж))A(t))= А ^А и h{P2)= h(A{t)ЗЖ ( А ( Х ) ) ) = АА.Далее, правило Modus ponens сохраняет тавтологичпость пропозициональнойструктуры, то есть если h(A) и h(A —> В) — тавтологии, то h,(B) — тавтология. Правилаи V+ также сохраняют тавтологичпость пропозициональнойструктуры, поскольку в этих правилах пропозициоиалышя структура заключе-166Глава 4. Логические исчисленияния совпадает с пропозициональной структурой посылки. Таким образом, еслиформула А является теоремой теории X, то формула h(A) является тавтологией.Далее от противного.
ЕслиА и- А то h(A) и h(A) — тавтологии, чтоневозможно.•Следующие две метатеоремы устанавливают свойства полноты исчисления предикатов, аналогичные тем, которые установлены для исчисления высказыванийв подразделе 4.3.8. Теоремы приводятся без доказательств, которые техническидовольно громоздки.ТЕОРЕМА 2Всякая теорема чистого исчисления предикатов первого порядка об-щезначима.Всякая общезначимая формула является теоремой чистого исчисления предикатов первого порядка.ТЕОРЕМА 34.4.5.
Логическое следование и логическаяэквивалентностьФормула В является логическим следствием формулы А (обозначение А ==*• В),если формула В выполнена па любом наборе в любой интерпретации, на которомвыполнена формула А. Формулы А и В логически эквивалентны (обозначениеА = В), если они являются логическим следствием друг друга. Можно показать,что имеют место следующие логические следования и эквивалентности:1. ->Vx (А(х)) = Зх (iA(x)).2. - G x (А(х)) = Vx (-Vl(x)).3. Vx ((A(x) k B(x))) = Vx (A(x)) k Vx (B(x)).4.
Зх (A(x) V B(x))Зх {A(x)) V 3x (£(x)).5. 3x (A(x) k B{x)) =• Зх (A(x)) k 3x (B{x)).6. Vx {A(x)) V Vx (B(x))Vx (A(x) V B(x)).7. Vx (Vy (A(x,y)))=Vy(Vx (A(x,y))).8. З х (3у (A(x,y))) = 3y (3x (A(x,y))).9. Vx (A(x) k C) = Vx (A(x)) k C.10. Vx (Л(х) V С) = Vx {A{x)) V C.11. 3x [A(x) kC) = Зх (A(x)) k C.12. Зх (A{x) V С) = Зх (A{x)) V C.13. C ^ V x ( A ( x ) ) = V x{C^A(x)).14. СЗх {A{x)) = Зх (CA(x)).15. 3x (Vy (A(x,y)))=>Vy(3x (A(x,y))).16. Vx (A(x)B(x)) = » Vx (A(x)) -> Vx (B(x)),где формула С не содержит никаких вхождений переменной х.1674.4. Исчисление предикатовДля всякой формулы А существует логически эквивалентная ей формула А',имеющая предварённую форму:Aгде Qi,...,=QIX\...QП ХП А{х 1,...1 XN)IQn — некоторые кванторы, а А — бескванторная формула.4.4.6.
Теория равенстваЭтот подраздел начинает серию примеров прикладных исчислений предикатов.ЗАМЕЧАНИЕНапомним, что всякое прикладное исчисление предикатов содержит в себе чистое исчисление предикатов, поэтому при описании прикладного исчисления аксиомы и все теоремычистого исчисления подразумеваются, указываются только собственные функциональныесимволы, предикаты и аксиомы.Теория равенства £— это прикладное исчислеиие предикатов, в котором имеются:1. Собственный двухместный предикат = (инфиксная запись х = у).2.
Собственные аксиомы (схемы аксиом):Е\\ Чх (х = х),Е2-. (х =у)^(А(х)-+А(х){у/х}).ТЕОРЕМАВ теории £ выводимы следующие теоремы:1. I t = t для любого терма t.2. Ь £х =у3. bg х = уу = х.(у = z -> х = z).ДОКАЗАТЕЛЬСТВО[ 1 ] Из Ei и Pi по Modus ponens.[ 2 ] Имеем: (х = у) —• (х = х —• у = х) из Е2 при подстановке {х = х/А(:г)}.Зиачит, х = у, х = ху = х. Но hg х = х, следовательно, х = у hg у = х.По теореме дедукциих = у —• у = х.[ 3 ] Имеем: у = х —• (у = z —• х = z) из Е2 при подстановке {х = z/A{x), у/х, х/у},зиачит, у = х l-£ (у = z —> х = z). Но х = у hg у = х, по транзитивности х = у hg(у = г —> х = z), по теореме дедукции hg (х = у) —у (у = zх = г).•Таким образом, равенство является эквивалентностью.
Но равенство — это болеесильное свойство, чем эквивалентность. Аксиома Е2 выражает неотличимостьравных элементов.168Глава 4. Логические исчисления4.4.7. Формальная арифметикаФормальная арифметика А — это прикладное исчисление предикатов, в которомимеются:1. Предметная константа 0.2. Двухместные функциональные символы -1-й-, одноместный функциональныйсимвол '.3. Двухместный предикат =.4.
Собственные аксиомы (схемы аксиом):Ai:(Р(0) & Vx ( Р ( х )Р(х')))Vx ( Р ( х ) ) ,А2: U' =t2'^tx=t2,А3: - . ( * ' = 0 ) ,Л4: £i = t2 -> (£i = £3 -» t2 = £3),-^5 • t] = t2t\ = £2',Л6:£ + 0 = £,Л7: i] +t2' = {h +t2)',Л 8 : £• 0 = 0,AQ : t] • t2 = t\ • t2 -f £1,где P — любая формула, a £, £1, t2 — любые термы теории Л.ЗАМЕЧАНИЕВпервые данная система аксиом для арифметики была предложена Пеано1, а А\ — этосхема аксиомы математической индукции.4.4.8. Неаксиоматизируемые теорииВ этом подразделе на примере некоторых понятий теории (абелевых) группнеформально устанавливаются границы применимости исчисления предикатовпервого порядка.Теория групп S — это прикладное исчисление предикатов с равенством, в которомимеются:1.
Предметная константа 0.2. Двухместный функциональный символ +.3. Собственные аксиомы (схемы аксиом):G1:G2:G3:1V х. у, z (х + (у + z) = (х + у) + z),Vx (0 + х = х),Vx (Зу (х + у = 0)).Джузсппе Псапо ( 1 8 5 8 - 1 9 3 2 ) .1694.4. Исчисление предикатовЗАМЕЧАНИЕВыражение «теория первого порядка с равенством» означает, что подразумевается наличие предиката =, аксиом Е\ и £2 и всех их следствий.Группа называется абелевой, если имеет место собственная аксиомаС4:Ух,у(х + у = у + х) .Говорят, что в абелевой группе все элементы имеют конечный порядок п, есливыполнена собственная аксиомаG5 :VX(3 k ^ п (kx = 0 ) ) ,где kx — это сокращение для х + х + • • • + х.А: разЭта формула пе является формулой теории S, поскольку содержит «посторонние» предметные предикаты и переменные.
Однако для любого конкретного конечного п собственная аксиома может быть записана в виде допустимой формулытеории S:G'5:Vx ((х = 0 V 2х = 0 V . . . V пх = 0 ) ) .Абелева группа называется делимой, если выполнена собственная аксиомаV n ^ 1 (Vx (Зу (пу = х))).G6:Эта формула не является формулой теории S, поскольку содержит «посторонние» предметные константы и переменные.
Однако собственная аксиома может быть записана в виде бесконечного множества допустимых формул теории S:G'6:Vx (Зу (2у = х ) ) ,Vx (Зу (Зу = х ) ) ,Но можно показать, что любое конечное множество формул, истинное во всехделимых абелевых группах, истинно и в некоторой неделимой абелевой группе,то есть теория делимых абелевых групп не является конечно аксиоматизируемой.Абелева группа называется периодической, если выполнена собственная аксиомаG-j:Vx (Зп ^ 1 (пх = 0 ) ) .Эта формула также не является формулой теории 9, поскольку содержит «посторонние» предметные константы и переменные. Если попытаться преобразоватьформулу G-1 по образцу формулы G5, то получится бесконечная «формула»Gj:Vx ((х = 0 V 2 x = 0 V . . .
V n x = 0 V • • • ) ) ,которая не является допустимой формулой исчисления предикатов и тем более теории S. Таким образом, теория периодических абелевых групп пе является аксиоматизируемой (если не включать в теорию групп и всю формальнуюарифметику).170Глава 4. Логические исчисленияОТСТУПЛЕНИЕНаличие неаксиоматизируемых и конечно неаксиоматизируемых формальных теорий пеозначает практической неприменимости аксиоматического метода на основе использования языка исчисления предикатов первого порядка. Это означает, что аксиоматическийметод не применим «в чистом виде*. На практике формальные теории, описывающиесодержательные объекты, задаются с помощью собственных аксиом, которые наряду ссобственными предикатами и функциональными символами содержат «внелогические»предикаты и функциональные символы, свойства которых аксиомами не описываются, асчитаются известными (в данной теории). В рассмотренных примерах подраздела 4.4.8внелогическими являются натуральные числа и операции над ними.
Аналогичное обстоятельство имеет место и в системах логического программирования типа Пролог. Реализация такой системы всегда снабжается обширной библиотекой внелогических (или встроенных) предикатов и функций, которые и обеспечивают практическую применимостьсистемы логического программирования.4.4.9. Теоремы Гёделя о неполнотеДавно известны некоторые важные свойства формальных теорий, в частности,прикладных исчислений предикатов первого порядка, которые существеннымобразом влияют на практическую применимость формальных теорий (аксиоматического метода).
Полное доказательство этих фактов выходит далеко зарамки данного учебника. Однако понимание границ применимости формальныхметодов является, по нашему мнению, необходимым для использования такихметодов. Поэтому ниже приводятся для сведения (без доказательства и в упрощённой формулировке) два важнейших факта, известные как теоремы Гёделя1 онеполноте.Аксиоматический метод обладает множеством достоинств и с успехом применяется па практике для формализации самых разнообразных предметных областейв математике, физике и других науках.
Однако этому методу присуще следующеепринципиальное ограничение.ТЕОРЕМА (Первая теорема Гёделя о неполноте)Во всякой достаточнобогатойтеории первого порядка (в частности, во всякой теории, включающей формальную арифметику), существует такая истинная формула F, что ни F, нинеявляются выводимыми в этой теории.Утверждения о теории первого порядка также могут быть сформулированы ввиде формул теории первого порядка. В частности, утверждения о свойствах формальной арифметики (например, утверждение о непротиворечивости формальной арифметики), могут быть сформулированы как арифметические утверждения.1Курт Гёдель ( 1 9 0 6 - 1 9 7 8 ) .1714.5.
Автоматическое доказательство теоремТЕОРЕМА (Вторая теорема Гёделя о неполноте)Во всякой достаточнобогатойтеории первого порядка (в частности, во всякой теории, включающей формальнуюарифметику), формула F, утверждающая непротиворечивость этой теории, неявляется выводимой в ней.ОТСТУПЛЕНИЕВторая теорема Гёделя не утверждает, что арифметика противоречива. (Формальная арифметика из примера 4.4.7 как раз непротиворечива.) Эта теорема утверждает, что непротиворечивость достаточно богатой формальной теории не может быть установлена средствами самой этой теории (см. ещё раз следствие к теореме 4.3.8).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
