Реферат Курсовая Конспект
Система аксиом и правил вывода - раздел Информатика, ПРОГРАММА КУРСА МАТЕМАТИЧЕСКАЯ ЛОГИКА И ТЕРИЯ АЛГОРИТМОВ Используя Понятие Формального Исчисления, Определим Исчисление Высказывани...
|
Используя понятие формального исчисления, определим исчисление высказываний (ИВ).
Алфавит ИВ состоит из букв x,y,z,u,v, возможно с индексами (которые называются пропозициональными переменными), логических символов (связок) ¬, ∧, ∨, →, а также вспомогательных символов (, ).
Множество формул ИВ определяется индуктивно:
а) все пропозициональные переменные являются формулами ИВ;
б) если φ, ψ ‑ формулы ИВ, то ¬φ, (φ∧ψ), (φ∨ψ), (φ → ψ) – формулы ИВ;
в) выражение является формулой ИВ тогда и только тогда, когда это может быть установлено с помощью пунктов "а" и "б".
Таким образом, любая формула ИВ строится из пропозициональных переменных с помощью связок ¬, ∧, ∨, →.
В дальнейшем при записи формул будем опускать некоторые скобки, используя те же соглашения, что и в предыдущей главе.
Подформулой ψ формулы φ ИВ называется подслово φ, являющееся формулой ИВ.
Под длиной формулы будем понимать число символов, входящих в слово φ.
Аксиомами ИВ являются следующие формулы для любых формул φ, ψ, χ ИВ:
1) φ→(ψ→φ);
2) (φ→ψ)→((φ→(ψ→χ))→(φ→χ));
3) (φ∧ψ)→φ;
4) (φ∧ψ)→ψ;
5) (φ→ψ)→((φ→χ)→(φ→(ψ∧χ)));
6) φ→(φ∨ψ);
7) φ→(ψ∨φ);
8) (φ→χ)→((ψ→x)→((φ∨ψ)→χ));
9) (φ→ψ)→((φ→¬ψ)→¬φ);
10) ¬¬φ→φ.
Указанные формулы называются схемами аксиом ИВ. При подстановке конкретных формул в какую-либо схему получается частный случай схемы аксиом.
Единственным правилом вывода в ИВ является правило заключения (modus ponens): если φ и φ→ψ ‑ выводимые формулы, то ψ ‑ также выводимая формула. Символически это записывается так:
Говорят, что формула φ выводима в ИВ из формул φ1,…,φm (обозначается φ1,…,φm⊢φ), если существует последовательность формул ψ1,…,ψk,φ, в которой любая формула либо является аксиомой, либо принадлежит множеству формул {φ1,…,φm}, называемых гипотезами, либо получается из предыдущих по правилу вывода. Выводимость формулы φ из (⊢φ) равносильна тому, что φ ‑ теорема ИВ или доказуемая формула ИПΣ.
Пример 1. Покажем, что ⊢φ→φ.
Решение. Построим вывод данной формулы:
1) (φ→(φ→φ))→((φ→((φ→φ)→φ)→(φ→φ)) (схема аксиом 2);
2) φ→(φ→φ) (схема аксиом 1);
3) (φ→((φ→φ)→φ))→(φ→φ) (к пп. 2 и 1 применили правило вывода);
4) φ→((φ→φ)→φ) (схема аксиом 1);
5) φ→φ (к пп. 4 и 3 применили правило вывода).
Квазивыводом в ИВ формулы φ из формул φ1,…,φm называется последовательность формул ψ1,…,ψk,φ, в которой любая формула , либо принадлежит множеству формул {φ1,…,φm}, либо выводима из предыдущих.
Замечание 1. Если существует квазивывод в ИВ формулы φ из формул φ1,…,φm, то φ выводима в ИВ из формул φ1,…,φm.
Пример 2.Покажем, что φ,ψ⊢φ ψ.
Решение: Построим квазивывод формул φ ψ из φ и ψ:
1) φ (гипотеза);
2) ψ (гипотеза);
3) (φ→φ)→((φ→φ)→(φ→φ ψ)) (схема аксиом 5);
4) φ→φ (теорема ИВ по примеру 1);
5) ((φ→ψ)→(φ→φ ψ)) (к пп. 4 и 3 применили правило вывода);
6) ψ→(φ→ψ) (схема аксиом);
7) φ→ψ (к пп. 2 и 6 применили правило вывода);
8) φ→φ ψ (к пп. 7 и 5 применили правило вывода);
9) φ ψ (к пп. 1 и 8 применили правило вывода).
Пример 3. Покажем, что φ⊢¬¬φ.
Решение. Построим квазивывод формулы ¬¬φ из формулы φ:
1) φ (гипотеза);
2) (¬φ→φ)→((¬φ→¬φ)→¬¬φ) (схема аксиом 9);
3) φ→(¬φ→φ) (схема аксиом 1);
4) ¬φ→φ (к пп. 1 и 3 применили правило вывода);
5) (¬φ→¬φ)→¬¬φ (к пп. 4 и 2 применили правило вывода);
6) ¬φ→¬φ (теорема ИВ по примеру 2);
7) ¬¬φ (к пп. 6 и 4 применили правило вывода).
– Конец работы –
Эта тема принадлежит разделу:
Логика это наука о законах мышления Это одна из древнейших наук Основные законы логики были сформулированы еще древнегреческим мыслителем... Современная математическая логика определяется как раздел математики... Данное учебно практическое пособие соответствует учебной программе курса Математическая логика и теория алгоритмов...
Если Вам нужно дополнительный материал на эту тему, или Вы не нашли то, что искали, рекомендуем воспользоваться поиском по нашей базе работ: Система аксиом и правил вывода
Если этот материал оказался полезным ля Вас, Вы можете сохранить его на свою страничку в социальных сетях:
Твитнуть |
Новости и инфо для студентов