Дедуктивная система натурального вывода
Существуют различные, но эквивалентные между собой формы построения логической теории рассуждения. Наиболее удобной из них является система натурального вывода, содержащая только правила логического перехода или вывода от одних формул языка классической логики высказываний к другим.
Само название указывает на то, что выводы в данной системе близки к естественным формам практического рассуждения. Это значительно облегчает проверку логической корректности рассуждений и поиск методов такой проверки. Кроме того, система натурального вывода более удобна в методологии гуманитарных наук — юриспруденции, эстетики, этики, язык которых содержит нормативные и оценочные суждения, не имеющие истинностной интерпретации. Понятие логического следствия, определенное в терминах истинности, — заключение логически следует из посылок, если оно истинно при условии истинности посылок — не «работает» в языке с нормативными и оценочными суждениями. Действительно, в каком смысле это определение применимо для проверки корректности, скажем, рассуждения: «Если хочешь быть опрятным, должен бриться по утрам. Хочу быть опрятным. Следовательно, должен бриться утром»? Ведь заключение рассуждения не является ни истинным, ни ложным, а представляет собой норму.В системе натурального вывода понятие логического следствия определяется без использования понятия истинности. Заключение в рассуждении логически следует из посылок, если и только если оно выводимо из заданных посылок по определенным для системы логическим правилам. Выводом в натуральной системе будем называть последовательность формул языка классической логики высказываний, каждая из которых является либо посылкой, либо формулой, полученной из предшествующих в последовательности формул по определенным в системе логическим правилам. Последняя формула последовательности вывода называется выводимой формулой или заключением вывода.
Логические правила вывода контролируют две формы оперирования логическими связками языка в исследовании информации. В процессе анализа информация расчленяется на составные части удалением из нее логических связок; в процессе синтеза, наоборот, разрозненная информация объединяется в целое введением в нее соединяющих логических связок. Итак, различают правила введения и удаления.
Основные правила логического вывода:
[уо] -і-iA =gt; А [во] А =gt; В, А —» —iB
—iA
[УК ]АлВ=gt;А;АлВ=5В [вк]а,В=gt;АлВ
[УД] A=gt;C, B=gt;C, AvB=gt;C [ВД] A=gt;AvB;B=gt;AvB
[УИ] А -» В, А =gt; В [ВИ] Г, А =gt; В, где Г - формулы
Г =gt; А —gt; В, вывода
Правило введения отрицания [ВО] называют также правилом сведения к противоречию — или правилом рассуждения от противного. Оно утверждает, что для обоснования выводимости некоторой формулы, например —iA, достаточно ввести в вывод в качестве дополнительной посылки косвенного допущения (п.к.д.) ее отрицание, то есть А, и показать, что сделанное допущение влечет противоречие: В и —iB.
|
| А -» В, | — В - у —А | Правило «модус толленс» [МТ] |
| 1. | А В | посылка |
|
| 2. | В | посылка |
|
| 3. | -.-.А | П.К.Д. |
|
| 4. | А | (3), УО |
|
| 5. | В | (1,4), У И (1), (5) - | противоречие. |
Правило удаления дизъюнкции [УД] называют также правилом рассуждения по случаям. Оно утверждает, что для обоснования выводимости формулы из посылок, содержащих дизъюнкцию, т.е.
A v В =» С, достаточно доказать два случая: когда в качестве посылки используется один дизъюнктор, т.е. А=»С, и когда посылкой является другой дизъюнктор, т.е. В=»С.A v В, -.В =gt; А Правило «модус толлендо поненс» [МТП]
| 1. 1. | А | посылка | 2. 1. | В | посылка |
| 2. | -,В | посылка | 2. | -,В | посылка |
| 3. | -А | П.К.Д. | 3. | —.А | П.К.Д. |
(II, (3) — противоречие. (1), (2) — противоречие.
Правило удаления импликации [УИ] называют также правилом «модус поненс» [МП].
Правило введения импликации [ВИ] называют также принципом дедукции [ПД]. Оно утверждает, что для обоснования выводимости формулы, имеющей импликативную структуру, т.е. Г=gt; А—gt;В, достаточно построить вывод ее консеквента, в котором антецедент импликативной формулы фигурирует в качестве посылки, т.е. Г, А =» В.
А В, В -у С =gt; А -у С Правило силлогизма [ПС]
А -gt; В, В -» С, А =gt; С по правилу [ВИ] [ПД]
| 1. | А—gt;В | посылка |
| 2. | В -gt; С | посылка |
| 3. | А | посылка |
| 4. | В | (1,3), МП [УИ] |
| 5. | С | (2,4), МП [УИ] |
В системе натурального вывода различают Основные и производные логические правила. Производные правила выводимы из основных и после своего логического обоснования могут использоваться в последующих рассуждениях.
Таким образом, правила МТ, МТП и ПС являются производными в системе натурального вывода.| -.(А а-,в), В С =» -,С -» -.А | ||||
| .(л а —iB) В —gt; С, —Г gt; -Л |
|
| [ПД] | |
| 1. -п(а л -,в) | посылка | 5. | А | (4), УО |
| 2. В -gt; С | посылка | 6. | -,В | (2, 3), МТ |
| 3. -.с | посылка | 7. | А л-.В | (5, 6), ВК |
| 4. -.-iA | П.К.Д. | (Т), | (7) — противоречие. | |
В натуральной системе различают прямой и косвенный вывод. Прямым выводом называется переход по логическим правилам от данной, уже полученной в выводе формулы к выводимой, то есть результирующей формуле. Косвенным выводом называется переход от данного вывода к результирующему выводу по логическим правилам. Таким образом, основные логические правила ВО, УД и ВИ являются правилами косвенного вывода. С другой стороны, построенный выше вывод А В, В—gt; С, А С является прямым, так как в нем осуществляется переход от формулы к формуле, но не от вывода к выводу. Построение прямого вывода обычно представляет эвристические трудности, — да мы так и не рассуждаем, — поэтому косвенный вывод принципиально облегчает нахождение метода нормализации вывода.
| А -,((В л —iC) v d), С—»Е=gt;В—gt;(А—»е) |
|
| А -gt; -,((В л -,С) v D), С Е, В =gt; А Е | [ПД] |
| А Д(В a-.C)v D), С Е, В, А =gt; Е | [І1Д] |
| 1. | А -gt; —і((в л —.c)v d) | посылка | 6. | —.([в л —iC)v в) | (1, 4), МП |
| 2. | С -gt; Е | посылка | 7. | -,с | (2, 5), МТ |
| 3. | В | посылка | 8. | В А —iC | (3, 7), ВК |
| 4. | А | посылка | 9. | (В л —iC)v D | (8). ВД |
| 5. | -Е | п.к.д. | (6), (9) — противоречие. | ||
Укажите применение производного и косвенного правил вывода.
Упражнения
- Дайте необходимые логические обоснования для каждого шага следующего вывода:
-A v В, -.С -» -Н, Д(с л -4gt;) v е) =gt; Д(А л -Л)) V е)
*- —і А, —iC —gt; —iB, —((С л —ОО) v Е) =» Д(А a4))vE)
П- В, -,С -> -,В, -{(с a-J))vE)^ -,((А л -,») V Е)
| 1. -А |
|
| 2. -.С |
|
|
|
| 6.1. A a-.D | 6.2. Е |
| 7.1. А | 7.2. (с л -jo) v Е . |
| (?) — противоречие 1. В | (?) — противоречие |
| 2. -,С -gt; -,В |
|
|
|
| 6.1. A л-iD | 6.2. Е |
| 7.1. -JD | 7.2. (Ca-Od)vE |
| 8.1. С | (?) — противоречие |
| 9.1. С л-iD |
|
| 10.1. (Ca-JD)vE | (?) — противоречие |
- Установите логическую корректность следующих рассуждений методом натурального вывода. Подберите подходящие примеры перевода логических структур рассуждений на естественный язык.
- —(А а -iB), —iC —gt; ~iB, —iD —gt; -iC, -iD v E =gt; A —gt; E;
- —iB —gt;—iA, —iB v С, —iC v D, —i(d v —iE) =gt; —i(A a —iE);
- —iB —gt; —iA, —i(b a—iC), ~iD —gt; —iC, I) —gt; E =gt; A —gt; E;
- A -gt; -i(b a -iC), BvC,C-gt;D=gt; -iD -gt; -iA;
- —iA v В, —i(b a—iC), —iC v D, D —gt; E =gt; —i(A л-iE);
- (в a -iC) —gt; —iA, —iB —gt; С, —i(c a ~iD), -iD v E =» A —gt; E.
- Задача. Ограблен склад. Подозреваются лишь А, Б или С. Известно, что С всегда «работает» без помощников. А и Б — близнецы, по характеру робки и всегда «идут на дело» с соучастником. Одного из близнецов в момент ограбления видели в другом конце города. Кто виновен? (Решите задачу и укажите логические правила вывода, используемые при ее решении.)