Игошин Математическая логика и теория алгоритмов (1019110), страница 66
Текст из файла (страница 66)
Аналогично, множество Ф формул называется семантически непротиворечивым, если ни одна формула, выводимая из Ф, не является противоречивой. В теореме 16.1 доказано, что всякая теорема формализованного исчисления высказываний общезначима (тождественно истинна), а потому не является противоречивой. Это означает, что формализованное исчисление высказываний семантически непротиворечиво. Аналогичная теорема доказана и для формализованного исчисления предикатов (см.
следствие 29.3 из теоремы 29.1 выше). Значит, и ФИП семантически непротиворечиво. Семантическая непротиворечивость ФИВ и ФИП означает, что эти формальные теории пригодны для описания любых классов алгебраических систем, т.е. они войдут в теории этих классов составными частями, что вполне соответствует общенаучному принципу универсальности законов логики (Лейбниц формулировал его как выполнимость логических законов «во всех мыслимых мирах»).
Произвольная формальная теория Т есть теория множества М(Т) всех своих моделей, а значит, теория Т семантически не- противоречива, если и только если М(Т) ,-с И, т.е. для теории Т существует модель. Если отождествить пригодность математической теории, ее целесообразность с ее семантической непротиворечивостью, то можно сказать, что сформулированный критерий пригодности теории известен уже давно. Отыскание модели для теории до возникновения оснований математики было единственным общепризнанным методом доказательства «законности» теории. Математическая логика выработала аналог этого критерия, не опирающийся на наличие модели теории — внешний фактор по отношению к теории, а опирающийся на внутренние свойства самой теории, — понятие синтаксической непротиворечивости теории.
Определение 29.5. Формальная теория Т называется синтаксически (или дедуктивно, или формально) непротиворечивой, если не существует такой формулы Г, что Г и — Г являются теоремами теории Т, т.е. в Тневыводимыми являются одновременно формула и ее отрицание. Аналогичное определение можно сформулировать и для произвольного множества Ф формул: Ф называется синтаксически непротиворечивым, если из Ф невыводимы одновременно формула и ее отрицание, В теореме 16.9 доказана синтаксическая непротиворечивость формализованного исчисления высказываний.
Аналогично доказывается следующая теорема. Теорема 29.6. Формализованное исчисление предикатов синтаксически непротиворечиво. 265 До к аз а тел ь ство. Допустим противное, т.е. предположим, что ФИП синтаксически противоречиво. Значит, найдется такая формула Р, что Р и Р будут теоремами ФИП.
Тогда по следствию 29.3 из теоремы 29.1 формулы Ри Р будут общезначимыми, что невозможно на основании определения общезначимости. П Теперь перейдем к установлению взаимосвязей между понятиями семантической и синтаксической непротиворечивости. Наша задача состоит в том, чтобы доказать их эквивалентность. Начнем с достаточно простой, но важной леммы. Лемма 29. 7. Если множество формул имеет модель, то это множество семантически непротиворечиво. Доказательство. Если множество Ф формул имеет модель М, то ни одна формула, выводимая из Ф, не является противоречивой, т.е.
ложной во всякой интерпретации, ибо в противном случае она была бы ложна и в М (что невозможно в силу теоремы 29.1). Это и означает, что Ф семантически непротиворечиво. П Теорема 29.8. Если множество формул семантически непротиворечиво, то оно синтаксически непротиворечиво. Доказательство.
Допустим, что некоторое множество Ф формул узкого исчисления предикатов семантически непротиворечиво, но противоречиво синтаксически. Следовательно, из него выводима некоторая формула Ри ее отрицание — Р. Но тогда из Ф выводима и их конъюнкция (по правилу введения конъюнкции) Р и -Х Но эта формула ложна в любой интерпретации, что означает, что множество Ф семантически противоречиво. Получаем противоречие, доказывающее, что Ф синтаксически непротиворечиво.
П Непосредственно из предыдущих леммы и теоремы вытекает такое следствие. Следствие 29.9. Если множество формул имеет модель, то оно синтаксически непротиворечиво. Теорема Геделя о существовании модели. Утверждение, обратное следствию, также оказывается справедливым. Но с конструктивной точки зрения оно оказывается более глубоким. Смысл его состоит в том, что всякое множество формул не только имеет модель, но эту модель можно конструктивно построить. Доказательство этого факта как раз и заключается в изложении метода такого построения. Это еще одна из замечательных теорем Геделя (теорема о существовании модели), относящаяся к важнейшим теоремам математической логики. Она доказана Геделем в 1930 г.
Теорема 29.10 (теорема Геделя о существовании модели). Любое синтаксически непротиворечивое множеопво Е замкнутых формул узкого исчисления предикатов сигнатуры о имеет модель. Доказательство. Пусть сигнатура о = (ао а~ - '1ь Х Р,, Р„„,), Требуется построить модель М =<М; аь, ап " '1ь,Х " 266 Р,, Р„... >, такую, что М ~ Е (т.е. в алгебраической системе М выполняются все формулы из Е). Эта модель будет строиться из слов некоторого алфавита. Под непротиворечивостью всюду в этом доказательстве будем понимать синтаксическую непротиворечивость.
Прежде всего расширим данную сигнатуру и до о' введением новых индивидных констант: о' = и 0 (со, с„..., с„, ...), где все с; отличны от всех символов из о. Далее будем работать с формулами расширенной сигнатуры и'. Поскольку все такие (замкнутые) формулы являются конечными словами некоторого счетного алфавита, то множество всех таких формул имеет счетную мощность и мы можем все их расположить в последовательность (т.е. занумеровать натуральными числами). Итак, пусть Ао, Ап ..., А„, ... — множество всех предложений (замкнутых формул) сигнатуры о'.
Построим далее последовательность (цепочку) Хо ~ Е, ~ ... ~ Х„~ ... (1) множеств замкнутых формул следующим образом: а) Ео= Е; б) если Е„ Ц (А„) противоречиво, то Е„, ~ = Х„ 0 ( А„); а) если Е„ 0 (А„) непротиворечиво и А„ не начинается с кван- тора существования, то Е„,, = Е„() (А„); г) если Е„() (А„) непротиворечиво и А„м (Лх)(В(х)), то Е„,, = =Е„0 (А„, В(с„)), где со я о'~о — новая константа с наименьшим номером 7г, не встречающаяся в формуле А„и во всех формулах множества Е„. 1) Докажем сначала, что каждое множество Е„построенной последовательности будет непротиворечивым множеством формул исчисления предикатов сигнатуры и'. Доказательство будем вести индукцией по и.
а) Б а з а и н д у к ц и и: и = О. Так как Хо = Е, то по условию Хо непротиворечиво в исчислении предикатов сигнатуры о. Докажем, что оно непротиворечиво и в исчислении сигнатуры о'. ДопУстим пРотивное, т.е. Ео ь- Ги Ео ~- Г, где à — фоРмУла сигнатуры и'. Следовательно, Е ь- Г и Х ь- Г. Это означает, что в Х имеется такое конечное подмножество формул бь ..., б „что бь „,, 6 ь- Р, —,Г.
Пусть В„Вм ..., В, =- à — вывод формулы Риз гипотез бп ..., б„в исчислении предикатов сигнатуры и'. Допустим, что с;„с;„..., с;, — все те новые константы, которые входят в формулы этого вывода. Поскольку Ъ'- и Л-правила вывода к константам не применяются, то, заменив все новые константы с;„с;„..., с, предметными переменными, не входящими в формулы В„Вь ..., В„получим новую последовательность формул Вь Вм ..., В, исчисления предикатов уже сигнатуры и, представляющую собой вывод в этом ис- 2б7 числении ее последней формулы В, ьэ В. Аналогично доказывается, что в исчислении сигнатуры а из множества Е выводима формула ~ Получается противоречие с условием, согласно которому Š— непротиворечиво в исчислении сигнатуры а. Таким образом, Е а непротиворечиво в исчислении сигнатуры а'.
Шаг индукции. Предположим, что Е„непротиворечиво в исчислении предикатов сигнатуры а. Покажем, что тогда таким же свойством обладает и множество Е„,, Согласно определению для него возможны следующие случаи: б) Е„() (А„) противоречиво. В этом случае Е„,, = Е„0 ( А„). Допустим, что последнее множество противоречиво. Тогда Е„, А„»- Ви Е„, 4„»- — балля некоторой формулы Е Тогда для некоторого конечного подмножества Г с Е„: Г, — А„»- Ги Г, 4„»- — Г. Отсюда по производному правилу вывода -вв получим Г»- А„, т.е. Г»- А„, а значит, Е„»- А„. В то же время из условия противоречивости множества Е„() (А„) аналогичные рассуждения приведут к заключению: Е„»- А„.
Эти два заключения говорят о противоречивости множества Е„, что противоречит предположению индукции; в) Е„0 (А„) непротиворечиво и А„не начинаются с квантора существования. В этом случае по определению Е„„, = Е„0 (А„), а значит, Е„,, — непротиворечиво; г) Е„Ц (А„) непротиворечиво и А„начинается с квантора сушествования: А„м (Зх)(В(х)). В этом случае Е„„получается добавлением к Е„двух формул А„и В(с»), где В(с„) получена из В(х) подстановкой константы с» (первой из с»ь с„..., не входящей в А„ и все формулы из Е„) вместо предметной переменной х: Е„,, = = Е„Ц (А„, В(с»)). Допустим, что Е„,, противоречиво, т.
е, Е„,, »- Г, Е Тогда найдется такое конечное подмножество Г ~ Е„, что Г, (Зх)(В(х)), В(с»)» — В и Г, (Эх)(В(х)), В(сД»- -Х Поскольку в выводах этих формул ~Г-правило и Э-правило вывода не применяются к константе сы то, заменив в них эту константу новой переменной у, не участвующей в выводах этих формул, получим выводы, доказывающие что Г, (Зх)(В(х)), В(у„)»- Г, и Г, (Эх)(В(х)), В(у»)»- .Г, где г, получена из Гзаменой константы с» на предметную переменную у (у — фиксированная переменная в этих выводах). Из двух последних выводимостей по производному правилу вывода (введения отрицания -вв) получаем: Г, (Эх)(В(х))» — — В(у).