- •Введение
- •Программа курса математическая логика и терия алгоритмов
- •Логическое следствие в алгебре высказываний
- •2.1.3. Эквивалентные формулы алгебры высказываний
- •2.1.4. Дизъюнктивные и конъюнктивные нормальные формы в алгебре высказываний
- •2.1.5. Совершенные дизъюнктивные и конъюнктивные нормальные формы
- •Исчисление высказываний
- •Определение формального исчисления
- •Система аксиом и правил вывода
- •Теорема о дедукции в исчислении высказываний
- •Теорема о замене в исчисления высказываний
- •Свойства выводимых и эквивалентных формул исчисления высказываний
- •Основные эквивалентности исчисления высказываний
- •Полнота и непротиворечивость исчисления высказываний
- •Логика предикатов
- •Алгебраические системы
- •Пример 3. Построить подсистему алгебраической системы , порожденную множествомХ:
- •Формулы логики предикатов
- •Истинность формулы логики предикатов в алгебраической системе
- •2.3.4. Логическое следствие в логике предикатов
- •2.3.5. Эквивалентные формулы логики предикатов
- •2.3.6. Пренексная нормальная форма в логике предикатов
- •X(φ∧ψ)≡xφ∧ψ, X(φ∨ψ)≡xφ∨ψ,
- •X(φ∧ψ)≡xφ∧ψ, X(φ∨ψ)≡xφ∨ψ,
- •Xφ≡X(φ)xφ≡X(φ)
- •2.4. Исчисление предикатов
- •2.4.1. Система аксиом и правил вывода
- •2.4.2. Эквивалентные формулы исчисления предикатов
- •2.4.3. Теорема Геделя о полноте. Непротиворечивость исчисления предикатов
- •Элементы теории алгоритмов
- •2.5.1. Машины Тьюринга
- •2.5.2. Примитивно рекурсивные функции
- •2.5.3. Частично рекурсивные функции
- •Задания для домашних и контрольных работ
- •3.1. Совершенные дизъюнктивные нормальные формы, совершенные конъюнктивные нормальные формы
- •3.2. Логическое следствие в алгебре высказываний
- •Логическое следствие в логике предикатов
- •Частично рекурсивные функции
- •Список литературы
- •Основная литература
- •4.2. Дополнительная литература
- •Содержание
2.3.6. Пренексная нормальная форма в логике предикатов
Формула φ сигнатуры Σ называется бескванторной, если она не содержит кванторов. Бескванторная формула φ является дизъюнктивной (конъюнктивной) нормальной формой, если она получается из некоторой формулы ψ АВ, находящейся в ДНФ (КНФ), заменой всех пропозициональных переменных x1,…,xn на некоторые атомарные формулы φ1,…,φn сигнатуры Σ соответственно.
Говорят, что формула φ сигнатуры Σ находится в пренексной нормальной форме (ПНФ), если она имеет вид Q1x1…Qnxnψ, где Qi, ‑ кванторы (1≤i≤n), n ψ – дизъюнктивная нормальная форма.
Теорема 1. Для любой формулы φ сигнатуры Σ существует ПНФ ψ, эквивалентная формуле φ.
Опишим алгоритм приведения формулы к ПНФ:
выражаем импликацию, участвующую в построении формулы, через дизъюнкцию и отрицание, используя эквивалентность φ→ψ≡¬φ∨ψ;
используя законы де Моргана ¬(φ∧ψ)≡¬φ∨¬ψ, ¬(φ∨ψ)≡¬φ∧¬ψ
и эквивалентности ¬xφ≡x¬φ, ¬xφ≡x¬φ,
переносим все отрицания к атомарным подформулам и сокращаем двойные отрицания по правилу ¬¬φ≡φ;
приводим формулу к виду Q1x1…Qnxnψ , где Qi, ‑ кванторы (1≤i≤n), n ψ – бескванторная формула, пользуясь эквивалентностями
X(φ∧ψ)≡xφ∧ψ, X(φ∨ψ)≡xφ∨ψ,
X(φ∧ψ)≡xφ∧ψ, X(φ∨ψ)≡xφ∨ψ,
Xφ≡X(φ)xφ≡X(φ)
используя закон дистрибутивности
φ∧(ψ∨χ)≡(φ∧ψ)∨(φ∧χ),
преобразуем формулу ψ к дизъюнктивной нормальной форме.
Пример 10. Формулу χxyφ(x,y)→xyψ(x,y) привести к ПНФ, считая формулы φ и ψ атомарными.
Решение. Избавившись от импликации, получаем
χ≡¬(xyφ(x,y))∨xyψ(x,y).
Переносим отрицание к атомарной подформуле φ(x,y):
χ≡xy¬φ(x,y)∨xyψ(x,y).
Так как в формуле xyψ(x,y) переменные х, у являются связанными, то по пп. 2΄, 3΄ утверждения 2 имеем
χ≡xy(¬φ(x,y)∨xyψ(x,y)).
Пусть u, v ‑ некоторые новые переменные. Тогда по пп. 4, 4΄ утверждения 2 получаем
χ≡xy(¬φ(x,y)∨uv ψ(u,v)),
откуда по по пп. 2΄, 3΄ утверждения 2
χ≡xyuv(¬φ(x,y)∨ψ(u,v)).
Формула ¬φ(x,y)∨ψ(u,v) является дизъюнктивной нормальной формой, а значит, формула xyuv(¬φ(x,y)∨ψ(u,v)) является ПНФ.
2.4. Исчисление предикатов
2.4.1. Система аксиом и правил вывода
Зафиксируем некоторую произвольную сигнатуру Σ и определим исчисление предикатов сигнатуры Σ (ИПΣ).
Формулами ИПΣ будут формулы сигнатуры Σ.
Примем следующие соглашения. Пусть x1,…,xn ‑ переменные, t1,…,tn ‑ термы сигнатуры Σ и φ ‑ формула сигнатуры Σ.Запись будет обозначать результат подстановки термов t1,…,tn вместо всех свободных вхождений в φ переменных x1,…,xn соответственно, причем, если в тексте встречается запись , то предполагается, что для всех i{1,...,n} ни одно свободное вхождение в φ переменной xi не входит в подформулу φ вида y или y, где у – переменная, входящая в ti.
Аксиомами ИПΣ являются следующие формулы для любых формул φ, ψ, χ ИПΣ, любых переменных x,y,z и любого терма t:
φ→(ψ→φ);
(φ→ψ)→((φ→(ψ→χ))→(φ→χ));
(φ∧ψ)→φ;
(φ∧ψ)→ψ;
(φ→ψ)→((φ→χ)→(φ→(ψ∧χ)));
φ→(φ∨ψ);
φ→(ψ∨φ);
(φ→χ)→((ψ→x)→((φ∨ψ)→χ));
(φ→ψ)→((φ→¬ψ)→¬φ);
¬¬φ→φ;
xφ→(φ)tx;
(φ)tx→xφ;
x=x;
x=y→((φ)xz→(φ)yz).
Указанные формулы называются схемами аксиом ИПΣ. При подстановке конкретных формул в какую-либо схему получается частный случай схемы аксиом.
Правила вывода ИПΣ:
где в правилах 2 и 3 переменная x не входит свободно в χ.
Говорят, что формула φ выводима в ИПΣ из формул φ1,…,φm (обозначается φ1,…,φm⊢φ), если существует последовательность формул ψ1,…,ψk,φ, в которой любая формула либо является аксиомой, либо принадлежит множеству формул {φ1,…,φm}, называемых гипотезами, либо получается из некоторых φ1,…, φi-1 по одному из правил вывода 1-3? Причем при применении правил 2 и 3 переменная x не должна входить ни в одну гипотезу свободно. Выводимость формулы φ из (⊢φ) равносильна тому, что φ ‑ теорема ИПΣ или доказуемая формула ИПΣ.
Так же, как в исчислении высказываний, определяется понятие квазивывода.
Формула ψ ИПΣ называется тавтологией в ИПΣ, если она получается из формулы φ исчисления высказываний, доказуемой в исчислении высказываний, путем замены всех ее пропозициональных переменных x1,…,xn на формулы ψ1,…,ψn ИПΣ соответственно. Формулу φ при этом называют основой тавтологии.
Утверждение 1. Любая тавтология φ в ИПΣ доказуема в ИПΣ.
Формулы φ и ψ ИПΣ называются пропозиционально эквивалентными, если φ→ψ и ψ→φ – тавтологии. Формулы φ и ψ ИПΣ называются эквивалентными (обозначаем φ≡ψ), если ⊢φ→ψ и ⊢ψ→φ.
Следствие 1. Если φ и ψ ‑ пропозиционально эквивалентные формулы ИПΣ, то φ и ψ ‑ эквивалентные формулы ИПΣ.
Теорема 1 (о дедукции). Пусть φ1,…,φm,φ,ψ – формулы ИПΣ. Тогда φ1,…,φm,φ⊢ψ φ1,…,φm,⊢φ→ψ.
Следствие 2. Пусть φ и ψ ‑ формулы ИПΣ. Следующие условия эквивалентны:
φ≡ψ;
φ⊢ψ и ψ⊢φ.