Дискретно-непрерывная математика (стр. 7 )

Имеют место следующие факты, связанные с СДНФ:

a) Каждую не тождественно ложную формулу логики высказываний можно представить в виде эквивалентной ей СДНФ. Отсюда следует функциональная полнота множества связок

b) Это представление в виде СДНФ единственно;

c) Если СДНФ формулы F содержит в точности п пропозициональных переменных, то формула F является тавтологией т. т.т., когда ее СДНФ состоит из 2п дизъюнктивных членов. Отсюда следует разрешимость классической логики высказываний.

1.3.1. Полиномы Жегалкина

Представляет интерес еще один класс нормальных форм, названный полиномами (многочленами) Жегалкина [Жегалкин 1927], которые были предложены в качестве удобного средства для представления булевых функций.

Рассмотрим на множестве классических истинностных значений {0, 1} арифметические операции. Арифметическое умножение • совпадает с конъюнкцией , но арифметическое сложение + выводит за пределы множества {0, 1}. Однако можно взять сложение по модулю 2 (равное остатку от деления на 2). В результате получаем булеву функцию, которую обозначим посредством :

Заметим, что р q можно выразить в видеВ свою

очередь,

Применяя эти две формулы, любую формулу классической логики высказываний можно представить через связки, и константу 1, причем рп есть р при п ≥ 1 и(теорема

Жегалкина). . -

Например, полином Жегалкина для формулы

К СДНФ и полиному Жегалкина мы вернемся при изучении функциональных свойств и-значных логик (см. гл. 7).

Изучение свойств логических связок, их систематизация и выделение основных равносильностей приводит к формированию понятия алгебры Буля (см. раздел 4.4.1). Все эти и другие вопросы, включая свойства булевых функций, изучает алгебра логики.

1.3.2. Штрих Шеффера

В классической логике существуют две истинностно-функциональные связки, каждая из которых образует функционально полную систему. Первая из них называется штрих (функция) Шеффера и обозначается посредством | (1913 г.): высказывание р|д истинно т. т.т., когда неверно, что р и q оба истинны, т. е. (антиконъюнкция). Тогда Другая связка называется стрелка Пирса и обозначается посредством ↑: высказывание p↑q истинно т. т.т., когда неистинно р и неистинно q, т. е. (антидизъюнкция). Тогда

Таким образом, для того чтобы показать, что какая-то связка

является аналогом штриха Шеффера, надо (i) определить ее

посредством исходных связок, а затем (ii) посредством ее

определить сами исходные связки. Некоторые аналоги штриха

Шеффера и стрелки Пирса нам понадобятся в последующем.

1.4. Логическое следование. Аксиоматизация. Адекватность

Наряду с понятием тавтологии фундаментальным для логики является понятие логического следования, которое является некоторым отношением, заданным на множестве формул. Говорят «В логически следует из А или является логическим следствием из А», и пишут если в совместной таблице истинности для А и В

формула В имеет значение 1 во всех тех строках, где А имеет значение 1. Отсюда следует, что т. т.т., когда есть

тавтология. Если формула А является тавтологией, то иногда пишут Приведенное определение логического следования без

труда может быть расширено на некоторую систему формул Г, и тогда пишут Дадим стандартное (классическое)

определение логического следования, которое восходит к работе А. Тарского 1936 г.: Формула В логически следует из множества формул Г т. т.т., когда при любом приписывании значений переменным в составе Г и В, при котором все формулы из Г принимают значение «истина», формула В также принимает значение «истина». Приведем следующий пример логического следования из посылок: Отметим также, что в силу приведенного выше табличного определения импликации получаем, что тождественно истинная формула А логически следует из любой системы формул, а из противоречия следует любая формула A.

Если определено понятие тавтологии и определено семанти­ческое понятие логического следования (как это сделано выше), то говорят, что дано семантическое представление логики высказы­ваний, а сама логика высказываний зачастую отождествляется с множеством тавтологий или с самим отношением логического следования. Однако при этом возникает следующая серьезная проблема: как обозреть все тавтологии, которых бесконечное мно­жество? Для решения этой проблемы переходят к синтаксическому представлению логики высказываний,

В рамках синтаксического подхода формальный (символиче­ский) язык логики высказываний и понятие формулы остаются прежними, а из всего множества тавтологий выбирается некоторое их конечное подмножество, элементы которого называются аксиомами. Наиболее известным является следующее множество аксиом [Клини 1957]:

Таким образом, мы задали аксиоматическое определение логических связокв отличие от табличного при семантическом описании логики высказываний. Как обычно, р ≡q означает

Переход от формулы или множества формул к формуле осуществляется с помощью следующих правил:

R1. Из А иследует В (modus ponens). Это правило

Иногда обозначается посредством МР и записывается в виде

R2. Изследует (подстановка).

Данное правило подстановки легко обобщается на случай одновременной подстановки формул В1, В2, ..., Вп вместо различных переменных р1,р2, ..., pп, входящих в формулу A.

Заметим, что каждая аксиоматическая система, которая; использует правило подстановки, может быть представлена в виде схем аксиом, где вместо пропозициональных переменных используются символы для произвольных высказываний (метапеременные). В этом случае каждая схема аксиом представляет бесконечное множество аксиом (см. более подробно в разделе 4.2) и тогда правило подстановки оказывается излишним. Именно в таком виде дается в [Клини 1957] приведенная выше аксиоматизация, где вместо пропозициональных переменных р, q, r используются метапеременные А, В, С. Однако зачастую более удобно пользоваться аксиоматизацией с правилом подстановки, особенно при анализе доказательств.

Так заданную логику высказываний обозначим посредством С2 и назовем классической логикой высказываний,

Логика, заданная посредством некоторого множества аксиом и некоторого множества правил вывода, называется гилъбертовским исчислением L. Заметим, что существуют также другие типы логических исчислений, эквивалентные данному. Например, генценовские (секвенциальные) исчисления, семантические таблицы Бета, исчисления натурального вывода и др. (см. [Смирнов 1972]). Но для наших целей намного более удобными являются именно гильбертовские исчисления в силу простоты их задания, прозрачности соотношения между семантикой и синтаксисом и, главное, они являются очень удобным инструментом при рассмотрении взаимоотношений одних логик с другими.

Теперь перейдем к описанию того, что есть доказательство и что есть теорема в исчислении L.

Доказательством в L называется такая конечная последовательность формул А1, А2, ..., Ап, что каждая формула этой последовательности есть либо аксиома, либо получена из некоторых предыдущих формул последовательности по одному из правил вывода. Формула А называется теоремой L, если существует доказательство в L, в котором последней формулой является А, Записьслужит сокращением утверждения «А есть теорема». Если формула А доказуема из некоторого множества Г исходных формул (посылок), то запись принимает вид с соответствующей модификацией определения доказательства.