Основные положения математической логики

Формальные теории

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

Формальная теория :

1) множество символов ,образующих алфавит;

2) множество слов в алфавите, которые называются формулами;

3) подмножество ; состоит из аксиом;

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

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

.

Формулы в числителе называются посылками, а формула в знаменателе – заключением, или секвенцией. Иногда обозначение правила вывода справа от черты дроби опускают, если ясно, о чем идет речь.

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

Если формула выводима из формул в теории , то это обозначается так: . Формулы называются гипотезами вывода. Если формула G непосредственно выводима из аксиом (т.е. без гипотез), то она называется теоремой. Обозначение: .

Если некоторый набор гипотез позволяет вывести формулу, то добавление гипотез не должно приводить к невыводимости:

.

Интерпретацией формальной теории в области интерпретации называется функция I: , которая с каждой формулой формальной теории сопоставляет некоторое содержательное высказывание относительно объектов множества . Это высказывание может быть истинным, ложным или не иметь значения истинности. Если соответствующее высказывание является истинным, то формула выполняется в данной интерпретации. Интерпретация называется моделью множества формул, если все формулы этого множества выполняются в данной интерпретации. Интерпретация называется моделью формальной теории, если все теоремы этой теории выполняются в данной интерпретации (т.е. все выводимые формулы модели являются истинными в данной интерпретации).

Формула называется общезначимой (или тавтологией), если она истинна в любой интерпретации.

Исчисление высказываний

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

1. Множество символов , образующих алфавит:

– и – связки;

– (, ) – служебные символы;

– – пропозициональные переменные.

2. Формулы:

– переменные суть формулы;

– если – формулы, то ( ) и ( ) – формулы.

3. Аксиомы:

;

;

.

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

4. Правило: – modus ponens.

Другие связки вводятся определениями (а не аксиомами):

.

Если в формулу подставить вместо переменных подставить соответственно формулы , то получится формула, которая называется частным случаем исходной. Набор подстановок называется унификатором. Формула называется совместным частным случаем формул и , если является частным случаем и частным случаем при одном и том же общем унификаторе. Наименьший возможный унификатор называется наиболее общим унификатором.

При конструктивном определении исчисления высказываний помимо приведенного правила modus ponens вводится еще одно, называемое правилом подстановки: если формула является частным случаем формулы , то формула непосредственно выводима из .

Теорема 1. .

Доказательство. В аксиому : вместо подставим .

Тем самым выведем формулу .

По второй аксиоме : . Подставим вместо , вместо :

.

Теперь видим, что по правилу modus ponens выводится формула .

Подключаем : , заменив на : .

По правилу modus ponens , что и требовалось доказать.

Теорема 2. (правило введения импликации).

Доказательство. – гипотеза. : – гипотеза .

По правилу modus ponens , что и требовалось доказать.

Теорема 3. Если , , то , и наоборот (дедукция).

Доказательство. Дано: существуют , такие, что , а – либо аксиомы, либо , либо , либо , .

Доказательство проводим по индукции. Необходимо доказать, что если существует вывод , то , ,…

1. Докажем, что . Дано: , . Доказать: . Возможны три случая:

а) – аксиома. Применяем первую аксиому: : . По правилу МР , МР , или (в левой части аксиомы не пишут);

б) . Тогда : . Предположим, что . Тогда по МР МР . Значит, , . Но так как , то в левой части писать незачем, и ;

в) . Тогда , . Выше было показано, что . Принимая правую (выведенную) часть , в виде гипотезы и используя : , по правилу МР получаем . Это можно записать в виде . Но , значит, .

2. Пусть выведены. Выведем : . Возможны те же три случая а – в, которые доказываются аналогично, но существует и четвертый случай: . Используем вторую аксиому :

.

Получаем . – это гипотеза индукции, которая считается выведенной. По МР . Опять-таки, – гипотеза вывода, и по МР . Результат: .

При приходим к утверждению теоремы.

Обратная теорема: .

Доказательство. Примем выведенное утверждение в качестве гипотезы. Если – гипотеза, то по МР . Отсюда , что и требовалось доказать.

Следствие 1. Если , то , и обратно.

Следствие 2. , (правило транзитивности).

Доказательство. , – гипотезы. По правилу МР , – гипотезы. Значит, . Это записываем в виде , , . По теореме дедукции , , что и требовалось доказать.

Следствие 3. , (правило сечения).

Другие теоремы:

; ; ;

; ;

; , ….

Способы доказательства теорем в исчислении высказываний следующие:

1. Использовать методику, приведенную выше. Ее суть – применение аксиом, правил вывода и поиск унификаторов. Каждая выведенная теорема подключается к списку левой части любого вывода. Основное средство – теорема дедукции:

, .

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

, где .

Далее записать формулу АВ (алгебры высказываний):

.

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

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

, .

Теперь запишем соответствующую формулу АВ (в булевой форме) и преобразуем, используя эквивалентности АВ:

.

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

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

.

Эту теорему нужно доказать. Используем алгебру высказываний (АВ), считая символ «+» дизъюнкцией, а символ «•» конъюнкцией: , что соответствует аналогичной формуле АВ, которую запишем в булевой форме:

.

Придадим поочередно значения 0 и 1:

;

.

Итак, при любых значениях , , данная формула алгебры высказываний имеет значение «истина», что и означает выводимость теоремы .

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

.

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

Знаменатель правила имеет название «резольвента».

Исчисление предикатов

Пусть – произвольное множество. Предположим, что на нем задана тотальная функция (однозначное отображение) на этом множестве : (однозначное отображение), т.е. . Эта функция является -парной (или -местной).

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

Примеры:

1. Пусть – множество целых чисел. Рассмотрим сигнатуру, состоящую из двух бинарных операций: «+», «*». Возникает алгебра чисел – .

2. Задано произвольное множество и операция «*» (или «+»). Получаемая алгебра называется группой.

Частные случаи:

– = , «*» – группа целых чисел.

– (, «+») – группа целых чисел; (2 , «+») – подгруппа группы целых чисел, или группа четных чисел.

Если функции сигнатуры являются произвольными отношениями, то пара (, )называется моделью.

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

Пример. (2; 4; 10; «+»); 2 + 2 = 4; 2 + 4 = 6 (2; 4; 6; 10; «+») – все то, что можно получить, и является замыканием (все четные числа).

Элементы сигнатуры называются функторами; – терм. Отображение некоторого множества термов во множество {И, Л} называется атомом. Он состоит из двух объектов: , где – предикат, – список термов.

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

Указанием на пункт А или Б являются кванторы: «все» – All: ; «существует» – Exists: .

С помощью кванторов исчисление высказываний обогащается новым типом формул: ; – «И», «Л» в зависимости от .

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

П1 ; П2 ;

MP: : ; : .

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

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

Основные идеи такого приведения:

1. .

Пример. Доказать, что число 36 делится на 6. Вместо этого докажем две другие теоремы: 36/2 и 36/3. После доказательства этих теорем следует, что (36/2) и (36/3) (36/6). Значит, исходную формулу желательно представить в виде конъюнкций.

2. Избавиться от отрицаний перед кванторами:

, .

3. .

Пример. Пусть дана плоскость и вектор нормали.

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

.

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

Шаг 1. Избавление от импликаций:

.

Шаг 2. «Протаскивание» отрицаний:

.

Шаг 3. Вспомогательная операция – разделение связанных переменных. Основная идея заключается в том, что каждая связанная переменная может встречаться только два раза: первый раз – в обозначении квантора, второй – в обозначении терма:

… … (… …) = … … (… …).

Например, – не имеет смысла; – правильно.

Шаг 4. Приведение к предваренной форме. Основная ид