В Степин - Новая философская энциклопедия. Том второй Е—M

416

ЛОГИКА ВЫСКАЗЫВАНИЙ щая процедура для тавтологий, получаем, что проблема выводимости произвольной формулы В из заданной системы посылок также разрешима. Если определено понятие тавтологии и определено семантическое понятие логического следования (как это сделано выше), то говорят, что дано семантическое представление логики высказываний, а сама логика высказываний зачастую отождествляется с множеством тавтологий или с самим отношением логического следования. Однако такое представление ставит серьезную проблему: как обозреть все тавтологии, которых бесконечное множество? Для решения этой проблемы нужно перейти к синтаксическому представлению логики высказываний. Формальный (символический) язык логики высказываний и понятие формулы остаются прежними. Но теперь из всего множества тавтологий выбирают некоторое их конечное (и, вообще говоря, определяемые неоднозначно) подмножество, элементы которого называются ахтамшм*. Напр.:1.рЗ (qDp).l(pD(qD r))D((pDq)D(pD г)), З.р 3 (pvq),4.q3(pvq),5.(p 3 г) 3 ((q 3 г) 3 ((pvq) 3 г)), 6.(рл <0 3 р,7.(рлЧ) 3 q,8.(p 3q)3((p3r)3(p3 (q/ur))), 9.(p3 -^q)3 (qD-()),10.pD H> 3 q),ll.pv-4>. Т. о., в отличие от табличного определение логических связок -ц л, V, з задается аксиоматически. Затем с помощью уже известных правил, но чисто формально осуществляется вывод — переход от высказывания или системы высказываний к высказыванию: из А и АзВ следует В (правило заключения); из А(р) следует А(В) (подстановка). Так, заданную логику высказываний обозначим посредством С2 и назовем классической. Каждая аксиоматическая система, которая использует правило подстановки, может быть переформулирована в виде системы аксиомных схем, где вместо пропозициональных переменных используются символы произвольных высказываний (т. н. метапеременные). В этом случае каждая аксиомная схема представляет бесконечное множество аксиом и тогда правило подстановки оказывается излишним. Логическое исчисление, заданное посредством некоторого множества аксиом и некоторого множества правил вывода, называется исчислением гильбертовского типа. Выводом в нем называется всякая последовательность А,,..., А^ формул такая, что для любого i формула А есть либо аксиома, либо непосредственное следствие каких-либо предыдущих формул по одному из правил вывода. Формула А называется теоремой, если существует вывод, в котором последней формулой является А; такой вывод называется выводом формулы А. Запись |— А служит сокращением утверждения «А есть теорема». Если формула А выводима из некоторого множества Г исходных формул, то тогда запись принимает вид Г|— А (подробнее см. ВШидльтчмшш). Исходя из синтаксического представления логики высказываний, последняя зачастую отождествляется с множеством теорем или, что более принято, с отношением выводимости. Итак, при семантическом подходе формулы понимаются содержательно (как функции на множестве из двух элементов И, Л), а при синтаксическом подходе формула—это определенный набор символов и различаются только теоремы и нетеоремы. Однако, несмотря на такое различие, оба подхода к построению логики высказываний по существу совпадают и, как говорят, являются адекватными. Это значит, что совпадают понятия логического следования и понятия вывода. Рассмотрим следующую примечательную теорему, которая иногда называется теоремой адекватности: для всех А, |— А тогда и только тогда, когда |= А. Доказательство водну сторону, аименно: для всехА, если |—А, то |= А носит название теоремы о корректности. Это минимальное условие, которое мы требуем от логического исчисления и которое состоит в том, что представленная нами семантика корректна для выбранной аксиоматизации. Для доказательства теоремы нужно проверить, во-первых, что все аксиомы ( 1 )—( 11 ) являются тавтологиями, что легко устанавливается непосредственной проверкой с помощью истинностных таблиц, и, во-вторых, что правила вывода выбраны т. о., что они сохраняют тавтологичность. Поэтому все формулы последовательности, образующей доказательство какой-либо теоремы исчисления С2, в том числе и сама доказуемая теорема, являются тавтологиями. Из этой теоремы следует важнейшее свойство нашего исчисления высказываний С2: в С2 формулы А и -А одновременно недоказуемы, т. е. исчисление высказываний С2 непротиворечиво. Ели бы это было не так, то (с использованием аксиомы (10) и двойным применением modus ponens) в С2 была бы доказуема любая формула В. В силу этого противоречивая логика высказываний никакой ценности не представляет. В ней истина и ложь неразличимы и поэтому любая теорема одновременно истинна и ложна. Имеет место и обратное утверждение о том, каждая тавтология доказуема, т. е для всех А, если |= А, то |— А. Доказательство этой теоремы не столь тривиально и носит название теоремы о полноте исчисления высказываний относительно предложенной семантики. По существу здесь утверждается, что логических средств, т. е. аксиом и правил вывода, исчисления высказываний С2 вполне достаточно для доказательства всех тавтологий. Т. о., поставленная цель достигнута; используя минимальные средства, можно обозреть все множество тавтологий. Имеется много различных аксиоматизаций С2, в том числе состоящих из одной аксиомы и содержащих только одну связку (штрих Шеффера). Понятно, что чем меньше аксиом, тем сложнее доказательства. И вообще, в гильбертовских исчислениях доказательство теорем и сам поиск вывода весьма громоздок. Поэтому используются другие формулировки исчисления, более или менее приближенные к естественным рассуждениям, такие, как m шшмшт. сояемрш, исчисление натурального вывода и др. Но соотношение между семантикой и синтаксисом здесь не столь прозрачно. Первая аксиоматизация классической логики С2 была гтред- принята F. Фреге(\Ъ79). Однако в терминах современного символического языка аксиоматизация С2 появилась в «Principia Mathematical А. Штяеаш и К Ртахлт (1910-13). В обеих работах вопрос о полноте просто не возникал. Их целью было показать, что вся логика, а в действительности вся математика может быть развита внуфи их системы. Первая публикация доказательства полноты принадлежит Э. Посту (1921), который исходил из системы Уайтхеда и Рассела. Еще ранее это было сделано П. Бернайсом. В обоих случаях использовались двузначные истинностные таблицы (приведенные выше) для доказательства теоремы адекватности. В этом случае говорят еще, что эти таблицы являются характеристическими для С2. Теперь можно перейти к характеризации того, что называется классической логикой высказываний: (а) С2 основана на принципе двузначности (бивалентности). В последнее время большое развитие получили так называемые «бивалентные