Свойства выводимых и эквивалентных формул исчисления высказываний
Утверждение 3. Пусть φ,ψ, χ – формулы ИВ. Тогда
⊢φ→φ;
φ∧ψ⊢φ;
φ∧ψ⊢ψ;
φ,ψ⊢φψ;
φ→ψ, ψ→χ⊢φ→χ (свойство транзитивности);
φ→(ψ→χ)≡ψ→(φ→χ) (свойство перестановочности посылок);
φ→(ψ→χ)≡φ∧ψ→χ (свойство соединения и разъединения посылок);
φ→ψ≡¬ψ→¬φ (свойство контрапозиции).
Доказательство. Пункты 1, 4, 6, 8 доказаны в примерах 13, 14, 16, 17.
Докажем пункт 7. Покажем, что φ→(ψ→χ)⊢φψ→χ. По теореме о дедукции
φ→(ψ→χ)⊢φψ→χφ→(ψ→χ), φψ⊢χ.
Строим вывод формулы χ из формул φ→(ψ→χ), φψ:
φ→(ψ→χ) (гипотеза);
φψ (гипотеза);
φψ→φ (схема аксиом 3);
φ (к пп. 2 и 4 применили правило вывода);
φψ→ψ (схема аксиом 4);
ψ (к пп. 2 и 5 применили правило вывода);
ψ→χ (к пп. 4 и 1 применили правило вывода);
χ (к пп. 6 и 7 применили правило вывода).
Покажем, что φψ→χ⊢φ→(ψ→χ). По теореме о дедукции
φψ→χ⊢φ→(ψ→χ)φψ→χ, φ⊢φ→χφψ→χ, φ, ψ⊢χ.
Строим квазивывод формулы χ из формул φψ→χ, φ, ψ:
φψ→χ (гипотеза);
φ (гипотеза);
ψ (гипотеза);
φψ (к п.п. 2 и 3 применили свойство 4);
χ (к пп. 4 и 1 применили правило вывода).
-
Содержание
- Введение
- Программа курса математическая логика и терия алгоритмов
- Логическое следствие в алгебре высказываний
- 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. Дополнительная литература
- Содержание