Математическая логика и теория алгоритмов

зывает, что данное правило исю1Ючает или вводит этот символ. Тогда рассмотренные правила моясно записать следующим образом: в теорема дедукции: GJt [-Б.-G =>; а =i' в у в правило перевертывания: \-В: ОЛв 1: . а&в - в правило удаления &; & ; а о ав „ в правило введения &: &; а&в а » правила введения v; v , а\/ в т правило доказательства разбором случаев: а \-c.b\c.awb у. С в правило сведения к нелепости: а в. а [-1Д 1 . Отметим, что перечисленные производные правила вывода позволяют намного упростить выкладаси в теории l. Подчер1шем, что в принципе можно и не пользоваться этими производными правилами вывода, а пользоваться только правилом mp. Однако при этом, может быть, придется проводить более громоздкие выкладки. Например, ес­ ли при выяснении, теорема или нет формула а, пользовались теоре­ мой дедукции, то при отказе от этой теоремы дедукции фактически придется ее доказывать для этого частного случая. В других подобных случаях снова придется ее доказывать. § 11. Свойства исчисления высказываний Непротиворечивость исчисленшвысказываний. Исчисление высказываний, как и любую формальную аксиоматическую теорию, содержащую символ 1, будем считать непротиворечивой, если ни для 158 ^ & • в ' - М _ в&а а V; bwa