Кузнецов О.П., Адельсон-Вельский Г.М. - Дискретная математика для инженеров (1048837), страница 50
Текст из файла (страница 50)
(Здесь символы = и - используются на разных уровнях: символ = — как формальная преднкатная буква, не имеющая смысла до ее интерпретации, а символ « — как символ отношения на множестве, имеющий всем известный смысл «быть меньше»,) Собственные аксиомы прикладных исчислений вообще не общезначимы — иначе по теореме 6.6 они были бы доказуемы в чистом исчислении предикатов. Введенное ранее определение противоречивой формулы является семантическим, т.
е. связывающим непротиворечивость с истинностью. Исходя из него, можно сформулировать понятие семантически непротиворечивой теории; теория семантически непротиворечиво, если ни одна из ее теорем не является противоречивой, т. е. ложной в любой интерпретации. Исчисление высказываний и исчисление предикатов семантически непротиворечивы в силу теорем 6.3 и 6.5: все их теоремы общезначимы н, следовательно, непротнворечивы. С помощью введенных понятий ответ на общий вопрос, поставленный в начале параграфа, формулируется так: теория Т пригодна для описания тех множеств, которые являются ее моделями; модель для теории Т существует тогда и только тогда, когда Т семантически непротнворечива.
Чисто логические теории — исчисление высказываний и исчисление предикатов — в силу теорем 6.3 и 6.5 пригодны для описания любых множеств, что соответствует общенаучному принципу универсальности законов логики (Лейбниц форму- 241 пировал его как выполнимость логических законов «во всех мыслимых мирах»). Такой критерий пригодности теорий по существу известен уже давно; отыскание модели для теории до возникновения оснований математики было единственным общепризнанным методом доказательства законности теории.
Одно из важных достижений оснований математики заключается в том, что аналог этого критерия сформулирован в терминах самих формальных теорий, без привлечения семантических понятий. Таким аналогом является понятие формальной, или дедуктивной, непротиворечивости. Теория Т называется формально непротиворечивой, если не существует формулы Р, такой, что г" и ~г являются теоремами теории Т, т. е, в Т не выводимы одновременно формула и ее отрицание, Аналогичное определение можно сформулировать и для произвольного множества формул.
Для любой теории, содержащей исчисление высказываний, из определения непосредственно следует, что если она формально противоречива, то в ней доказуема тождественно-ложная формула и, следовательно, она семантически противоречива. Действительно, если Р и ~г доказуемы, то, подставив в аксиому! 5 г" вместо А, ~Р вместо В и дважды применив правило заключения, получим ) — АЬ 1А. Более того, никакое множество формул, содержащее г и ~Е (т. е. формально противоречивое), не может иметь модели, поскольку г" и 1Е не могут быть одновременно истинными ни в какой интерпретации, Тем самым доказано (от противного), что если множество формул семантически непротиворечиво, то оно формально непротиворечиво. Обратное утверждение (которое также оказывается верным), если понимать его конструктивно, гораздо глубже.
Смысл его в том, что по всякому формально непротиворечивому множеству формул можно построить его модель. Доказательство этого факта — его можно найти, например, в (39) — довольно сложно и заключается в изложении метода такого построения. Вместе оба утверждения образуют важную метатеорему.
Теорема 6.9. Множество формул формально непротиворечиво, если и только если оно семантически непротиворечиво (т. е. имеет модель). П Таким образом, понятие формальной непротиворечивости оказывается эквивалентным более привычному в математике понятию семантической непротиворечивости; однако оно сформулировано в синтаксических терминах и с конструктивной точки зрения более надежно (вспомним, что именно семантические трудности — парадоксы и привели к возникновению науки об основаниях математики и к концепциям формального подхода).
Привыкнуть же к эквивалентности этих двух понятий в математике было нелегко. Неприятие современниками неевклидовых геометрий Лоба. чевского — Бойаи объясняется именно тем, что законность этих теорий обосновывалась отсутствием в них противоречий — аргументом, по существу совпадающим с современным понятием формальной непротиворечивости. Геометрические модели для этих теорий, доказывающие их семантическую непротиворечивость, были найдены позднее. Полнота, разрешимость, аксиоматизнруемость. Теперь можно приступить к обсуждению вопросов об адекватности формальных теорий, т.
е. соответствии тем целям, ради которых они создавались. Пусть имеется, с одной стороны, содержательная теория 5, сформулированная в семантических терминах, т. е. совокупность истинных высказываний о некоторой алгебраической системе М; с другой стороны— формальная теория Т, т. е. множество выражений, выводимых из аксиом теории Т с помощью правил вывода теории Т. В каких случаях можно утверждать, что Т является удовлетворительной формализацией 5? Каковы признаки удовлетворительности формализации? Очевидно, необходимым признаком является условие, чтобы 5 была моделью теории Т, т.
е. чтобы существовало отображение, при котором всякая теорема теории Т отображается в истинное высказывание из 5. Однако само по себе это условие явно недостаточно, иначе дтя формализации любой теории 5 хватило бы чистого исчисления предикатов; ведь для него любое множество является моделью. Исчеряывающей формализацией 5 будет служить такая теория Т, для которой выполняется и обратное соответствие; каждое истинное высказывание теории 5 отображается в некоторую теорему теории Т, Теория Т с таким свойством называется полной относительно 5, а иногда (например, в (391 ) — адекватной 5.
Из теорем 6.3 и 6.4 следует, что исчисление высказываний полно относительно алгебры высказываний, а теоремы 6.6 я 6.6 образуют известную теорему Геделя о полноте исчисления предикагов относительно логики предикатов, т. е. множества всех общезначимых предикатных формул, Если для семантической (содержательной) теории 5 удается построить непротиворечивую и полную формальную теорию Т, то 5 естественно назвать аксиомагизируемой, или 16* (йормализугиой, теорией. Из предыдущих результатов следует, что логика высказываний и логика предикатов аксиома4изируемы с помощью соответствующих исчислений. Еще одна важная характеристика формальной теории— это ее разрешимость.
Формальная теория Т называется разрешимой, если существует алгоритм, который для любой формулы языка определяет, является она теоремой в Т или нет, иначе говоря, если предикат «быть теоремой в теории Т» общерекурсивен. Теорема 6.10. Исчисление высказываний разрешимо. Разрешающий алгоритм для формулы г" исчисления высказываний заключается в вычислении значений г" на всех наборах значений. ее переменных.
Ввиду полноты исчисления высказываний Г является его теоремой, если и только если она истинна на всех наборах. П Теорема 6.11 (теорема Черча). Исчисление предикатов неразрешимо. Несмотря на полноту исчисления предикатов, разрешающий алгоритм, связанный с вычислением значений истинности предикатных формул, построить не удается по причине, отмеченной в гл, 3, — из-за бесконечности предметной области, которая приводит в общем случае к бесконечным таблицам истинности.
Идея доказательства теоремы Черча (которое здесь не приводится; его можно найти в (371) состоит в том, чтобы в чистом исчислении предикатов описать предикат Я(й а, х): «машина Тьюринга с номером й будучи применена к исходным данным а, закончит вычисление в момент х». Предикат ВхЯ(1, а, х) — это предикат остановки, а ВхЯ(а, а, к) — предикат самоприменимости; неразрешимость обоих предикатов была доказана в гл. 5. П Отметим, что важный для приложений фрагмент исчисления предикатов разрешим: исчисление одноместн ы х п р е д и к а т о в (т.
е. исчисление, допускающее в формулах только одноместные предикатные буквы) р а з р'ешимо. Еще тяжелее обстоит дело с формальной арифметикой, система аксиом которой приведена в конце 3 6.2. Теорема 6.12 (первая теорема Геделя о неполноте в форме Клики). Любая формальная теория Т, содержащая формальную арифметику, неполна; в ней существует (и мо. жет быть эффективно построена) замкнутая формула Г, такая, что )Г истинно, но ни Г, ни )Р не выводимы в Т. Теорема 6.13 (вторая теорема Геделя о неполноте). Для любой непротиворечивой формальной теории Т, содержащей 244 формальную арифметику, формула, выражающая непротиворечивость Т, недоказуема в Т.
С) Таким образом, арифметика и теория чисел оказываются неаксноматизируемыми теориями. В терминах теории алгоритмов сформулированные ранее результаты можно резюмировать так: 1) множество всех истинных высказываний логики высказываний перечислимо и разрешимо; 2) множество всех истинных высказываний логики предикатов перечислимо (ввиду его полноты), но неразрешимо; 3) множество всех истинных высказываний арифметики неперечислимо: если бы для него существовала перечисляющая процедура (и, следовательно, соответствующая машина Тьюринга), то по ней можно было бы построить полную формальную теорию, рассматривая правила перехода машины от одной конфигурации к другой как правила вывода, процесс вычисления — как вывод, а результаты вычисления — как теоремы.
Две знаменитые теоремы Геделя имеют важное методологическое значение. Из первой теоремы следует, что для достаточно богатых математических теорий не существует адекватных формализаций. Правда, любую неполную теорию Т можно расширить, добавив, например, к ней в качестве новой аксиомы истинную, но не выводимую в Т формулу, Однако по первой теореме Геделя новая теория Т также будет неполна, Вторая теорема может быть истолкована как невозможность исследования метасвойств теории средствамн самой формальной теории (опять невозможность самоприменимости)); иначе говоря, метатеория теории Т для того, чтобы иметь возможность доказывать хотя бы непротиворечивость теории Т, должна быть богаче Т.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
