Студопедия — Система аксиом и правил вывода. Используя понятие формального исчисления, определим исчисление высказываний (ИВ)
Студопедия Главная Случайная страница Обратная связь

Разделы: Автомобили Астрономия Биология География Дом и сад Другие языки Другое Информатика История Культура Литература Логика Математика Медицина Металлургия Механика Образование Охрана труда Педагогика Политика Право Психология Религия Риторика Социология Спорт Строительство Технология Туризм Физика Философия Финансы Химия Черчение Экология Экономика Электроника

Система аксиом и правил вывода. Используя понятие формального исчисления, определим исчисление высказываний (ИВ)






Используя понятие формального исчисления, определим исчисление высказываний (ИВ).

Алфавит ИВ состоит из букв 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 применили правило вывода).

 







Дата добавления: 2014-11-10; просмотров: 901. Нарушение авторских прав; Мы поможем в написании вашей работы!



Композиция из абстрактных геометрических фигур Данная композиция состоит из линий, штриховки, абстрактных геометрических форм...

Важнейшие способы обработки и анализа рядов динамики Не во всех случаях эмпирические данные рядов динамики позволяют определить тенденцию изменения явления во времени...

ТЕОРЕТИЧЕСКАЯ МЕХАНИКА Статика является частью теоретической механики, изучающей условия, при ко­торых тело находится под действием заданной системы сил...

Теория усилителей. Схема Основная масса современных аналоговых и аналого-цифровых электронных устройств выполняется на специализированных микросхемах...

Тема 5. Организационная структура управления гостиницей 1. Виды организационно – управленческих структур. 2. Организационно – управленческая структура современного ТГК...

Методы прогнозирования национальной экономики, их особенности, классификация В настоящее время по оценке специалистов насчитывается свыше 150 различных методов прогнозирования, но на практике, в качестве основных используется около 20 методов...

Методы анализа финансово-хозяйственной деятельности предприятия   Содержанием анализа финансово-хозяйственной деятельности предприятия является глубокое и всестороннее изучение экономической информации о функционировании анализируемого субъекта хозяйствования с целью принятия оптимальных управленческих...

Типовые ситуационные задачи. Задача 1. Больной К., 38 лет, шахтер по профессии, во время планового медицинского осмотра предъявил жалобы на появление одышки при значительной физической   Задача 1. Больной К., 38 лет, шахтер по профессии, во время планового медицинского осмотра предъявил жалобы на появление одышки при значительной физической нагрузке. Из медицинской книжки установлено, что он страдает врожденным пороком сердца....

Типовые ситуационные задачи. Задача 1.У больного А., 20 лет, с детства отмечается повышенное АД, уровень которого в настоящее время составляет 180-200/110-120 мм рт Задача 1.У больного А., 20 лет, с детства отмечается повышенное АД, уровень которого в настоящее время составляет 180-200/110-120 мм рт. ст. Влияние психоэмоциональных факторов отсутствует. Колебаний АД практически нет. Головной боли нет. Нормализовать...

Эндоскопическая диагностика язвенной болезни желудка, гастрита, опухоли Хронический гастрит - понятие клинико-анатомическое, характеризующееся определенными патоморфологическими изменениями слизистой оболочки желудка - неспецифическим воспалительным процессом...

Studopedia.info - Студопедия - 2014-2024 год . (0.012 сек.) русская версия | украинская версия