Логика высказываний

Для понятия ``высказывание'' иногда используют термин ``пропозиция'', что является калькой с английского. Мы этот термин не используем, но говорим ``пропозициональный'' в смысле относящийся к логике высказываний. Центральными понятиями данной части являются пропозициональные формулы и пропозициональный вывод.

Объектный язык и метаязык

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

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

Пропозициональные формулы

Пропозициональная сигнатура – это множество символов, называемых атомами. Символы ¬ (отрицание), & (конъюнкция), Ъ (дизъюнкция) и Й (импликация) называются пропозициональными связками; ¬ – унарная связка, а другие – бинарные.

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

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

Определение 7. Множество X строк замкнуто относительно правил построения (для логики высказываний), если

• каждый атом принадлежит X,
• для любой строки F, если F принадлежит X, то ¬F тоже принадлежит,
• для любых строк F, G и любой бинарной связки Д, если F и G принадлежат X, то также принадлежит (F Д G).

2.1 Укажите два примера множества строк: одно замкнутое, другое не замкнутое относительно правил построения.

Определение 8 (Формула). Строка F называется пропозициональной формулой, если F принадлежит всем множествам, которые замкнуты относительно правил построения.

2.2 Множество формул замкнуто относительно правил построения.

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

В двух следующих задачах мы предполагаем, что рассматриваемая сигнатура – это {p, q}.

2.3 Является ли формулой ¬(p & q)?

2.4 Является ли формулой (p)?

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

Доказательство свойств формул по индукции

Семантика

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

Определение 10 (Интерпретация). Символы л,и (``ложь'', ``истина'') называются истиностными значениями. Интерпретация пропозициональной сигнатуры s есть функция из s в {л,и}.

Если s конечна, тогда интерпретация может быть определена таблицей её значений, например:

p q л и

(3)

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

Прежде всего нам надо связать функцию с каждой пропозициональной связкой – функцию из {л,и} в {л,и} с унарной связкой ¬ и функцию из {л,и}ґ {л,и} в {л,и} с каждой бинарной связкой. Функции определяются следующими таблицами:

x ¬(x) л и и л

x y &(x, y) Ъ(x, y) Й(x, y) л л л л и л и л и и и л л и л и и и и и

Для любой формулы F и любой интерпретации I истиностное значение F^I , назначенное формуле F интерпретацией I, определяется как значение суперпозиции соответствующих булевых функций, а именно, следующим образом:

• F^I = I(F) если F – атом,
• (¬F )^I = ¬(F^I),
• (F Д G)^I = Д(F^I,G^I) для каждой бинарной связки Д.

Заметим, что это определение рекурсивно: (¬F)^I определяется через F^I и (F Д G)^I – через F^I и G^I.

Если F^I = и, мы говорим, что формула F истинна при интерпретации I (символически I |= F ).

2.10 Найдите формулу F такую, что (3) – единственная интерпретация, при которой F истинна.

Если рассматриваемая сигнатура конечна, тогда множество интерпретаций тоже конечно, и значения F^I для всех интерпретаций можно представить в виде конечной таблицы. Эта таблица называется таблицей истинности формулы F. Например, предыдущая задача может быть сформулирована следующим образом: найти формулу, таблицей истинности которой является

p	q
л	л	л
л	и	и
и	л	л
и	и	л

2.11 Для любых формул F₁,...,F_n (n і 1) и любой интерпретации I

2.12 Сформулируйте и докажите подобный факт для дизъюнкции F₁ Ъ ··· Ъ F_n.

В двух следующих задачах мы предполагаем, что рассматриваемая сигнатура конечна: s = { p₁, ..., p_n}.

2.13 Для любой интерпретации I существует формула F такая, что I – единственная интерпретация, при которой F истинна.

2.14 Для любой функции a из интерпретаций в истинстные значения существует формула F такая, что для всех интерпретаций I: F^I = a(I).

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

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

Определение 11 (Эквивалентность). Формула F эквивалентна формуле G, если F^I = G^I для любой интерпретации I.

В задачах 2.16, 2.18 и 2.20 мы вводим несколько ``нормальных форм'' таких, что любая пропозициональная формула может быть эквивалентно трансформирована в любую из этих форм.

2.15 Покажите, что для атомов p и q

• каждая из формул p & q, p Й q эквивалентна формуле, не содержащей связок, кроме Ъ и ¬,
• каждая из формул p Ъ q, p Й q эквивалентна формуле, не содержащей связок, кроме & и ¬,
• каждая из формул p & q, p Ъ q эквивалентна формуле, не содержащей связок, кроме Й и ¬.

2.16 Любая формула эквивалентна

• формуле, не содержащей связок, кроме Ъ и ¬,
• формуле, не содержащей связок, кроме & и ¬,
• формуле, не содержащей связок, кроме Й и ¬.

В сочетании с результатом задачи 2.14 этот факт показывает, что множества { Ъ, ¬ }, { &, ¬ } и { Й, ¬ } – ``полные'' множества связок – они достаточны для выражения любой таблицы истинности. С другой стороны, множество { Ъ, &, Й } не ``полное'':

2.17 Предполагая, что p – атом, покажите что любая формула, эквивалентная ¬p, содержит по крайней мере одно отрицание. см. Указания

Литерал – это атом или отрицание атома. Элементарная конъюнкция – это формула вида L₁& ··· & L_n (n і 1), где L₁,...,L_n – литералы. Будем говорить, что формула находится в дизъюнктивной нормальной форме, если она имеет вид C₁ Ъ ··· Ъ C_m (m і 1), где C₁, ..., C_m – элементарные конъюнкции.

2.18 Любая формула эквивалентна некоторой формуле в дизъюнктивной нормальной форме.

Элементарная дизъюнкция – это формула вида L₁ Ъ ··· Ъ L_n (n і 1), где L₁,...,L_n – литералы. Будем говорить. что формула находится в конъюнктивной нормальной форме, если она имеет вид D₁ & ··· & D_m (m і 1), где D₁, ..., D_m – элементарные дизъюнкции.

2.19 Пусть F – формула в дизъюнктивной нормальной форме. Покажите, что ¬F эквивалентно некоторой формуле в конъюнктивной нормальной форме.

2.20 Любая формула эквивалентна некоторой формуле в конъюнктивной нормальной форме.

Выполнимость

Определение 12 (Выполнимость). Если существует интерпретация, при которой формула F истинна, мы говорим, что F выполнима.

Эта терминология применима также к множествам формул: множество G формул выполнимо, если существует интерпретация, при которой истинны все формулы G.

2.21 Пусть G – множество литералов. Покажем, что G выполнимо тогда и только тогда, когда не существует атома A, для которого и A и ¬A принадлежат G.

Для любого атома A литералы A, ¬A называются дополнительными друг к другу. Так, утверждение последней задачи может быть выражено следующим образом: множество литералов выполнимо тогда и только тогда, когда оно не содержит дополнительных пар.

Логическое следование

Определение 13 (Логическое следование). Формула F (логически) следует из множества формул G (или множество формул G влечёт формулу F, символически, G |= F ), если для каждой интерпретации, при которой все формулы G истинны, формула F также истинна.^*

Про формулы, которые логически следуют из G будем говорить ``логическое следствие G''.

2.22 Предполагая, что p и q – атомы, определите

• следует ли q из (множества состоящего из) p и p Й q,
• следует ли ¬q из ¬p и p Й q.

2.23 G влечёт F тогда и только тогда, когда G И { ¬F } не выполнимо.

Определение 14 (Тавтология). Формула F называется тавтологией, или тождественно истинной формулой, если F истинно при любой интерпретации.^*

Понятие тавтологии ``двойственно'' понятию выполнимой формулы: F – тавтология тогда и только тогда, когда ¬F не выполнима. Определение эквивалентных формул, данное выше, может быть переформулировано следующим образом: F эквивалентна G, если F є G – тавтология.

2.24 Определить, какие из следующих формул являются тавтологиями: (p Й q) Ъ (q Й p), ((p Й q) Й p) Й p, ((p є q) є r) є (p є (q є r)).

2.25 Для любых формул F, G₁,...,G_n (n і 1) : F следует из { G₁,..., G_n } тогда и только тогда, когда (G₁ & ··· & G_n) Й F – тавтология.

Пропозициональный вывод

Существует другое определение следования, которое выглядит совершенно отличающимся от данного выше, но в действительности эквивалентное ему. В соответствие с этим определением, G влечёт F, если F может быть выведено из G с использованием определенного набора ``правил вывода''. Первое определение, основанное на интерпретации, – ``семантическое'', второе, основанное на понятии вывода – ``синтаксическое'' или ``дедуктивное''.

О корректности, полноте и разрешимости

Выводы в логике высказываний – наш основной объект изучения до конца данной части.

Вывод строятся из конструкций, которые называются ``секвенциями''.

Определение 15 (Секвенция). Секвенция – это выражение вида G |– F (``F при посылках G'') или G |– ^ (``посылки G противоречивы''), где F – формула и G – конечное множество формул. ^*

Мы определим, какие секвенции рассматриваются ``начальными'', и опишем несколько ``правил вывода'' для порождения новых секвенций из секвенций, порождённых ранее. Начальные секвенции называются аксиомами.

Определение 16 (Аксиомы). Аксиомы в исчислении высказываний имеют вид

Мы определим 12 правил вывода, и удобно вводить их постепенно.

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

Определение 17 (Дерево доказательства). Дерево доказательства определим рекурсивно:

1. Деревом доказательства является пустое дерево доказательства, состоящее только из корня – аксиомы.
2. Пусть T₁, ..., T_k – деревья доказательства с корнями R₁, ..., R_k. Тогда

   T1 ... Tk

   S

   (где S – некоторая секвенция) – дерево доказательства, если S может быть получена из R₁, ..., R_k с помощью одного из правил вывода. Корнем такого дерева является S.

Определение 18 (Доказуемая секвенция). Если существует дерево доказательства с корнем R, то R называют доказуемой секвенцией. Если этот корень имеет вид G |– F, то говорят о выводе формулы F из G.

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

Правила для конъюнкции и импликации

G |– F G |– G (В&) G |– F & G	G |– F & G (У&) G |– F G |– F & G G |– G
G И { F } |– G (ВЙ) G |– F Й G	G |– F G |– FЙ G (УЙ) G |– G

В каждом из этих пяти правил вывода, одно или два выражения над горизонтальной чертой представляют ``посылки'', к которым правило может быть применено, и выражение под чертой представляет ``заключение'' которое выводится по этому правилу. Правила В& и ВЙ – ``правила введения'' конъюнкции и импликации; У& и УЙ – ``правила удаления''. Подставляя конкретные формулы вместо метапеременных F и G и конкретные конечные множества формул вместо метапеременной G некоторое правило вывода, мы получаем пример этого правила. Например,

{q, r} |– p {p Ъ q, r} |– ¬q

{q, r, p Ъ q} |– p & ¬q

Пример простого вывода. . Выведем формулу q из посылки p & q. Этот вывод получается за один шаг с помощью второго правила удаления конъюнкции.



2.26 Найдите вывод q & p из p & q.

см. Решение

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

2.27 (p & p) Й p.

2.28 (p & p) є p.

Правило введения посылки

Мы построили несколько примеров простых выводов. Однако, используя только правила для конъюнкции и импликации, мы не сможем построить вывод формулы p & q из множества посылок {p, q}. Действительно, формулу {p, q} |– p & q мы можем получить с помощью правила (В&) из формулу {p, q} |– p и формулу {p, q} |– q. Однако ``очевидные'' формулы {p, q} |– p и {p, q} |– q мы не сможем вывести. У нас нет правила, позволяющего выводить формулу из некоторого множества посылок, если она выводится из более узкого множества. Это правило вывода назовём правилом введения посылки.

Пример вывода. Мы приводим вывод p Й ((p Й q) Й (p & q)) из пустого множества посылок:



2.29 Найдите вывод p Й r из p Й q и q Й r.

2.30 Найдите вывод r из p & q и p Й (q Й r).

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

2.31 p Й (q Й p).

2.32 p Й ((p & q) є q).

2.33 ((p & q) Й r) є (p Й (q Й r)).

Корректность правил вывода

Определение 19 (Истинность секвенций). Секвенция G |– F тождественно истинна, если G влечёт F.^*

Определение 20 (Корректность правил вывода). Правило вывода корректно, если для каждого примера этого правила посылки которого являются тождественно истинными, его заключение также тождественно истинно.

2.34 Правило введения посылки корректно.

2.35 Оба правила удаления конъюнкции корректны.

2.36 Правило введения конъюнкции корректно.

2.37 Правило удаления импликации корректно.

2.38 Правило введения импликации корректно.

Правила для отрицания и правила противоречия

Следующие четыре правила вывода – правила введения и удаления отрицания ``правило сведения к противоречию'' и ``правило противоречия''.

G И { F } |– ^ (В¬) G |– ¬F	G И { ¬F } |– ^ (У¬) G |– F
G |– F G |– ¬F (В^) G |– ^	G |– ^ (У^) G |– F

Выведите секвенции:

2.39 {¬¬p} |– p.

см. Решение

2.40 {p} |– ¬¬p.

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

2.41 ¬(p & ¬p).

2.42 (p & ¬p) Й q.

Определение 21 (Истинность секвенций). Секвенция G |– ^ тождественно истинна, если G не выполнимо.

2.43 Правило удаления отрицания корректно.

2.44 Правило введения отрицания корректно.

2.45 Правило противоречия корректно.

Правила для дизъюнкции

Оставшиеся три правила вывода – правила введения и удаления дизъюнкции:

G |– F (В Ъ) G |– F Ъ G

G |– G G |– F Ъ G

	G |– F Ъ G G И F |– C G И G |– C
(У Ъ)
	G |– C

Здесь F и G – формулы, и C – либо формула, либо ^.

Теперь описание системы вывода для логики высказываний завершено.^*

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

О том, как строить дерево доказательства.

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

2.46 (p Ъ q) Й (q Ъ p).

2.47 (p Ъ p) є p.

2.48 ¬p Й ((p Ъ q) є q).

2.49 (p & (q Ъ r)) є ((p & q) Ъ (p & r)).

2.50 ¬¬p є p.

2.51 ¬(p Ъ q) є (¬p & ¬q).

2.52 Оба правила введения дизъюнкции корректны.

2.53 Правило удаления дизъюнкции корректно.

Корректность и полнота логики высказываний

Теорема корректности. Если существует вывод F из G, тогда G логически влечёт F.

Теорема полноты. Для любой формулы F и любого множества формул G, если G влечёт F, тогда существует вывод F из подмножества G.

Полнота логики высказываний (для другого множества правил вывода) была установлена Емилем Постом в 1921 году.