Дискретная математика (998286), страница 22
Текст из файла (страница 22)
3, Имеем; у = х -+ (у = г -+ х = 2) из Ег при подстановке (у/х,х/у), значит, у = х 1-с (у = г -+ х = 2). Но х = у 1-е у = х, по транзитивности х = у г.с (у= а-к х = 2), по теореме дедукции ьз (х=у) » (у= 2-кх= 2). и Таким образом, равенство является эквивалентностью. Но равенство — это более сильное свойство, чем эквивалентность. Аксиома Ег выражает неоииичимссть равных элементов. 4.4.7. Формальная арифметика Формальная аригрметика Я вЂ” это прикладное исчисление предикатов, в котором имеются: 1. Предметная константа О.
2. Двухместные функторы + и, одноместный функтор 3. Двухместный предикат -. 4. Собственные аксиомы (схемы аксиом): А1. (Р(0) йУх (Р(х) -+ Р(х'))) -+ Чх Р(х), Аг . '11' = 12' -+ 11 = 12„ Аз. '-(1' = О) А»: 11 = сг -+ (11 = 12 -+ 12 = сз), Аз: 11 = 12 -+ 11' = 12', А: 1+0 =й Ат ~1+~2 =(11+12), Аз: 1 0=0 Ая. 11 12' =11. 12+11, где Р— любая формула, а 1,11,12 — любые термы теории Я. 4.4.8.
Теория (абелеаых) групп теория групп 5 — это прикладное исчисление предикатов с равенсэ1всм, в котором имеются: 1. Предметная константа О. 2. Двухместный функтор +. 125 4.4, Исчисление предикатое 3. Собственные аксиомы (схемы аксиом): С1. Ч х, у, з х + (у + з) = (х + у) + з, Сз. Чх О+х =х, Сз: ч'х зу х+ у = О. ЗАМЕЧАНИЕ Выражение «теория первого порядка с раеенстаом» означает, что подразумевается наличие преднката -, аксиом Е1 н Еа н всех нх следствий. Группа называется абелевой, если имеет место собственная аксиома С«.
Чх,ух+у=у+х. Абелева группа называется группой конечного порядка и, если выполнена соб- ственная аксиома Се. Чх Л и ( и кх = О, где кх — это сокрашенне для х+х+ +х (к слагаемых). Эта формула не является формулой теории 9, поскольку содержит «посторонние» предметные предикаты и переменные. Однако для любого конкретного конечного н собственная аксиома может быть записана в виде допустимой формулы теории 9: С~а. » х (х = О 'ч' 2х = О Ч... 'ч' пх = О). Абелева группа называется полной, если выполнена собственная аксиома Се. 'ч'и > 1 Ч х 3 у пу = х. Эта формула ие является.
формулой теории 9, поскольку содержит «посторонние» предметные константы и переменные. Однако собственная аксиома может быть записана в виде бесконечного множества допустимых формул теории 9: Се: Ч х Э у 2у = х, 'тх зу Зу = х, Но любое конечное множество формул, истинное во всех полных абелевых группах, истинно и в некоторой неполной абелевой группе, то есть теория полных абелевых групп не является конечно аксиоматизируемой. Абелева группа называется периодической, если выполнена собственная аксиома Ст: Чх Эп > 1 нх = О. Эта формула не является формулой теории 9, поскольку содержит «посторонние» предметные константы и переменные.
Если попытаться преобразовать формулу Ст но образцу формулы Сз, то получится бесконечная «формула» 126 Глава 4. Логические исчисления Ух (х = О 72х = О у, ч пх т О Ч ...), которая не является допустимой формулой исчисления предикатов и тем более теории 9. Таким образом, периодическая абелева группа не является аксиоматизируемой (если не включать в теорию групп и всю формальную арифметику). ОТСТУПЛЕНИЕ Наличие иеаксиоматиэируемых и конечна иеаксиоматиэируемых формальных теорий ие означает практической неприменимости аксиоматического метода Это означает, что аксиоматический метод ие применим «в чистом виде». На практике формальные теории, описывающие содержательные объекты, задаются с помощью собственных аксиом, которые наряду с собственными предикатами и функторами содержат «виелогические»' предикаты и фуикторы, свойства которых аксиомами не описываются, а считаются известными (в данной теории).
В рассмотренных примерах подраздела 4А.8 виелогическими являются натуральные числа и операции иад ними. Аналогичное обстоятельство имеет место и в системах логического программирования типа Пролог. Реализация такой системы всегда снабжается обширной' библиотекой виелогических (или встроенных) предикатов и фуикторов, которые и обеспечивают практическую применимость системы логического программирования. 4.4.9. Теоремы Геделя о неполноте В настоящее время точно известны некоторые важные свойства формальных теорий, в частности, прикладных исчислений предикатов первого порядка, которые существенным образом влияют на практическую применимость формальных теорий (аксиоматичского метода). Полное изложение этих фактов выходит далеко за рамки данного учебника. Поэтому ниже приводятся для сведения (без доказательства и в упрощенной формулировке) два важнейших факта, известные как теоремы Геделят о неполноте.
Аксиоматический метод обладает множеством достоинств и с успехом применяется на практике для формализации самых разнобразных предметных областей в математике, физике и других науках. Однако этому методу присуще следующее принципиальное ограничение. ТЕОРЕМА (Первая теорема Геделя о неполноте) Во всякой достаточно богатой теории первого порядка (в частности, во всякой теории, включающей формальную арифметику), существует такая иппинная формула г', что ни г, ни г не являются выводимыми в этой теории. Утверждения о теории первого порядка также могут быть сформулированы в виде формул теории первого порядка. В частности, утверждения о свойствах формальной арифметики могут быть сформулированы как арифметические утверждения, »Курт Гелель (1906-1978) 127 4.8.
Автоматическое доказательство теорем ТЕОРЕМА (Вторая теорема Геделя о неполноте) Во всякой достаточно богатой теории первого порядка (в частности, во всякой теории, включающей формальную арифметику), формула г, утверждающая непротиворечивость этой теории, не является выводимой в ней. ОТСТУПЛЕНИЕ Вторяя теорема Геделя пе утверждает, что арифметика противоречива. (Формальнаа арифметика нэ примера 4.4.7 как Раз пепротиаоречнва.) Теорема Геделя утверждает, что непротиворечивость достаточно богатой формальной теории не может быть установлена средствами самой этой теории (см. еще раэ следствие к теореме 4.3.8). При этом вполне может статься, что непротиворечивость одной конкретной теории может быть установлена средствами другой, более могш1ой формальной теории. Но тогда возникает вопрос о непротиворечивости этой второй теории и т.
д. 4.5. Автоматическое доказательство теорем Автоматическое доказательство теорем — зто краеугольный камень логического программирования, искусственного интеллекта и других современных направлений в программировании. Здесь излагаются основы метода резолюций — классического и в то же время популярного метода автоматического доказательства теорем. 4.5.1. Постановка задачи Алгоритм, который проверяет отношение Г)- В для формулы Я, множества формул Г, н теории Т называется алгоритмом автоматического доказательсгпва теорем.
В общем случае такой алгоритм невозможен, то есть не существует алгоритма, который для любых Я, Г и Т выдавал бы ответ «Да», если Г )-т Я, и ответ «Нет», если неверно, что Г )-т Я. Более того, известно, что нельзя построить алгоритм автоматического доказательства теорем даже для большинства конкретных достаточно сложных формальных теорий Х В некоторых случаях удается построить алгоритм автоматического доказательства теорем, который применим не ко всем формулам теории (то есть частичный алгоритм, см.
подраздел 4.2.5). Для некоторьгх простых формальных теорий (например исчисление высказываний) и некоторых простых классов формул (например прикладное исчисление предикатов с одним одноместным предикатом) алгоритмы автоматического доказательства теорем известны. Пример Поскольку для исчисления высказываний известно, что теоремами являются общезначимые формулы, можно воспользоваться простым методом проверки общезначимости формулы с помощью таблиц истинности.
А именно, достаточно 128 Глава 4. Логические исчисления вычислить нстинностное значение формулы при всех возможных интерпретациях (их конечное число). Если во всех случаях получится значение И, то проверяемая формула — тавтология, и, следовательно, является теоремой теории Г.. Если же хотя бы в одном случае получится значение Л, то проверяемая формула не является тавтологией и, следовательно, не является теоремой теории г".. ЗАМЕЧАНИЕ Приведенный выше пример является алгоритмом автоматического доказательства теорем в теории С, хотя и пе является алгоритмом автоматического поиска вывода теорем из аксиом теории Г..
Наиболее известный классический алгоритм автоматического доказательства теорем называется методом резолюций. Для любого прикладного исчисления предикатов первого порядка Т, любой формулы Я и множества формул Г теории Т метод резолюций выдает ответ «Да», если Г ьг Я, и выдает ответ «Нет» или не выдает никакого ответа (то есть зацикливается), если неверно, что Г )-т Я.
4.5.2. Доказательство от противного В основе метода резолюций лежит идея «доказательства от противного» твсрЕМА Если Г, Я г- р, еде Р— любое противоречие (тождественно ложная формула), то Г Ь Я. Доказаткпьство (Для случая С.) Г, — Я Ь Р 4=» Гй Я » Р— тавтология. Но Г й Я -+ Р = (Г й Я) ч Р = (Г й Я) = Г ч Я = Г » Я. Имеем: à — г Я вЂ” тавтология е=» Г Ь Я. Пустая формула не имеет никакого значения ни в какой интерпретации, в частности, не является истинной ни в какой интерпретации и, по определению, является противоречием. В качестве формулы Р при доказательстве от противного по методу резолюций принято использовать пустую формулу, которая обозначается г1.
4.5.3. Сведение к предложениям Метод резолюций работает с особой стандартной формой формул, которые называются предложениями. Предложение — зто бескванториая дизъюнкция литералов. Любая формула исчисления предикатов может быть преобразована в множество предложений следуюшим образом (здесь знак ==. используется для обозначения способа преобразования формул). 129 4.5. Автоматическое доказательство теорем 1. Элиминация импгикации.' Преобразование: А — ь В ~е - А тг В. После первого этапа формула содержит только, Ч, Й, Ч, 3.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
