Логика и теория аргументации. Скачков А.С. - 97 стр.

   Правило исключения отрицания является однопосылочным и позволяет сни-
мать двойное отрицание с любой формулы.

     ™ Пример
   Если в рассуждениях есть формула ¬¬А, являющаяся формулой ¬¬(p⊃q), то
применяя правило ¬и, получим новую формулу (p⊃q).

                       7.3. Выводы и доказательства

   Посредством правил вывода строятся формальные рассуждения двух видов:
   1. Выводы.
   2. Доказательства.
   Вывод — это не пустая и конечная последовательность формул, каждая из
которых является либо посылкой, либо получена из предыдущих формул согласно
одному из дедуктивных принципов так, что после применения правил ⊃в и ¬в все
формулы, начиная с последней посылки и вплоть до результата применения дан-
ного правила, не используются в дальнейших шагах построения вывода. Выпав-
шие из дальнейших шагов построения вывода формулы называются исключён-
ными (замороженными), соответственно исключёнными называются выражаемые
такими формулами посылки.
   Вывод может быть получен либо из пустого множества замороженных по-
сылок (когда часть посылок оказываются не исключёнными в ходе рассуждения),
либо из непустого множества замороженных посылок (когда все посылки ока-
зываются исключёнными в ходе рассуждения). Так, различают собственно вывод
— рассуждение, в ходе которого из каких-либо исходных суждений, посылок вы-
вода получается заключение — суждение, логически вытекающее из посылок, и
вывод-доказательство.
   Доказательство есть вывод из непустого множества неисключенных посы-
лок, при этом последняя формула вывода — это доказанная формула (теорема).
Доказать какую-либо формулу, значит вывести её из формул посылок таким об-
разом, чтобы, используя дедуктивные принципы ⊃в или ¬в, перевести все эти
формулы в разряд исключённых.
   В целом структура любого вывода может быть представлена последователь-
ностью формул, располагающихся, например, друг под другом. Каждая из фор-
мул этой последовательности в исчислении высказываний нумеруется натураль-
ными числами.

      ™ Пример
   Если требуется вывести формулу ¬p из посылок p⊃¬p и p (записывается:
p⊃¬p, p |- ¬p, читается: «из посылок p⊃¬p и p выводимо ¬p», где « |- » — знак
выводимости), то следует найти и записать такую последовательность формул, в
которой множество используемых посылок равно множеству формул p⊃¬p и p, а
последней оказывается именно выводимая формула ¬p:


                                     97