Главная   Онлайн инструменты по математической логике   Мат. логика теория   Как считает компьютер?   Схемы для ЭВМ    

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

Определение булевой функции
Элементарные булевы функции
Задание булевых функций посредством элементарных
Существенные и несущественные переменные
Эквивалентные функции
Основные эквивалентности
Функциональная полнота
Нормальные формы
Совершенные нормальные формы
Минимизация ДНФ методом Квайна
Карты Карно
Полином Жегалкина
Высказывания
Предикаты
Кванторы
Определение формальной теории
Исчисление высказываний
Теорема о дедукции. Полнота ИВ
Автоматическое доказательство теорем
Метод резолюций в ИВ
Определение алгоритма
Машина Тьюринга
Рекурсивные функции
Алгоритмически неразрешимые задачи
Алгоритмы и их сложности



     Используя понятие формального исчисления, определим исчисление высказываний (ИВ).
     Алфавит ИВ состоит из
         1. букв А, В, Q, R, Р и других, возможно с индексами (которые называются пропозициональными переменными},
         2. логических символов (связок) ¬, &, v, →,
         3. вспомогательных символов (,).
     Множество формул ИВ определяется индуктивно:
         1. все пропозициональные переменные являются формулами ИВ;
         2. если A, B — формулы ИВ, то ¬A, AΛB, AvB, A→B — формулы ИВ;
         3. выражение является формулой ИВ тогда и только тогда, когда это может быть установлено с помощью пунктов "1" и "2".
     Таким образом, любая формула ИВ строится из пропозициональных переменных с помощью связок ¬, Λ, v, →, ~.
     В дальнейшем при записи формул будем опускать некоторые скобки, используя те же соглашения, что и в предыдущей главе.
     Аксиомами ИВ являются следующие формулы (для любых формул A,B,C)
         1. A→(B→A);
         2. (A→B)→((A→(B→C))→(A→C));
         3. (AΛB)→A;
         4. (AΛB)→B;
         5. (A→B)→((A→C)→(A→(BΛC)));
         6. A→(AvB);
         7. A→(BvA);
         8. (A→C)→((B→C)→((AvB)→C));
         9. (A→B)→((A→¬B)→¬A);
         10. ¬¬A→A.
     Указанные формулы называются схемами аксиом ИВ. При подстановке конкретных формул в какую-либо схему получается частный случай схемы аксиом.
     Правилом вывода в ИВ является правило заключения {modus ponens): если A и A→B — выводимые формулы, то B — также выводимая формула.
     Например, если высказывания АΛВ и АΛВ→(А→С) выводимы, то высказывание А→С также выводимо согласно правилу заключения.
     Говорят, что формула G выводима из формул F1,F2,…,Fn (обозначается F1,F2,…,Fn ├G), если существует последовательность формул F1,F2,…,Fk,G, в которой любая формула является либо аксиомой, либо принадлежит списку формул F1,F2,…,Fn (называемых гипотезами), либо получается из предыдущих формул по правилу вывода. Выводимость формулы G из ∅ (обозначается ├G) равносильно тому, что G — теорема ИВ.
     Пример. Покажем, что формула A→A выводима в ИВ. Для этого построим вывод данной формулы:
         1) в аксиоме 2 заменим B на A→A, C — на A. Получаем аксиому (A→(A→A))→((A→((A→A)→A))→(A→A));
         2) в аксиоме 1 заменим B на A. Получаем A→(A→A);
         3) из 1 и 2 по modus ponens заключаем (A→((A→A)→A))→(A→A);
         4) в аксиоме 1 заменяем B на A→A. Получаем A→((A→A)→A);
         5) из пп. 3 и 4 по правилу вывода справедливо ├ A→A.
     Теорема.
         1. Если F1,F2,…,Fn,A,B — формулы ИВ, Г={F1,F2,…,Fn}, Г├A, то Г,B├A. (можно увеличивать число гипотез).
         2. Тогда и только тогда F1,F2,…,Fn├A, когда F1ΛF2Λ...ΛFn├A (сведение множества гипотез к одной гипотезе).

@ 2010 - 2017 tablica-istinnosti.ru Рейтинг@Mail.ru