Колмогоров, Драгалин - Введение в математическую логику, страница 9

Последняя из тавтологий служит основанием для проведения доказательств от противного: если отрицание А прцводит к противоречию, то А верно. Чтобы убедиться, что формула Р(Рь, Р,) является тавтологией, достаточно проделать довольно громоздкую, но всегда выполнимую процедуру вычисления соответствующей функции 1(хь ..., х„) для всевозможных наборов значений переменных. Таким образом, всегда можно эффективно установить, является л~и данная формула тйвтологней или нет.

Две формулы Р и 6 равносильны или логически эквивалентны, если формула (Р=б) является тавтологией. Иными словами, если Р и О рассматривать как задающие булевы функции от одних,и' тех же,переменных, то Р и б задают одну и ту же функцию. ' Существует несколько «нормальныХ форм» формул логики высказываний. Упомянем о совершенной дизъюнктивной нормальной форме, которая вполне аналогична установленной в 5 б для булевых функций. Для ~пропозициональных переменных Рь ..., Р, будем называть совершенным конъюнктивным членом коиъюнкци ю А,Л...ЛА„, в:которой А; есть Р; или ) Рь Формула Р(Рь ..., Р») имеет дизъюнктивную совершенную нормальную форму, если она имеет вид дизъюнкции 6,~/..Л/О, где.

каждое 6~ является совершенным конъюнктивным членом переменных Р„..., Р„. Имеет место Теорема. Любая не тождественно ложная формула логики высказываний равносильна формуле в совершенной дизъюнкгивной нормальной форме. С Для доказательства следует, например, рассмотреть булеву функцию, соответствующую данной формуле. Затем булеву функцию привести к совершенной дизъюнктивной нормальной форме согласно п.

9 $ б и написать формулу по полученному представлению. П. й в. исчислвнив выскдзывднии 1. На примере логики высказываний познакомимся с приемами строгой формализации математических теорий. При формализации математической теории полностью отвлекаются от ее содержания. Теоремы воспринимаются просто как формулы, которые могут быть выведены по определенным правилам. Поэтому формальные теории иначе называют исчислениями. О знаках и формулах исчисления приходится, однако, рассуждать содержательно: рядом с формальной теорией возникает «мегатеорил», которая тоже пользуется некоторыыи обозначениями. Эти обозначения метатеории следует строго отличать от знаков и формул, относящихся к собственно формальной теории.

Формализация логики высказываний, превращение ее в «исчисление высказываний» сама по себе не очень интересна, так,как после сведения логики высказываний к вычислениям с истинностными значениями мы и так находимся в сфере рассуждений о конечных объектах весьма простой природы. Однако с ней полезно познакомиться, как с первым важным примером формальной аксиоматической теории. Существует, много вариантов формализации логики высказываний.

Мы опишем один из них; назовем его «теория 1.». Формализация всякой содержательной теории начинается с выбора символов формальной теории; языка теории. Основные символы теории Е суть: 1) пропозициональные буквы Р„..., Р„, ..., 2) логические связки Л, ~/, ~, 3) скобки (,) Как уже было ск~азаио, кроме знаков самой теории Ь, мы будем, пользоваться символами, относящимися к мета- теории.

Для обозначения произвольной пропозвциональной буквы мы будем употреблять знаки Р, Я, )«, Рь Яь .... Даль- 45 нейшие соглашения и обозначения метатеории будут появ- ' ляться по мере необходимости. После того как выбраны основные символы теории, вы- деляют некоторые их комбинации которые называют фор- мулами. Формулы определяются индуктнвно с помощью следующих ниже двух пунктов. Первый,из этих пунктов яв- ляется базисом индукции. В 'нем непосредственно сообщает- ся, какие комбинации символов следует считать формула- ми.

Второй пункт представляет собой порождающее прави- ло. Предполагается, что все формулы Е построены из фор- мул пункта 1) с помощью последовательного применения правила 2): Итак: 1) Пропозициональные буквы суть формулы Е. 2) Если А и  — формулы, то формулами являются и следующие комбинации символов: (АЛВ), (А~/В), (А:зВ), ) А. Некоторые из формул теории называются аксиомами. В теории Е их десять: 1) (Р~-з (Рз~Р1) ), 2) ((Р~-э(Рз'~Рз)):э((Р~~Рз)~(Р1~Рз))), 3) ((Р1ЛРз)зР1) > 4) ( (РзЛРз):эРз), 5) (Р~-э (Рз:э (Р, ЛРз) ) ), 6) (Р1 з (Р1 У Рз) ), 7) (Рз-э (Р|~7Рз) ), 8) ( (Р1~Рз) ~ ( (ЫРз) з( (РИРз) -зРз) ) ) 9) ((Р1~Рз) ~((Р1» 1Рз) ~ 1 Р~) ).

10) ( ) ( Рз~Р1). Здесь Рь Р,, Рз — конкретные пропозициональные пере- менные, так,что 1) — 1О) есть список из десяти конкретных формул языка Е. Далее принимаются правила вывода, применяя которые можно из уже установленных теорем получать новые. В тео- рии Š— два таких правила вывода. Первое правило имеет вид (МР)л, А в в Это,правило, называемое тодиз ропепз, утверждает, что если формулы А и А=эВ установлены как теоремы, то формула В также является теоремой.

Второе правило имеет вид (В) А (Е,, ..; з Е 1 В„ ..., В 1 ' Здесь А, Вь, В суть формулы, Яь ..., Я вЂ” попарно различные пропозициональные буквы. Через А(Яь ..., Я 1~ 46 В„..., В„) мы обозначим результат одновременного замещения всех вхождений букв Яь ..., Я в А на формулы В„..., В соответственно. Следует заметить, что это провала подстановки (5) можно применять и к пропозициональиым буквам Яь которые вовсе,не входят в А. В этом случае соответствующее В; никуда не подставляется и просто ие играет никакой роли.

' 2. Перейдем теперь к описанию того, что есть теорема, или, иначе, выводимая формула теории Е. Выводом назовем любую конечную последовательность ,формул Аь Аг,, Ая, такую, что каждая формула этой последовательности есть либо аксиома, либо совпадает с какой-либо предыдущей, либо получается из каких-то предыдущих с помощью одного из правил вывода. Скажем, что вывод Аь ..., А, является выводом своей последней формулы А„и формулу А, зазовем выводимой, или, что то же самое, теоремой теории. Будем записывать это в виде: Е 1- А или просто 1- А.

В дальнейшем мы будем употреблять сокращенный вывод, когда в качестве А; могут стоять теоремы теории Е, полученные раньше, имея в виду, что мы всегда,можем дополнить вывод, вставляя недостающие его отрезки. Рассмотрим для примера вывод в теории Е теоремы (А:зА). Возьмем в качестве первой формулы А| вывода аксиому 2). Применим к ней правило подстановки в виде (Р» Рм РДА, (А:зА), А). Получим (а) т- ((Аэ((А:зА)~А))~((А=э(А:зА))~(А~А))). Из аксиомы 1) подстановкой (Рь РДА,(А~А)) получаем (б) 1- (А=э((А=зА) ~А)). Применим правило (МР) к (а) и (б): (в) 1- ((А=э(А~А)) ~(А~А)). Из аксиомы 1) подстановкой (Рь РД~А, А) получаем г) 1- (А~(А~А)), Применяя (МР) к (в) и (г), окончательно получим д) ~- (А:зА), 3. Напомним, что теорию Е мы строили как формаль- ный аналог содержательного исчисления высказываний.

В соответствии с этим нам хотелось бы, чтобы все теоремы теории Ь при содержательном толковании давали «истин ные» утверждения логики выаказываний, т. е. тавтологи Это действительно так. Покажем сначала, что всякая выво димая формула теории Т. при нашей интерпретации ес тавтология. Для этого надо проверить, что аксиом 1), 2) ... 10) — тавтологии; такая проверка проводится эл ментарно -построением таблиц истийности. Далее, всяка выводимая формула А является конечной формулой неко торого вывода Аь „., А„(=А). Вспомнив определение вывода, убеждаемся, что достаточн проверить, что правила вывода (МР) и (5), примененны к тавтологиям, снова дают тавтологии.

Такая проверк также тривиальна. Таким образом, всякая выводимая форр мула — тавтология. Замечательно, что имеет место и обратное утверждениее всякая тавтология выводится в теории. В. Мы не буде здесь останавливаться на доказательстве этого утвержде ния.

В следующей нашей книге будет доказана гораздо бо лее глубокая теорема о полноте исчисления предикатов. Ме год доказательства этой теоремы непосредственно ~приложи и к теории 1., которая являешься частью исчисления преди катон. Из изложенных результатов вытекает, что формальна теория Т. непротиворечиво в следующем смысле: не найдетт ся формулы такой, что и она сама и ее отрицание выводи мы. В самом деле, если А выводима, то она является тав тологией, то же верно для ) А. С другой стороны, если од на из формул А или ) А — тавтология, то вторая необхо димо является противоречием, что и доказывает наше ут верждение.

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

нулей и единиц, такой, что на этом наборе Р нмее значение нуль. Для каждого е, выберем формулу В; следую щим образом: если а;=1, то В~ есть С~/ ) С, если же е,,=О то В~ есть СЛ ) С, Здесь С вЂ” некоторая фикоировапна формула Формула Р(Вь, В„) принимает значение О уж при любых значениях переменных, и, значит, формул ~( Р(Вь ..., В«) есть тавтология и, следовательно ~- )Р(Вь ..., Ва).