Лекция 6. Свойства  ИП как ФС. Нормальные формы

1. Полнота. Разрешимость. Непротиворечивость.

2. Доказательство теорем.

3. Нормальные формы для исчисления высказываний и исчисления предикатов.

 

Остановимся теперь на свойствах исчисления предикатов: не­противоречивости и полноте. Как и раньше, будем считать непроти­воречивым такое исчисление, в котором не выводимы никакие две ППФ, из которых одна является отрицанием другой.

Теорема 4. Исчисление предикатов первого порядка непротиворечиво.

Так как аксиомам исчисления предикатов соответствуют выводи­мые ППФ исчисления высказываний, то, очевидно, что всякой вы­водимой ППФ исчисления предикатов соответствует выводимая ППФ исчисления высказываний. Из полноты исчисления высказы­ваний и непротиворечивости исчисления предикатов вытекает, что всякая ППФ исчисления высказываний, выводимая в исчислении предикатов, является выводимой ППФ исчисления высказываний.

Теорема 5. Во всяком исчислении предикатов первого поряд­ка всякая теорема являетсяобщезначимой ППФ.

Обратное утверждение носит название проблемы полноты исчис­ления предикатов в широком смысле, которая решается положи­тельным образом. Впервые проблему полноты в широком смысле в 1930 г. доказал выдающийся немецкий математик и логик К. Гедель.

Теорема 6. (Геделя о полноте). Во всяком исчислении преди­катов первого порядка всякая общезначимая ППФ является тео­ремой.

Что касается проблемы полноты в узком смысле, то для исчис­ления предикатов первого порядка она решается отрицательно. На­помним, что система аксиом называется полной в узком смысле, если нельзя без противоречия присоединить к данной системе никакую другую не выводимую ППФ. Исчисление предикатов оказы­вается неполным в узком смысле, так как к его аксиомам можно присоединить без противоречия недоказуемую в нем следующую ППФ $х А(х) → " x A(x). Считаем, что преди­кат, входящий в данную ППФ, определен на некоторой области V, состоящей из одного элемента. Тогда данная ППФ вырождается в ППФ вида A → A, которая является выводимой ППФ. Следова­тельно, эта ППФ может быть без противоречия присоединена к аксиомам исчисления предикатов.

Проблема нахождения эффективной процедуры (алгоритма) решения задач из данного класса задач (массовая проблема) называется проблемой разрешения этого класса. В интуитивном смысле массовая (алгоритмическая) проблема – это бесконечный класс родственных единичных конкретных проблем, каждая из которых требует ответа «да» или «нет», а метод разрешения массовой проблемы – это единый общий метод, дающий правильный ответ для каждой единичной проблемы. Фактически произвольную массовую проблему можно сформулировать как проблему распознавания некоторого свойства Е элементов данного бесконечного множества А; при этом единичные проблемы, составляющие эту массовую проблему, связываются с элементами множества А, и каждая из них состоит в том, что требуется узнать, обладает или нет свойством Е соответствующий элемент множества А.

При определении формальной системы мы требовали существования разрешающей процедуры для понятия вывода, но для понятия выводимости или доказуемости ППФ этого требования не выставляли. Мы отмечали, что формальная система, для которой существует эффективная разрешающая процедура, позволяющая узнать по данной ППФ, является ли она теоремой или нет, называется разрешимой, в противном случае такая формальная система неразрешима. Примером разрешимой формальной системы является исчисление высказываний. Для него мы имеем эффективную процедуру разрешения, выраженную в виде истинностных таблиц, по которым можно легко судить, является ли ППФ теоремой (общезначимой ППФ) или нет.

Исчисление предикатов первого порядка – пример неразрешимой формальной системы. Впервые доказал существование неразрешимых алгоритмических проблем в 1936 г. американский логик Алонзо Черч. В доказанной им теореме говорится об отсутствии эффективной процедуры при решении вопроса относительно произвольной ППФ формальной системы, содержащей арифметику натуральных чисел, является ли эта ППФ теоремой. В доказательстве Черча были использованы идеи Геделя, оно было тесно связано с его знаменитой теоремой о неполноте, точнее, с двумя теоремами, доказанными им в 1931 г. Первая теорема тесно связана с явлением алгоритмической неразрешимости, вторая содержит более тонкое утверждение о формальных системах. Содержание первой теоремы о неполноте (если ограничиться натуральной арифметикой) заключается в следующем. Пусть FS – арифметическая формальная система, содержащая аксиомы Пеано. При этом предполагается, что FS корректно описывает арифметику, т. е., что все формулы, выводимые в FS, являются истинными утверждениями о натуральных числах. Для любой такой системы первая теорема Геделя утверждает, что не все истинные ППФ арифметики доказуемы в FS, т. е. в арифметике имеется некоторое утверждение. А, обладающее тем свойством, что ни А, ни А не являются теоремами. Другими словами, понятие истинности ППФ арифметического языка шире, чем понятие доказуемости в любой формальной системе (если последняя корректна). Более того, если в арифметике имеются недоказуемые (неразрешимые) утверждения, то присоединение к такой теории неразрешимого утверждения в качестве аксиомы снова приводит к теории, являющейся формализацией арифметики, в которой по-прежнему имеются неразрешимые утверждения. Таким образом, теорема Геделя говорит не только о неполноте, но и о непополнимости формальной арифметики.

Во второй своей теореме Гедель показал невозможность доказательства непротиворечивости формальной теории, включающей формальную арифметику, конструктивными методами, формализуемыми в рамках самой этой теории.

Из геделевского доказательства неполноты арифметики, по существу, вытекала неразрешимость проблемы идентификации истинных утверждений элементарной арифметики.

А. Черч доказал, что для исчисления предикатов первого порядка также не существует алгоритма, распознающего выводимые утверждения.

Благодаря работам К. Геделя и А. Черча понятие алгоритмической неразрешимости было уточнено с привлечением понятий нумераций и частичной рекурсивности. Впоследствии английский математик А. Тьюринг предложил другое уточнение понятия неразрешимости, использовав понятие машины Тьюринга. Эти уточнения, как оказалось, приводят к равнообъемным понятиям неразрешимости. Известны и другие уточнения, дающие тот же результат: нормальные алгоритмы А. А. Маркова, формальные исчисления американского математика Э. Поста и другие.

В 1947 г. независимо друг от друга А. А. Марков и Э. Пост доказали алгоритмическую неразрешимость проблемы тождества в полугруппах. Это был первый пример неразрешимой алгоритмической проблемы, возникшей вне области математической логики. Известно, что всякая полугруппа может быть задана с помощью систем образующих и определяющих соотношений. Если полугруппа не является свободной (т. е. существует хотя бы одно соотношение между ее образующими), то представление любого ее элемента через образующие неоднозначно. Поэтому возникает задача: для данных двух выражений, представляющих собой произведения образующих, узнать, равны ли эти произведения между собой. В том случае, когда полугруппа задается конечными системами образующих и определяющих соотношений, нужно найти алгоритм, решающий любую такую задачу.

А. А. Марков и Э. Пост построили полугруппы с неразрешимой проблемой тождества. Аналогичная проблема для групп – проблема тождества в группе – занимает важное место в теории групп. Советский математик П. С. Новиков в 1952 г. доказал алгоритмическую неразрешимость проблемы тождества теории групп, заключающуюся в невозможности распознавания эквивалентности слов для ассоциативных исчислений специального типа. Проблема эквивалентности слов для ассоциативных исчислений, т. е. исчислений, состоящих из совокупности слов в данном алфавите вместе с системой допустимых подстановок типа P_i ↔ Q_i, была впервые сформулирована еще в 1914 г. норвежским математиком Туэ. С тех пор предпринимались многие попытки построить такую общую эффективную процедуру, которая для любого ассоциативного исчисления и любой пары слов в нем позволила бы установить, эквивалентны эти слова или нет, т. е. существует ли или нет дедуктивная цепочка слов, ведущая как от одного слова к другому, так и обратно. Были построены конкретные примеры ассоциативных исчислений, для каждого из которых проблема эквивалентности слов оказалась неразрешимой. Была доказана также алгоритмическая неразрешимость ряда проблем в теориях полугрупп, групп, структур, колец, полей и других алгебраических систем.

Почти все разделы математики изобилуют массовыми проблемами. Долго не поддавалась решению десятая проблема Гильберта, суть которой состоит в следующем: требуется найти эффективную процедуру, позволяющую для любого диофантового уравнения выяснить, имеет ли оно целочисленное решение. Напомним, что диофантовым называется уравнение вида P = 0, где P – многочлен с целочисленными коэффициентами. Для частного случая диофантова уравнения с одним неизвестным такой алгоритм известен, и он сводится к тому, что если уравнение с целочисленными коэффициентами имеет целый корень x₀, то обязательно свободный член в этом уравнении делится на x₀. Что касается общего случая для множества целочисленных многочленов от произвольного числа неизвестных, то вплоть до 1969 г. эта проблема, хотя над ней работали многие выдающиеся математики современности, не была решена. И только в конце 1969 г. советскому математику Ю. В. Матиясевичу удалось доказать, что эта проблема алгоритмически неразрешима.

В заключение отметим, что понятие эффективной процедуры является метаматематическим понятием. Что это значит? Язык, на котором дается описание какой-либо формальной системы, называется метаязыком в отличие от предметного языка или языка – объекта, который используется для высказываний внутри самой формальной системы. Таким образом, если мы возьмем высказывание типа «Исчисление предикатов первого порядка непротиворечиво», то это есть высказывание, сделанное на метаязыке. В свою очередь, высказывание типа " x(A(x) → B(x)) → ($x A(x) → $x B(x)) есть высказывание, записанное на предметном языке.

Отсюда понятие теоремы (выводимой ППФ) самой формальной системы нельзя путать с теоремой, описывающей какие-либо свойства формальной системы, последняя есть метатеорема. Вышеприведенное высказывание, записанное на русском языке о непротиворечивости исчисления предикатов первого порядка, есть метатеорема, высказывание же, записанное в терминах ", $, →, , &, Ú, ( ) есть теорема исчисления предикатов.

Нормальные формы.

При разработке методов автоматического доказательства теорем необходимо все формулы, как логики высказываний, так и логики предикатов первого порядка, представить в некотором стандартном виде. В дальнейшем слова «первого порядка» будут опускаться, а логика предикатов считаться расширением логики высказываний за счет введения предикатов и кванторов общности " и кванторов существования $. Простые высказывания в логике высказываний будем называть атомами, принимающими два значения: истина (И) или ложь (Л). Символы И и Л называются истинностными значениями.

Сложные высказывания (формулы) будут образовываться из простых с помо­щью логических связок Ø (не), & (конъюнкция), Ú (дизъюнкция), ® (импликация), « (эквивалентность).

Ранее мы ввели понятие нормальных форм для исчисления высказываний.

Основные определения:

Формула логики высказываний F представлена в конъюнктивной нормальной форме (КНФ) тогда и только тогда, когда она имеет форму F = B₁ & B₂ & … & B_m, где каждая из B_i (i = ) есть дизъюнкция литер.

Аналогично говорят, что формула логики высказываний F представлена в дизъюнктивной нормальной форме (ДНФ) тогда и только тогда, когда она имеет форму F = A₁ Ú A₂ Ú … Ú A_n, где каждая из A_i (i = ) есть конъюнкция литер.

Алгоритм преобразования произвольной формулы исчисления высказываний в нормальную форму состоит из следующих шагов.

Шаг 1. Избавляемся от связок эквивалентность и импликация, применяя формулы

                   А « В = (А ® В) & (В ® А).

                   А ® В = Ø А Ú В.

Шаг 2. Продвигаем знаки отрицания до атомов, используя правила Де-Моргана, также снимаем двойные отрицания.

                   Ø Ø А = А.

                    законы Де-Моргана.

Шаг 3.        Для получения КНФ применяем правило внесения в скобки

                   А Ú (В & С) = (А Ú В) & (А Ú С)  .

                   Для получения ДНФ многократно применяем правило раскрытия скобок

                   А & (В Ú С) = А & В Ú А & С.

 

Дизъюнктом называется формула вида L₁ Ú L₂ Ú … Ú L_k, где L_i (i = ) – произвольная литера. Дизъюнкт, не имеющий литер, называется пустым дизъюнктом (ÿ ). По определению он всегда ложен.

Дизъюнкты, соединенные знаком &, образуют КНФ. Существует простой алгоритм равносильного преобразования произвольной бескванторной формулы в КНФ (см. также алгоритм получения КНФ и ДНФ для логики высказываний, данный ранее). Здесь дадим его в развернутом виде.

Алгоритм приведения к КНФ.

Шаг 1. Дана формула F, составленная из литер с применением связок & и Ú.

Предполагается, что в формуле исключены скобки между одинаковыми связками, т. е. нет выражений вида

    F₁ Ú (F₂ Ú F₃),   (F₁ Ú F₂) Ú F ₃,

или   F₁ & (F₂ & F₃),   (F₁ & F₂) & F ₃.

Шаг 2. Найти первое слева вхождение двух символов Ú ( или )Ú (здесь предполагается, что скобка не является скобкой атома). Если таких вхождений нет, то СТОП: формула F находится в КНФ.

Шаг 3. Пусть первым вхождением указанной пары символов является Ú (. Тогда взять наибольшие формулы F₁, F₂, …, F_r, Y₁, Y₂ …, Y_s такие, что в F входит формула F₁ = F₁ Ú F₂ Ú F_r Ú (Y₁ & Y₂ & … & Y_s), которая связана с вхождением Ú (. Заменить формулу F₁ на формулу (F₁ Ú F₂ Ú … Ú F_r Ú Y₁) & (F₁ Ú F₂ Ú … Ú F_r Ú Y₂) & … & (F₁ Ú F₂ Ú … Ú F_r Ú Y_s).

Шаг 4. Пусть первым вхождением является )Ú. Тогда взять наибольшие формулы F₁, F₂, …, F_r, Y₁, Y₂ …, Y_s такие, что в F входит формула F₁ = (Y₁ & Y₂ & … & Y_s) Ú F₁ Ú F₂ Ú …Ú F_r, связанная с вхождением )Ú. Заменить F₁ на формулу (Y₁ Ú F₁ Ú F₂ Ú …Ú F_r) & (Y₂ Ú F₁ Ú F₂ Ú … Ú F_r) & … & (Y_s Ú F₁ Ú F₂ Ú … Ú F_r).

Шаг 5. Перейти к шагу 2.

Пример 1. Преобразуем формулу F = P(x) Ú P(a) Ú ((R(x, y) Ú Ø Q(y)) & P(x) & (R(x, a) Ú (Ø Q(y) & P(a)))) в КНФ.

F = (P(x) Ú P(a) Ú R(x, y) Ú Ø Q(y)) & (P(x) Ú P(a) Ú P(x)) & (P(x) Ú P(a) Ú R(x, a) Ú (Ø Q(y) & P(a))) =
 (P(x) Ú P(a) Ú R(x, y) Ú Ø Q(y)) & (P(x) Ú P(a)) & (P(x) Ú P(a) Ú R(x, a) Ú Ø Q(y)) & (P(x) Ú P(a) Ú R(x, a) Ú P(a)) =
(P(x) Ú P(a) Ú R(x, y) Ú Ø Q(y)) & (P(x) Ú P(a)) & (P(x) Ú P(a) Ú R(x, a) Ú Ø Q(y)) & (P(x) Ú P(a) Ú R(x, a)).

Здесь чертой подчеркнуты вхождения Ú (. Кроме того, в алгоритме надо предусмотреть приведение подобных членов, а также всевозможные склеивания и поглощения.

 

 

⇐ Предыдущая6789101112131415Следующая ⇒

Поделиться:

Воспользуйтесь поиском по сайту: