Введение в логику

Введение

В математике при помощи аксиом мы определяем объекты и их свойства. Затем, используя логические рассуждения, доказываем новые утверждения и называем их теоремами. Впервые подобная схема проявилась в книгах Евклида, в частности, при описании геометрии. Со временем возникла потребность так формализовать построение теории и доказательства теорем, чтобы ни какие незаметно привнесённые "очевидности" не портили её логическую стройность. В частности, по-возможности необходимо отказаться от естественного языка с присущей ему неоднозначностью. Блестящим примером подобного подхода явились "Основания геометрии" и последующие работы Давида Гильберта.

Появление компьютеров и начала исследований по искусственному интеллекту, привели к активному применению методов математический логики для описания "обыденных знаний". Во многих предметных областях (пространственные и временные отношения, родственные связи между людьми и т.п.) свойства различных объектов можно компактно описать пользуясь математическими обозначениями. А при помощи методов логического вывода, компьютер может проявлять определённую "разумность" извлекая из базы "аксиом" знания, которые там явным образом не содержатся.

Предметы и теории

Объектом исследования математических теорий или теорий формализации "обыденных знаний" являются чётко определённые сущности (предметы) и отношения между ними. Предметы могут объединяться в различные групы. Например, в геометрии рассматриваются предметы трёх видов: точки, прямые и плоскости. В арифметике все предметы одного типа - это числа. При формализации родственных отношений (дети, отцы, матери, братья и т.п.) предметами являются люди.

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

Предикат - это логическая функция принимающая значение истина при одних значениях предметных переменных и ложь - при других. Например в арифметике предикат x<y или LT(x,y) будет истинным, если число x меньше числа y. В системе человеческих отношений можно ввести предикат Parent(x,y), равный истине, если человек x является родителем человека y.

Предметная функция - это правило которое ставит в соответствие одной предметной величине другую. Например, в арифметике функция сложения add(x,y) любым двум числам x и y ставит в соответствие третье число (их сумму). Для человеческих отношений вместо предиката Parent можно ввести функцию y=parent(x), которая для каждого человека x указывает его родителя y. При этом, хотя предикат Son(x,y) = "x является сыном y-ка" хорошо определён, введение функции x=son(y) затруднительно y-к может иметь несколько сыновей).

Для предикатов и функций с двумя аргументами часто используется операторная запись. Например, утверждение (предикат): "точка x принадлежит прямой y" можно записать как On(x,y) или как x ∈ y. Аналогично функция сложения add(x,y) обычно обозначается как x+y.

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

Предикаты и функции

Рассмотрим теорию с конечной предметной областью в которой есть 3 предмета вида A и 6 предметов вида B. Пронумеруем их целыми числами: A={1,2,3} и B={1,2,3,4,5,6} и составим 18=3*6 различных упорядоченных пар aibj (такое множество называется прямым произведением A×B множеств A и B). Определим предикат P(a,b), отобрав 8 из 18 пар которым он удовлетворяет (при которых он истинен):
P: {(1,2), (1,3), (1,4), (1,5), (1,6), (2,4), (2,6), (3,6) }
Слева от таблицы по вертикали расположены элементы множества A, а сверху по горизонтали -- множества B. Каждая ячейка таблицы является элементом множества A×B всех пар. Звёздочками помечены элементы, отобранные в подмножество P(a,b). В арифметике подобный предикат может обозначать "число a - собственный делитель b, не равный ему". Например P(2,4) истинно, а P(3,4) - ложно.

Предикат F(x,y), обозначаемый также y=f(x), называется функциональным, если для каждого x утверждение F(x,y) истинно для не более одного y. Ниже первая таблица определяет функциональный предикат, тогда как вторая функциональным не является:

Действительно, в первой строке второй таблицы стоят две звёздочки, поэтому нельзя определить функцию, которая первому элементу x1 множества X ставит в соответствие один элемент y1 = f(x1) множества Y. Если мы переставим местами элементы в отношении (перевернём таблицу на 90 градусов) то получится обратная к f(x) функция. Не у каждой функции есть обратная (например, её нет выше у первой таблицы).

Бинарные функции двух аргументов z=f(x,y) любой паре прямого произведения двух множеств X и Y ставят в соответствие элемент из третьего множества Z (часто бинарные функции задаются на элементах одного множества f: X×X → X). Бинарные функции эквивалентны предикату с тремя аргументами F(x,y,z), который для каждого x,y истинен только для одного z.

Таким образом, предикаты являются более общими конструкциями, чем функции. Однако, когда они обладают функциональным свойством (и соответственно имеют мало "звёздочек") удобнее использовать предметную функцию. Для определения последней при помощи таблицы достаточно двух строчек: перечисления области определения (всех x) и области значений (соответствующие каждому x значения y).

Если предметов много или тем более бесконечно много, расставлять звёздочки в таблицах проблематично. Поэтому при задании предиката формулируют те или иные свойства (аксиомы), которым удовлетворяет данный предикат. Например, для предиката P(x,y) между элементами одного множества можно задать свойство симметрии: P(x,y) = P(y,x). Равенство означает, что если P(x,y) - истинно, то и P(y,x) будет истинным. Это соответствует квадратной таблице, симметричной относительно диагонали, идущей из левого верхнего угла в правый нижний. Величины x,y - это предметные переменные, означающие любой предмет теории.

Логические операции

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

A & B    : ''и''   (и A и B = оба)
A ∨ B    : ''или'' (или A или B, или оба = хотя бы одно)
¬A       : ''не''  (не A = утверждение A ложно).
Например, пусть в геометрии введен предикат x ∈ g принадлежности точки x прямой g. Тогда можно определить предикат от трёх сущностей: "прямая g проходит через точки x и y" следующим образом: 
L(g, x, y) : (x ∈ g) & (y ∈ g).
Двоеточие означает, что везде, где встречается предикат L(g,x,y), его необходимо заменить на строку (x ∈ g) & (y ∈ g).

Логические связки (операции) определяются при помощи таблиц истинности, в которых перечисляются значения истина (И) и ложь (Л) каждого аргумента операции и указывается какое значение принимает операция:

Кроме логических "и", "или", "не" определена операция следования (импликация): A → B и следования в обе стороны: A ↔ B. Импликация ложна только если первый аргумент истинен, а второй ложен: И → Л это Л ("из истины нельзя вывести ложь"). Если ли же из истины выводится истина, то это истинное "следование" (И → И это И). Из лжи можно вывести что угодно, поэтому Л → Л и Л → И будут истинными. Стоит проанализировать утверждение "очевидно верное" в арифметиике при произвольном числе x: ''(x<2) → (x<4)'', положив x=1,3,5.

Выражение ¬A ∨ B имеет такую же таблицу истинности, как и A → B, а A ↔ B эквивалентно (A → B) & (B → A). Поэтому это производные логические связки, однако они играют важную роль при записи аксиом.

При помощи таблиц истинности можно получать логичекие значения сотавных формул. В качестве приимера докажем, что выражение (A → B) ↔ (¬A ∨ B) является тавтологией, т.е. истинно при всех значениях входящих в неё высказываний. Для этого логические значения И,Л сначала подписываются под каждым логическим высказыванием, затем послеедовательно под знаками всех логических операций:

Любое выражение алгебры логики можно представить в виде дерева задающего последовательность вычислений значения этого выражения:

В вершине дерева стоит последняя выполняющаяся функция, а внизу, на "листьях" - высказывания. Вычисление выражения идёт по дереву снизу -- вверх. Считается, что отрицание имеет самый высокий приоритет, поэтому в выражении A ∨ ¬A сначала проводится отрицание утверждения A, а затем объединение логическим "или".

Булева алгебра

Из таблиц истинности следует, что логические "и", "или" являются симметричными операциями. С помощью этих же таблиц несложно проверить, что эти операции ассоциативны: 

A & B ≡ B & A,              A & (B & C) ≡ (A & B) & C,
A ∨ B ≡ B ∨ A,              A ∨ (B ∨ C) ≡ (A ∨ B) ∨ C.
Символ эквивалентности "≡" означает совпадение таблиц истинности логических выражений слева и справа от него. Ещё одно алгебраическое свойство - это взаимная дистрибутивность логических операций: 
A & (B ∨ C) ≡ (A & B) ∨ (A & C),
A ∨ (B & C) ≡ (A ∨ B) & (A ∨ C).
Более специфичными являются правила поглощения: 
A & A ≡ A,        (A ∨ B) & A ≡ A,
A ∨ A ≡ A,        (A & B) ∨ A ≡ A.
В обыденном понимании, например, логического "и" эти правила вполне естественны: A и A - это A.

Следующая группа правил связана с отрицанием (правила де-Моргана и двойное отрицание): 

¬(A & B) ≡ ¬A ∨ ¬B,         ¬(¬A) ≡ A,
¬(A ∨ B) ≡ ¬A & ¬B.

Последний набор правил называется законом исключения третьего: 

A ∨ ¬A,               A & (¬A ∨ B) ≡ A & B,
                      A ∨ (¬A & B) ≡ A ∨ B.
В бинарной логике и в конечной предметной области первое утверждение (или A или не A) всегда истинно. В многозначных логиках это уже не так. Определённые трудности этого закона появляются и в теориях с бесконечным числом предметов. Стоит обратить внимание, что все правила алгебры, кроме A ∨ ¬A инвариантны относительно перестановки операций & и ∨.

КНФ и ДНФ

Коньюктивная нормальная форма (КНФ) - это преобразование исходного выражения при помощи алгебры логики в следующий вид: 

(A1 ∨ A2 ∨ A3 ∨ ...) & (B1 ∨ B2 ∨ B3 ∨ ...) &  (C1 + C2 + C3 + ...) & ...,
где в скобках стоят "суммы" логических "или" (дизьюнкций) простых высказываний A,B,... или их отрицаний ¬A, ¬B, .... Для такого преобразования, сначала необходимо рекурсивно подставить определения для следований в обе стороны и в одну, затем при помощи правил де-Моргана и двойного отрицания прижать знак отрицания к высказываниям и, наконец, применить закон дистрибутивности по отношению к дизьюнкции: 
1) A ↔ B ≡ (A →  B) & (B → A);    A → B ≡ ¬A ∨ B;
2) ¬¬A ≡ A;  ¬(A&B) ≡ ¬A ∨ ¬B;   ¬(A∨B)  ≡ ¬A & !B;
3) A∨(B&C) ≡ (A∨B)*(A∨C);         (B&C)∨A ≡ (B∨A)&(C∨A)
В результате получится "произведение" логических "и" (конъюнкции) "сумм" логических "или" (дизьюнкций).

Аналогично определяется и получается дизьюнктивная нормальная форма, в которой символы ∨, & переставлены местами.

Иногда необходимо проверить совпадение таблиц истинности двух выражений. Каждое из них можно привести к конъюнктивной нормальной форме (КНФ). Однако в таком виде их ещё сравнивать рано. Дело в том, что одна и та же формула может иметь различные КНФ. Например, в силу справедливости закона поглощения, выражение (A ∨ B) & A это тоже самое, что и просто A. Поэтому для подобных задач формулу записанную в КНФ необходимо представить в совершенной конъюнктивной нормальной форме (СКНФ). Под этим подразумевается следующее. Если формула зависит, например, от трёх высказываний A, B и C, то каждая из этих букв должна встречаться хотя бы один раз в каждой из скобок соединённых логическим "и". В случае когда в конъюнкте нет, скажем буквы B, мы можем при помощи ''или'' в него добавить всегда ложную формулу B & ¬B которая истинность КНФ не изменит. Например (двойная стрелка означает преобразование выражения): 

  (A ∨ B) & A    ⇒   (A ∨ B) & [A ∨ (B & ¬B)]   ⇒   (A ∨ B) & (A ∨ B) & (A ∨ ¬B).
Если две формулы имеют одинаковые СКНФ, то они имеют и одинаковые таблицы истинности.

КНФ играет важную роль в логических рассуждениях. Любое утверждение (аксиома) представленное в КНФ разбивается на более элементарные, так как логическое "и" истинно только, если истинны каждые "сомножители" коньюнкции.

Кванторы ∀ и ∃

При формулировке утверждений в теории необходимы также следующие заменители слов: 

∀ : ''любой'' = ''каждый'' = ''для всех''  = квантор всеобщности
∃ : ''существует по крайней мере один''    = квантор существования
С их помощью можно, например, записать фразу "для любых точек x и y существует по крайней мере одна прямая g, которая через них проходит": 
∀x ∀y ∃g L(g,x,y),
где предикат L(g,x,y): (x ∈ g) & (y ∈ g) был определён ранее.

Предметные переменные, стоящие с квантором являются связанными. Например, рассмотрим конечную предметную область, состоящую только из трех предметных констант x = {1,2,3}. Тогда запись ∃x, ∀x на самом деле означает: 

∃x A(x) ≡ A(1) ∨ A(2) ∨ A(3),
∀x A(x) ≡ A(1) & A(2) & A(3).
В первой строке утверждается, что "существует такой x, что некий предикат A(x) истинен". Это значит, что истинно или A(1), или A(2), или A(3) (хотя бы что-то одно из {1,2,3}, которое и ''существует''). Аналогично во второй строке, для квантора ''каждый'' истинными должны быть и A(1), и A(2), и A(3), т.е., все. Таким образом, наличие в формуле переменной, связанной с квантором, аналогично индексу суммирования, и выражение (после явной записи "суммы") от нее не зависит. Как и суммационный индекс, связанная переменная может быть переобозначена в любую букву, которая еще не используется в выражении.

Пользуясь алгеброй логики из записью ∃x, ∀x при помощи "∨", "&", несложно получить тождества: 

∃x ∃y A(x,y)  ≡   ∃y ∃x A(x,y),       ¬( ∃x A(x) ) ≡ ∀x ¬A(x),
∀x ∀y A(x,y)  ≡   ∀y ∀x A(x,y),       ¬( ∀x A(x) ) ≡ ∃x ¬A(x).
Постулируется их справедливость и для бесконечной предметной области. В вербальном варианте они вполне естественны. Например, последнее соотношение: "не для каждого x справедливо A(x)" эквивалентно "существует такой x, что A(x) ложно".

Кванторы ∃x и ∀y не перестановочны и их последовательность важна. Так ∃x∀y A(x,y) означает, что "существует такой x, что для любого y справедливо утверждение A(x,y)". Запись же ∀y∃x A(x,y) звучит: "для каждого y существует некоторый x" (один или несколько).

Вывод для высказываний

После того как теория сформулирована при помощи некоторых аксиом (формально записанных утверждений относительно предикатов и предметных функций) из неё можно делать логические выводы. Рассмотрим сначала константные предикаты (не зависящие от предметных переменных). Такие предикаты называются высказываниями. Например A: "сейчас светит солнце" или B: "все блондинки умны".

Правило вывода modus ponens (лат.) соответствует вербальному: "если из A следует B и справедливо A, то справедливо и B": 

A, A → B  ⇒ B.
Двойная стрелка означает вывод (получение) утверждения B из двух утверждений A и A → B. При помощи правил алгебры логики можно проверить, что: A & (A → B) ≡ A & (¬A ∨ B) ≡ B.

Более общим является правило вывода резолюции: 

A ∨ B,   ¬B ∨ C  ⇒  A ∨ C.
Как и любое правило вывода оно сохраняет истинность исходных посылок. Действительно, пусть B ≡ И. Тогда ¬B ≡ Л, и если вторая посылка истинна, то C ≡ И и понятно, что истинно следствие. Аналогично, если B ≡ Л, вторая посылка будет истинной, а при истинности первой должно выполняться A ≡ И. Поэтому выводимое выражение снова истинно.

Докажем, например, справедливость следующего рассуждения (если из A следует B, и из B следует C, то справедливо, что из A следует C): A → B, B → C ⇒ A → C. Выразим обе посылки через "∨", "¬", и воспользуемся резолюцией: 

¬A ∨ B,   ¬B ∨ C    ⇒    ¬A ∨ C.
Так как в посылках встречается и B и ¬B мы их объединяем, выбрасывая B.

Метод резолюции

Резолюция активно используется в различных компьютерных системах автоматических доказательств. Предположим, что у нас есть множество формул A1, A2, ..., которые в данной теории считаются истинными (аксиомы). Мы хотим вывести из них формулу F. В хорошей теории (полной и непротиворечивой), если формула выводима (истинна), то её отрицание будет противоречить исходной системе аксиом, т.е. множество формул ¬F, A1, A2,... противоречиво. В частности из этого множества будет следовать некоторая формула R и одновременно её отрицание ¬R.

Повторим доказательство рассуждения A → B, B → C ⇒ A → C. проведенного выше, используя метод от противного. Возьмём отрицание доказываемой формулы ¬(A → C) ≡ A & ¬C. Это утверждение будет истинно, если истинна каждая формула соединённая логическим "и" &. В результате имеем следующее множество формул противоречивость которых необходимо доказать: ¬A∨B, ¬B∨C, A, ¬C. Будем попарно к ним применять резолюцию. Первые две породят ¬A∨C. Первая и третья дадут: B, а вторая и четвёртая: ¬B: 

¬A∨B, ¬B∨C,  A, ¬C    ⇒   ¬A∨B, ¬B∨C,  A, ¬C, ¬A∨C,   B,  ¬B.
Ещё одно применение резолюции к формулам B и ¬B даст "пустую формулу". Это и означает, что мы пришли к противоречию.

Может возникнуть вопрос: почему необходимо применять доказательство от противного, если прямым выводом можно получить требуемую формулу A → C? Ответ простой. Прямой вывод оказывается не целенаправленным. Из аксиом теории, при помощи вывода, можно получать быстро увеличивающееся множество "не нужных" теорем прежде чем "случайно" встретится нужная нам формула. В методе от противного, мы сразу помещаем её отрицание в список формул, и за конечное число шагов приходим к противоречию (если формула выводима).

Сколимизация

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

1. Формула записывается в терминах операций ¬, ∨, & в предварённой форме, когда все кванторы вынесены влево (предваряют формулу).

2. Если в формуле есть только кванторы всеобщности, мы их опускаем, считая, что свободная переменная обозначает "любую". Так, вместо ∀x ∀y A(x,y) просто пишем A(x,y).

3. Для формулы вида ∃x A(x) мы вводим некоторую константу a, которая отражает тот факт, что x существует, и получаем A(a). Если перед квантором существования (слева) стоят несколько кванторов всеобщности ∀x ∀y ∃z A(x,y,z) вводится новая предметная функция z=f(x,y) которая определяет какое z существует при данных x и y. В результате получаем A(x,y,f(x,y)).

Затем формулв приводится к конъюнктивной нормальной форме и разбивается на элементарные утверждения (которые были связаны логическим "и").

> Арифметический парсер