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

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