Формальный язык логики высказываний

Таблицы истинности в логике высказываний позволяют ответить на многие вопросы. Например, является ли данная формула тавтологией, противоречием или выполнимой формулой; влечёт ли она логически другую формулу; являются ли две формулы логически эквивалентными. Однако более сложные вопросы логики высказываний не решаются с помощью таблиц истинности. Поэтому в данном параграфе будет рассмотрен новый метод решения логических задач. Это – метод формальных теорий. Хотя основные вопросы в логике высказываний могут быть решены с помощью таблиц истинности, мы проиллюстрируем аксиоматический метод на этой простой ветви логики.

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

Определение 1: Формальная (аксиоматическая) теория считается определенной, если выполнены следующие условия:

1) Задано счетное множество символов – алфавит теории. Конечные последовательности символов алфавита называются выражениями теории.

2) Имеется подмножество выражений теории, называемых формулами теории (грамматика языка).

3) Выделено некоторое множество формул, называемых аксиомами теории.

4) Имеется конечное множество отношений между формулами, называемых правилами вывода (синтаксис языка теории). Для каждой из формул и данной формулы можно выяснить, является ли данная формула в одном из отношений с формулами. Если да, то формулу называют непосредственным следствием исходных формул по данному правилу вывода.

Определение 2: Выводом называется всякая последовательность формул , такая, что для любого формула является либо аксиомой данной теории, либо непосредственным следствием каких-либо предыдущих формул по одному из правил вывода.

Определение 3: Формула в некоторой теории называется теоремой теории, если существует вывод в данной теории, в котором последней формулой является ; такой вывод называется доказательством формулы .

Определение 4: Формула называется следствием формул множества тогда и только тогда, когда существует такая последовательность формул, что. И для каждого формула является либо аксиомой, либо формулой из множества, либо непосредственным следствием некоторых предыдущих формул по одному из правил вывода. Такая последовательность называется выводом из множества. Формулы из множества называются гипотезами, или посылками вывода.

Для краткой записи утверждения « является следствием » будем использовать обозначение: ├ . Если множество конечно, т. е. , будем писать: ├ . Если - пустое множество, то ├ имеет место тогда и только тогда, когда является теоремой. В этом случае принято писать: ├ . Эта запись означает, что - теорема.

Приведём простые свойства выводимости из посылок.

1) Если и ├ , то ├ .

Т. е., если выводимо из множества посылок , то останется выводимым, если добавить в новые посылки.

2) ├ тогда и только тогда, когда в найдётся конечное подмножество , для которого ├ .

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

3) Если ├ и ├ для любого из , то ├ .

Смысл этого утверждения состоит в том, что если выводимо из и каждая формула, содержащаяся в , выводима из , то выводимо из .

Теперь перейдём к изложению формальной аксиоматической теории для исчисления высказываний.

1) Алфавитом теории являются символы: , , , и буквы с целыми положительными индексами: Символы и называют примитивными связками (логические операции отрицание и импликация), а буквы – пропозиционными буквами.

2) а) Каждая пропозиционная буква есть формула.

б) Если и – формулы, то и – тоже формулы.

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

3) Каковы бы ни были формулы теории , следующие формулы есть аксиомы в теории :

(А1) ;

(А2) ;

(А3) .

4) Единственным правилом вывода служит правило modus ponens: « есть непосредственное следствие и ». Это правило называют также правилом отделения, будем его сокращенно обозначать: Далее будем придерживаться соглашений о сокращении числа скобок.

Отметим, что бесконечное множество аксиом теории задано с помощью всего лишь трех схем аксиом , , , каждая из которых порождает бесконечное множество аксиом.

Мы строим систему таким образом, чтобы класс всех теорем этой теории совпадал с классом всех тавтологий исчисления высказываний.

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

означает ;

означает ;

означает .

Другими словами, мы выбираем новые названия для некоторых выражений языка теории .

Замечание: Слово «вывод» (или «доказательство») употребляется в двух различных смыслах. Во-первых, оно употребляется как название конечных последовательностей формул теории . Во-вторых, оно означает последовательность предложений разговорного языка (дополненного техническими терминами), о которой предполагается, что она служит достаточно обоснованной аргументацией в пользу утверждения о теории . Мы изучаем язык теории с помощью метаязыка. Этот метаязык можно было бы формализовать, но тогда рассуждения о нём нужно было бы проводить в новом метаязыке и т. д.

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

Теорема 1: Для любой формулы в теории формула выводима.

Доказательство: Построим вывод формулы в теории .

1. (схема аксиом (А2)).

2. (схема аксиом (А1)).

3. (из 1 и 2 по правилу вывода ).

4. (схема аксиом (А1)).

5. (из 3 и 4 по правилу вывода ).

Подобным образом доказываются другие теоремы этой теории.

Теорема 2: (теорема дедукции, Эрбран (1930 г.)).

Если - множество формул, и – формулы и , ├ , то ├ .

В частности, если ├ , то ├ .

Доказательство: Пусть вывод из . Докажем, что ├ индукцией по .

При формула должна быть либо формулой из множества , либо аксиомой теории , либо должна совпадать с . По схеме аксиом (А1): есть аксиома. Поэтому, в первых двух случаях имеем: ├ по правилу вывода . В третьем случае, т. е. когда совпадает с , согласно теореме 1, имеем: ├ . Следовательно, ├ . Таким образом, теорема доказана для случая, когда длина вывода .

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

Замечание: Доказательство позволяет по данному выводу из построить вывод из , причём при доказательстве используются только схемы аксиом (А1) и (А2).

Следствие 1: ├ .

Доказательство:

1) - гипотеза.

2) - гипотеза.

3) - гипотеза.

4) - выводится из пунктов 1 и 3 по

5) - выводится из пунктов 2 и 4 по

Таким образом, ├ . Отсюда по теореме дедукции имеем: ├ .

Следствие 2: ├ .

Доказательство:

1) - гипотеза.

2) - гипотеза.

3) - гипотеза.

4) - выводится из пунктов 1 и 3 по

5) - выводится из пунктов 4 и 2 по

Значит, ├ . Применяя теорему дедукции, получаем: ├ .

Теорема 3: ├ .

Доказательство:

1) - схема аксиом (А3).

2) - теорема 1.

3) - следствие 2 из теоремы дедукции, применённое к пунктам 1 и 2.

4) - схема аксиом (А1).

5) - следствие 1 из теоремы дедукции, применённое к пунктам 4 и 3.

Теорема доказана.

Теорема 4: ├ .

Доказательство:

1) - схема аксиом (А3).

2) - теорема 3.

3) - выводится из пунктов 1 и 2 по правилу вывода .

4) - схема аксиом (А1).

5) - следствие 1 из теоремы дедукции, применённое к пунктам 4 и 3.

Теорема доказана.

Замечание (метаязык): Из теорем 3 и 4 следует, что в теории доказан закон двойного отрицания.

Теорема 5: ├ .

Доказательство:

1) - гипотеза.

2) - гипотеза.

3) - схема аксиом (А1).

4) - схема аксиом (А1).

5) - выводится из пунктов 3 и 2 по правилу modus ponens.

6) - выводится из пунктов 4 и 1 по правилу modus ponens.

7) - схема аксиом (А3).

8) - выводится из пунктов 6 и 7 по правилу modus ponens.

9) - выводится из пунктов 5 и 8 по правилу modus ponens.

Итак, доказано, что ├ . Применяя дважды теорему дедукции, получим: ├ и ├ . Что и требовалось доказать.

Замечание (метаязык): Доказанная теорема в содержательной логике означает, что из и , т. е. из любого противоречия, логически следует любое высказывание . Таким образом, следствием противоречия является вся «мудрость мира и все глупости», т. е. высказывания являются истинными.

Теорема 6: ├ .

Доказательство:

1) - гипотеза.

2) - гипотеза.

3) - схема аксиом (А3).

4) - схема аксиом (А1).

5) - выводится из пунктов 1 и 3 по правилу modus ponens.

6) - следствие 1 из теоремы дедукции, применённое к пунктам 4 и 5.

7) - выводится из пунктов 2 и 6 по правилу modus ponens.

Таким образом, ├ . Применяя дважды теорему дедукции, получаем: ├ . И, наконец, ├ . Что и требовалось доказать.

Теорема 7: ├ .

Доказательство:

1) - гипотеза.

2) - теорема 3.

3) - следствие 1 из теоремы дедукции, применённое к пунктам 2 и 1.

4) - теорема 4.

5) - следствие 1 из теоремы дедукции, применённое к пунктам 3 и 4.

6) - теорема 6.

7) - выводимо из пунктов 5 и 6 по правилу modus ponens.

Таким образом, доказано, что ├ , откуда по теореме дедукции имеем: ├ . Теорема доказана.

Замечание: Из теорем 6 и 7 следует закон контрапозиции в теории .

Теорема 8: ├ .

Доказательство: Правило modus ponens можно записать следующим образом: ├ . Применяя дважды теорему дедукции, получим:

├ . (а)

По теореме 7 имеем:

├ . (б)

Теперь по следствию 1 из теоремы дедукции, применённому к пунктам (а) и (б), получаем: ├ . Что и требовалось доказать.

Теорема 9: ├ .

Доказательство:

1) - гипотеза.

2) - гипотеза.

3) - теорема 7.

4) - выводится из пунктов 1 и 3 по правилу .

5) - теорема 6.

6) - выводится из пунктов 2 и 5 по правилу .

7) - схема аксиом (А3).

8) - выводится из пунктов 6 и 7 по правилу .

9) - выводится из пунктов 4 и 8 по правилу .

Итак, ├ . Применяя два раза теорему дедукции, получаем утверждение теоремы: ├ .

Замечание: Доказанной теореме в содержательной логике соответствует тот факт, что если выводимо из и выводимо из , то - истинно ().

Наша дальнейшая цель – показать, что произвольная формула теории тогда и только тогда является теоремой этой теории, когда она есть тавтология.

Теорема 10 (метатеорема): Всякая теорема теории есть тавтология.

Доказательство прямого утверждения очень простое. Для примера можно убедиться в том, что каждая аксиома теории есть тавтология. Кроме того, если и – тавтологии, то и является тавтологией. Таким образом, правило modus ponens, примененное к тавтологиям, приводит к тавтологиям. Следовательно, всякая теорема теории есть тавтология.

Следующая лемма необходима для доказательства обратного утверждения.

Лемма 1: Пусть есть формула, - пропозиционные переменные, входящие в формулу . Пусть задано некоторое распределение истинностных значений для переменных . Пусть есть , если ; пусть есть , если . Пусть, наконец, - есть , если при этом распределении принимает значение и, и , если принимает значение л. Тогда ├ .

Если, например, , то можно рассмотреть таблицу истинности данной формулы:

И	И	Л
Л	И	Л
И	Л	Л
Л	Л	И

Лемма утверждает, что факт соответствующей выводимости для каждой строки таблицы истинности. В частности, третьей строке соответствует утверждение: ├ , а четвёртой строке - ├ .

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

Если , то есть пропозиционная буква , и утверждение леммы сводится к следующему: ├ и ├ .

Допустим теперь, что утверждение леммы справедливо для любого числа .

Случай 1: имеет вид отрицания . Число вхождений логических операций в формулу , очевидно, меньше .

Случай 1а: Пусть при заданном распределении истинностных значений принимает значение «истина». Тогда принимает значение «ложь». Таким образом, есть , и есть . По индуктивному допущению, применённому к , имеем: ├ . Следовательно, по теореме 4: . Тогда по правилу вывода : ├ , но .

Случай 1б: Пусть принимает значение , тогда , а совпадает с . По индуктивному предположению имеем: ├ , что и требовалось доказать, ибо есть .

Случай 2: имеет вид , тогда число вхождений логических операций в и меньше, чем в . Поэтому, в силу индуктивного допущения, ├ и ├ .

Случай 2а: принимает значение «ложь». Тогда принимает значение «истина», есть , а есть . Таким образом, ├ и по теореме 5 имеем: ├ . Но и есть .

Случай 2б: принимает значение . Следовательно, принимает значение , есть , а есть . Имеем: ├ , тогда по схеме аксиом (А1) получаем: ├ , где совпадает с .

Случай 2с: принимает значение , принимает значение . Тогда есть , т. к. . есть и есть . Имеем: ├ и ├ . Отсюда по теореме 8 () получаем: ├ , где совпадает с формулой . Лемма доказана полностью.

Теорема 11: (теорема о полноте, Кальмар).

Если формула теории является тавтологией, то она является теоремой теории .

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

Следствие: Теория формально непротиворечива.

Доказательство: Все теоремы в теории суть тавтологии. Отрицание тавтологии не есть тавтология. Следовательно, в нет теоремы и ее отрицания.

Основные понятия о формализации логики предикатов.

Отметим, что формализация логики высказываний – это лишняя работа, т. к. на все основные вопросы логики высказываний можно получить ответ, например, построив таблицу истинности.

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

Далее будут рассмотрены основные определения, необходимые для формализации математических теорий.

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

.

Определение 1: - арной алгебраической операцией, определённой на множестве , называется функция

.

Операцию называют всюду определённой, если для всякого набора из элементов функция сопоставляет единственный элемент из множества . Если функция определена не для всех наборов, то операцию называют частичной.

Замечание: При операция называется унарной, при - бинарной и т. д.

Например, унарная частичная операция, определённая на множестве квадратных матриц: . Эта операция определена для невырожденных матриц. Операции сложения и умножения квадратных матриц данного порядка – это бинарные, всюду определённые операции.

Если - переменная, определённая на множестве действительных чисел, то выражение - это другая переменная, определённая на том же множестве, но для её записи необходимы постоянные величины (числа 2 и 3) и алгебраические операции (умножение и сложение).

Аналогично выражение представляет двуместный предикат, определённый на множестве действительных чисел. Для его записи необходимы константы (числа 3, 4 и 5) и алгебраические операции (умножение и вычитание).

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

Функциональные буквы, применённые к константам, порождают термы. Точнее:

а) всякая предметная переменная или константа – есть терм.

б) если - функциональная буква и - термы, то - есть терм.

в) выражение является термом тогда и только тогда, когда это вытекает из пунктов а) и б).

Определим теперь формулы логики предикатов.

Предикатные буквы, применённые к термам, порождают элементарные формулы. А точнее: если - предикатная буква, а - термы, то - элементарная формула.

Определение 2: Формулы исчисления предикатов определяются следующим образом:

1) всякая элементарная формула – есть формула.

2) если и - формулы и - предметная переменная, то каждое из следующих выражений есть формула: , и .

3) выражение является формулой тогда и только тогда, когда это следует из правил 1) и 2).

В выражении буква называется областью действия квантора общности. При этом может и не содержать переменной . В этом случае содержательный смысл и считается одинаковым.

Выражения , , определяются так же, как в теории . У нас нет необходимости включать в число основных символов знак квантора существования , так как можно определить , как сокращённую запись для выражения . Это полностью отражает содержательный смысл кванторов.

Оставляя в силе соглашение о снятии скобок, договоримся дополнительно считать, что кванторы и располагаются по силе между операциями и . Например, вместо выражения можно написать: .

Определение 3: Вхождение переменной в данную формулу называется связным, если находится под знаком квантора общности, или в области действия входящего в эту формулу квантора. В противном случае вхождение переменной в формулу называется свободным.