![]() |
Главная Случайная страница Контакты | Мы поможем в написании вашей работы! | |
|
Тема: ФОРМАЛЬНЫЕ СИСТЕМЫ. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ
Основные вопросы, рассматриваемые на лекции:
1. Определение формальной системы
2. Метод доказательства индукцией по формулам
3. Выводом формулы из множества формул
4. Исчисление высказываний
Краткое содержание лекционного материала
Формальная система S определена, если:
1) Задано счетное множество символов. Конечная последовательность символов называется словом (или строкой).
2) Выделяется множество формул системы S – подмножество множества слов системы S. Обычно указывается алгоритм построения формул.
3) Выделяется множество аксиом системы S – подмножество множества формул системы S.
4) Выделяется множество правил вывода системы S – множество некоторых отношений между формулами системы S. Если P – правило вывода, (A 1,…, Am, B)ÎP, то формулы A 1,…, Am называются посылками, а формула B – заключением правила P. При этом говорят, что формула B непосредственно следует из формул A 1,…, Am.
Следующее определение формулы системы S 1 является частным случаем определения пропозициональной формулы.
Слово системы S 1 называется формулой системы S 1, если оно построено строго по следующим правилам:
1) пропозициональные переменные – формулы системы S 1;
2) если слово A системы S 1 является формулой системы S 1, то слово Ø A тоже является формулой системы S 1;
3) если слова A и B системы S 1 являются формулами системы S 1, то слово (A Þ B) тоже является формулой системы S 1.
Имеет место метод доказательства индукцией по формулам. Пусть для некоторого свойства формул P (A) доказаны следующие утверждения:
1) если p – пропозициональная переменная, то P (p) верно;
2) если P (A), то P (Ø A) тоже верно;
3) если P (A) верно и P (B) верно, то P (A Þ B) тоже верно.
Тогда свойства P (A) верно для всех формул A системы S 1.
Следующее определение теоремы системы S 1 является частным случаем определения логического следствия.
Выводом формулы A из множества формул G называется конечная последовательность формул A 1,…, An, если:
1) An = A;
2) для каждого i =1,…, n формула Ai
(a) является некоторой аксиомой, или
(b) принадлежит множеству G, или
(c) непосредственно следует по некоторому правилу вывода из формул Ai 1,…, Aim, где 1£ i 1,…, im < i.
При этом говорят, что формула A следует из множества формул G (или A следствие из множества G), и пишут G|¾ A (или G|¾ SA). Если G={ A 1,…, Am } – конечное множество, то пишут также A 1,…, Am |¾ A (или A 1,…, Am |¾ SA).
Формула A системы S называется теоремой системы S, если следует из пустого множества формул. Обозначение: |¾ A, или |¾ SA.
Исчисление высказываний – это формальная система, символами которой являются пропозициональные переменные и связки, а формулами – пропозициональные формулы. Рассмотрим исчисление высказываний S 1 с двумя связками Ø и Þ (остальные связки можно определить в терминах Ø и Þ, например, A Ú B =Ø A Þ B и A Ù B =Ø(A ÞØ B)) и со следующими аксиомами и правилом вывода:
(A 1) A Þ(B Þ A);
(A 2) (A Þ(B Þ C))Þ((A Þ B)Þ(A Þ C));
(A 3) (Ø B ÞØ A)Þ((Ø B Þ A)Þ B);
(MP) A, A Þ B |¾ B
(где A, B, C – это произвольные пропозициональные формулы, построенные из пропозициональных переменных и связок Ø и Þ).
Формула системы S называется теоремой системы S, если оно получено строго по следующим правилам:
1) аксиомы (A 1), (A 2), (A 3) являются теоремами системы S;
2) если посылки A и A Þ B правила (MP) – теоремы системы S, то его заключение B – тоже теорема системы S.
Имеет место метод доказательства индукцией по теоремам (мы сформулируем этот метод для теорем системы S). Пусть для некоторого свойства формул P (A) доказаны следующие утверждения:
1) если формула A – одна из аксиом (A 1), (A 2), (A 3), то P (A) верно;
2) если формула A непосредственно следует по правилу (MP) из формул B, B Þ A, P (B) верно, P (B Þ A) верно, то P (A) верно.
Тогда свойство P (A) верно для всех формул A (системы S 1).
При доказательстве общих свойств теорем системы S 1 мы используем индукцию по формулам или индукцию по теоремам, а при доказательстве конкретной теоремы системы S 1 – приводим вывод этой теоремы.
Дата публикования: 2015-03-26; Прочитано: 172 | Нарушение авторского права страницы | Мы поможем в написании вашей работы!