рефераты конспекты курсовые дипломные лекции шпоры
- Раздел Математика
- /
- Формальное исчисление высказываний
Реферат Курсовая Конспект
Формальное исчисление высказываний
Формальное исчисление высказываний - раздел Математика, КОНСПЕКТ ЛЕКЦИЙ ПО МАТЕМАТИЧЕСКОЙ ЛОГИКЕ Подробно Рассмотрим Формальную Теорию Исчисления Высказываний (Ив). На...
Подробно рассмотрим формальную теорию исчисления высказываний (ИВ). Нашей целью будет обоснование адекватности этой теории, описанной формально в § 1 главы III, неформальной алгебре высказываний, изученной в главе I. Под адекватностью формальной теории её неформальному аналогу понимается доказательство всех основных теорем неформальной теории в соответствующей формальной теории. В частности, будет доказано, что формула доказуема в формальной теории исчисления высказываний тогда и только тогда, когда она тождественно истинна.
1. Свойства выводимости формул.Докажем некоторые основные свойства выводимости формул.
10. Всякая доказуемая формула выводима из любой совокупности формул. В частности, любая аксиома выводима из любой совокупности формул.
Действительно, доказательство формулы является и её выводом из любой совокупности формул, т.к. в нём используются аксиомы и правило вывода modus ponens. Последовательность из одной этой аксиомы является её доказательством.
20. Из любой совокупности выводима любая формула этой совокупности.
В самом деле, если Г = {А1 , … , Аi , … , Аn }, то последовательность из одной формулы Аi является выводом формулы Аi из совокупности Г.
30. Доказуемая формула выводима из любой совокупности формул.
Действительно, доказательство этой формулы является её выводом из любой конечной совокупности формул.
40. Если существует квазивывод формулы В из совокупности Г, т.е. конечная последовательность формул В1 , … , Вk = B, каждая формула которой либо выводима из Г, либо получена из двух предыдущих по правилу modus ponens, то формула В выводима из Г.
Нужно просто заметить, что квазивывод расширится до вывода, если вместо каждой выводимой из Г формулы Вi вставить её вывод из совокупности Г.
50. Если Г 
Ф, то для любой совокупности формул D верно Г, D Ф.
В самом деле, вывод формулы В1 , … , Вk = B из совокупности Г является её выводом и из расширенной совокупности Г, D .
60. Если Г Ф и Г (Ф ® Y), то Г Y .
Действительно, если В1 , … , Вk = Ф – вывод формулы Ф, а С1 , … , Сm = = (Ф ® Y ) – вывод формулы (Ф ® Y ), то В1 , … , Вk = Ф, С1 , … , Сm = = (Ф ® Y ), Y – вывод формулы Y, т.к. последняя формула этой цепочки получена из предыдущих Ф и (Ф ® Y) по правилу modus ponens.
Замечание: На самом деле в свойствах 50 и 60 обоснованы правила вывода 
– расширения посылок и 
– расширение modus ponens. Теперь ими можно пользоваться при выводе формул, сокращая длину доказательства. Дальнейший ход изложения лишь увеличит количество полезных правил вывода.
2. Теорема о дедукции:Обоснуем доказанные в главе I неформально правила дедукции: 
.
Теорема (о дедукции).Для формул А, В и произвольной конечной совокупности формул Г (возможно пустой) утверждение Г, А В имеет место тогда и только тогда, когда Г (А ® B).
Доказательство. Вначале докажем “лёгкую” импликацию (Ü). Если верно Г (А ® B), то (по правилу расширения посылок) Г, А (А ® B) и Г, А А (используется 20). Применяя расширение modus ponens, получим Г, А В, что и требовалось.
(Þ) Рассмотрим вывод В1 , … , Вk = В формулы В из совокупности Г, А . Если k = 1, то этот вывод состоит из одной формулы В и возможны случаи:
а: В – аксиома.Тогда цепочка (B ® (A ® B)), B, (A ® B) будет доказательством формулы (A ® B) и выводом её из совокупности Г. Последняя формула цепочки получена из предыдущих по правилу modus ponens.
б: В – формула совокупности Г, А. Если В = А , то (А ® B) = (A ® A) – доказуемая формула (см. пример доказательства в § 1), которая выводима из любого множества формул по свойству 10. Если же В Î Г, то цепочка (B ® (A ® B)), B, (A ® B) является выводом формулы (A ® B) из Г.
Пусть теперь k > 1 и неверно, что Г (А ® B). Можно считать, что k – наименьшее натуральное число с этим свойством. Таким образом, для любых формул Ф, Y со свойством Г, Ф Y и длиной этого вывода меньше k будет верно Г (Ф ® Y).
В случаях, когда В – аксиома или формула совокупности Г, А применимы использованные ранее для k = 1 аргументы. Значит можно считать, что последняя формула В рассматриваемого вывода получена из двух предыдущих по правилу modus ponens. Итак, среди формул вывода В есть формулы Вi = C, Bj = (C ® B), где i < k, j < k, т.е. Г, А С и Г, А (C ® B) с длинами выводов, меньшими k. Учитывая предположение о минимальности k, получаем Г (А ® C) и Г (А ® (C ® B)). Теперь можно написать квазивывод формулы (А ® B) из множества формул Г :
1· ((A ® (C ® B)) ® ((A ® C) ® (A ® B))) (И2) (А := A, B := C, С := B)
2 ·(A ® (C ® B)) выводима из Г
3 ·((A ® C) ® (A ® B)) МР(1, 2)
4 ·(A ® C)выводима из Г
5 · (A ® B) МР(3, 4)
Теорема о дедукции доказана.
3. Производные правила вывода.Обоснуем некоторые знакомые правила логического вывода. Остальные правила докажите самостоятельно.
Правило перестановки посылок:
. Запишем квазивывод формулы (В ® (A ® C)), предполагая, что (А ® (В ® C)) выводима.
1 · Г (А ® (В ® C))дано
2 · Г, А (В ® C) дедукция
3 · Г, А, В С дедукция
4 · Г, В (А ® C) дедукция
5 · Г (В ® (А ® C)) дедукция
Правила силлогизма: 
.
1 · Г В дано
2 · В С дано
3 · Г, В С расширение посылок
4 · Г (В ® С) дедукция
5 · Г СМР(1, 4)
1 · Г, А В дано
2 · Г (А ® B) дедукция
3 · Г, В С дано
4 · Г (В ® С) дедукция
5 · ((В ® C) ® (A ® (B ® C)))(И1)(A := (B ® C), B := A)
6 · Г (A ® (B ® C)) МР(4, 5)
7 · ((А ® (B ® C)) ® ((A ® B) ® (A ® C))) аксиома (И2)
8 · Г ((A ® B) ® (A ® C)) МР(6, 7)
9 · Г (A ® C) МР(2, 8)
10 · Г, А C дедукция
Правило объединения посылок:
.
1 · Г (А ® (В ® С)) дано
2 · Г, А (В ® С) дедукция
3 · ((А ® A) ® ((A ® B) ® (A ® (A Ù B)))) (К3) (A := A =: B, C := B)
– Конец работы –
Эта тема принадлежит разделу:
КОНСПЕКТ ЛЕКЦИЙ ПО МАТЕМАТИЧЕСКОЙ ЛОГИКЕ
Государственное образовательное учреждение... Тобольская государственная социально педагогическая академия... им Д И Менделеева...
Если Вам нужно дополнительный материал на эту тему, или Вы не нашли то, что искали, рекомендуем воспользоваться поиском по нашей базе работ: Формальное исчисление высказываний
Что будем делать с полученным материалом:
Если этот материал оказался полезным ля Вас, Вы можете сохранить его на свою страничку в социальных сетях:
| Твитнуть |
Хотите получать на электронную почту самые свежие новости?
Подпишитесь на Нашу рассылку
Реклама
Информация в виде рефератов, конспектов, лекций, курсовых и дипломных работ имеют своего автора, которому принадлежат права. Поэтому, прежде чем использовать какую либо информацию с этого сайта, убедитесь, что этим Вы не нарушаете чье либо право.
© copyright 1999 - 2024 allRefs.net. Все права защищены. Страница сгенерирована за: 0.023 сек.
Новости и инфо для студентов