logo search
DM_shpory

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

1. Алфавит исчисления высказываний состоит из переменных высказываний (пропозициональных букв): A, B, C …, знаков логических связок Ú, &, Ø, ® и скобок (, ).

2. Формулы:

а) переменное высказывание (пропозициональная буква) есть формула;

б) если À и  — формулы, то (À ÚÂ), (À &Â), (À ®Â) и (ØÀ) также формулы;

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

3. Аксиомы исчисления высказываний (система аксиом 1)

I1. A ® (B ® A);

I2. (A ® B) ® ((A®(B ® C)) ® (A®C));

I3. (A & B) ® A;

I4. (A & B) ® B;

I5. A ® (B ® (A & B));

I6. A ® (A Ú B);

I7. B ® (A Ú B);

I8. (A ® C) ® ((B ® C) ®((AÚB) ® C));

I9. (A ® B) ® ((A® Ø B) ® Ø A);

I10. ØØ A® A

4. Аксиомы исчисления высказываний (система аксиом II)

II1. A ® (B ® A);

II2. (A ® (B®C)) ® ((A®B) ® (A®C));

II3. (ØA ® ØB) ® ((ØA ® B) ® A)

AÚB заменяет Ø A® B,

A & B заменяет Ø(A® Ø B)

5. Система аксиом III (дизъюнктивный базис Буля)

III1. A Ú A ® A

III2. A Ú B ® B Ú A;

III3. A ® A Ú B;

III4. (B ® C) ® (A Ú B ® A Ú C),

где запись a ® b эквивалентна записи aØ  Ú b.

Правила вывода исчисления высказываний

правило подстановки: если a — выводимая формула, содержащая букву A (обозначив это как a(A)), то выводима формула a(b), получающаяся из a заменой всех вхождений A на произвольную формулу

правило заключения (modus ponens): (если a ® b и a — выводимые формулы, то b также выводимая формула)

Пример:

Покажем, что формула A ® A выводима из системы аксиом II:

|— A ® A

1. Подставим в II2 (A ® A) вместо B и A вместо C:

II2. (A ® (B®C)) ® ((A®B) ® (A®C));

(A ® ((A ® A)® A)) ® ((A®(A ® A)) ® (A® A));

2. Подставим в II1 (A ® A) вместо B:

II1. A ® (B ® A);

A ® ((A ® A)® A);

3. Из шагов 2, 1 по правилу заключения:

((A®(A ® A)) ® (A® A));

4. Подставим в II1 A вместо B:

II1. A ® (B ® A);

A ® (A ® A);

5. Из шагов 4, 3 по правилу заключения:

A® A

Логический вывод

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

Решение этой задачи называют выводом теоремы из аксиом.

Прямой вывод

В прямом выводе используется знание семантики тех операторов, через которые строятся аксиомы. Так, если аксиома утверждает, что A&B, то из смысла этого утверждения следует, что истинными будут высказывания A и B, которые войдут в цепочку вывода. Если известно, что истинным являются высказывания {A Ú B, `A}, то истинным будет высказывание B именно исходя из смысла этих высказываний. В прямом выводе строится цепочка высказываний F1, F2, ..., Fm которая и является выводом.

Пример:

B`®A, A&D, BÚC |— D&C.

Пронумеруем аксиомы: B`®A (1), A&D (2), BÚC (3).

Вывод. Из (2) Þ A (4), из (2) Þ D (5), из (4) и (1) `ÞB (6), из (6) и (3) ÞС (7), из (5) и (7) следует D&C. Здесь используется свойство связок И, ИЛИ и СЛЕДУЕТ. Действительно, A&B истинна, если истинны A и B одновременно (вывод 4 и 5) . Если A= T, то `A = F, значит B не может быть T, т.е. B=F (вывод 6). Если B=F и BÚC истинно, то C должно быть равно T (вывод 7). Наконец, из (7) и (5) следует искомый вывод.

Доказательство «от противного»

Из определения вывода вытекает, что если A1, …, An |— B, то справедливо утверждение, что A1& …& An |— B, или, что |— (A1& …& An)® B.

Принцип дедукции. Формула B является логическим следствием конечного множества A тогда и только тогда, когда A È {ØB } невыполнимо.

{A1, …, An}|— B Û { A1, …, An, ØB}|— 0.

На основе этого утверждение строится способ доказательства, который называется доказательством «от противного» или «reductio ad absurdum». В этом случае в множество аксиом добавляется высказывание, равное отрицанию того, что необходимо вывести. После этого нужно доказать, что из расширенного множества аксиом выводимо противоречие.

Пример:

Требуется доказать или опровергнуть вывод

{`AÚB, B ®C, AÚD }|— CÚD.

Обозначим`AÚB (1), B®C (2), AÚD (3). Введём ещё одно высказывание Ø(CÚD)= `С&`D (4) (по правилу де Моргана). Тогда из (4)`ÞС (5), из (4)`ÞD (6), из (6) и (3) ÞA (7), из (7) и (1) ÞB (8), из (8) и (2) ÞС (9), из (8) и (9) ÞС& `С, то есть противоречие. Значит, верно, что CÚD.

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

Ø(B ®C) = B & `С, следует тоже два утверждения: B и `С. Используя их необходимо построить противоречие.

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

Если формула имеет вид КНФ, то её можно рассматривать как множество дизъюнктов. Множество дизъюнктов невыполнимо тогда и только тогда, когда пустой дизъюнкт является логическим следствием из него. Невыполнимость множества S можно проверить, порождая логическое следствие до тех пор, пока не получим пустой дизъюнкт.

Выполнимые и общезначимые формулы

103