Полнота и непротиворечивость исчисления высказываний
Формула φ(x1,…,xn) ИВ называется тождественно истинной (обозначается ⊨φ), если φ(x1,…,xn) – тождественно истинная формула как формула алгебры высказываний.
Теорема 4 (о полноте). Формула φ ИВ доказуема тогда и только тогда, когда φ тождественно истинна:
φ⊨φ.
Таким образом, для того чтобы установить, доказуема ли формула ИВ, достаточно составить ее таблицу истинности. Как известно, существует эффективный алгоритм построения таблицы истинности, и, значит, ИВ разрешимо. Кроме того, из теоремы о дедукции и теоремы о полноте легко следует, что отношение эквивалентности ≡ в АВ и ИВ совпадают.
Теорема 5 (о непротиворечивости). ИВ непротиворечиво.
Доказательство. По теореме о полноте любая формула, не являющаяся тождественно истинной, не доказуема в ИВ. Например, такой формулой является формула х∧¬х. Следовательно, ИВ непротиворечиво.
Схема аксиом называется независимой в исчислении, если хотя бы один ее частный случай не доказуем в исчислении без этой схемы.
Теорема 6. Схемы аксиом ИВ независимы.
-
Содержание
- Введение
- Программа курса математическая логика и терия алгоритмов
- Логическое следствие в алгебре высказываний
- 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. Дополнительная литература
- Содержание