IX. Иные разрешающие процедуры

Глава IX. Иные разрешающие процедуры.

1. Дизъюнктивно и конъюнктивно нормальные формы

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

Прежде, чем перейти к нормальным формам логики высказываний, необходимо оговориться: в логике, в следствие эквивалентных преобразований, существует много разных языков, которые не используют всего массива логических знаков. Иными словами, есть языки, которые используют лишь конъюнкцию и импликацию, игнорируя дизъюнкцию; есть языки, которые используют импликацию и дизъюнкцию, игнорируя знаки конъюнкции. Есть языки, которые не используют знак импликации и оперируют только конъюнкцией и дизъюнкцией.

Здесь, вероятно, нужны примеры.

Известные логики и математики Д. Гильберт и В. Аккерман предпочитают систему, в которой не существует знака дизъюнкции. Для них формула «A˅B˄C⊃D» будет выглядеть так: «AB&C→D». Для большинства современных логиков та же самая формула «A˅B˄C⊃D» может быть написана как «A˅BC→D». Нам же нужно переписать эту формулу не используя знака импликации.

Формула должна представлять собой последовательность элементарных конъюнкций, соединённых знаками дизъюнкции (нормальная дизъюнктивная форма), либо последовательность элементарных дизъюнкций, соединённых знаками конъюнкции (нормальная конъюнктивная форма).

Иными словами, нормальная дизъюнктивная форма представляет собой последовательность вида «(a˄b)˅(c˄d)˅(e˄f)…», а нормальная конъюнктивная форма – последовательность вида «(a˅b)˄(c˅d)˄(e˅f)…»

Когда нормальная форма формулы будет построена, можно будет легко определить – является ли она тождественно-ложной или тождественно-истинной.

Если формула принимает значение конъюнктивно нормальной формы, где все ее дизъюнкции содержат переменную и, одновременное, ее отрицание, значит формула – тождественно-истинная. Например: «(a˅¬a)˄(b˅¬b)˄(c˅¬c)…» Если же дизъюнктивно нормальная форму формулы содержит противоречие в каждой конъюнкции, то формула – тождественно-ложная. Например: «(a˄¬a)˅(b˄¬b)˅(c˄¬c)…» Соответственно, если оба этих условия не выполняются, то формула, скорее всего, выполнима или опровержима.

Для начала необходимо объяснить алгоритм приведения формулы в нормальные формы.

1. Путем применения логических эквивалентностей мы добиваемся, чтобы формула содержала лишь знаки конъюнкции, дизъюнкции и отрицания. Для этого мы используем эквивалентности –

a⊃b↔¬a˅b (или, что тоже самое «a⊃b↔¬(a˄¬b)») – для удаления импликации;

a≡b↔(¬a˅b)˄(a˅¬b) (или «a≡b↔(a∧b)∨(¬a˄¬b)») – для удаления тождества;

a˅b↔¬((a∨¬b)∧(¬a∨b)) – для удаления строгой дизъюнкции.

2. Все отрицания, стоящие перед скобками, преобразуем в отрицания, стоящие непосредственно перед переменными. Для этого применяем законы де Моргана:

¬(a˅b)↔¬a˄¬b

¬(a˄b)↔¬a˅¬b

3. 3. Устраняем все двойные отрицания.
4. Раскрываем скобки, используя законы дистрибутивности:

a˄(b˅c)↔(a˄b)˅(а˄c) — дистрибутивность конъюнкции относительно дизъюнкции;

a˅(b˄c)↔(a˅b)˄(а˅c) — дистрибутивность дизъюнкции относительно конъюнкции;

5. По необходимости, сокращаем формулу по законам –

a˄(a˅b)↔a – первый закон поглощения;

a˅(a˄b)↔a – второй закон поглощения;

a˄(b˅¬b)↔a – закон исключения истинного члена из конъюнкции;

a˅(b˄¬b)↔a – закон исключения ложного члена из дизъюнкции.

Для удобства, во время всего процесса применяем законы ассоциативности и коммутативности:

(a˄b)˄c↔a˄(b˄c) — ассоциативность конъюнкции;

(a˅b)˅c↔a˅(b˅c) – ассоциативность дизъюнкции;

(a˄b)↔(b˄a) – коммутативность конъюнкции;

(a˅b)↔(b˅а) – коммутативность дизъюнкции.

Для того чтобы понять данный алгоритм (который требует высокой сосредоточенности и творческого мастерства студента) попробуем решить какую-нибудь простую задачу. К приме, попробуем построить нормальные формы формулы контрапозиции: (p⊃q)⊃(¬q⊃¬p).

1. Преобразуем импликации. Сначала главную импликацию выражения

(p⊃q)⊃(¬q⊃¬p)→¬(p⊃q)˅(¬q⊃¬p)

Затем преобразовываем остальные импликации:

¬(p⊃q)˅(¬q⊃¬p)→(p˄¬q)˅(¬¬q˅¬p)

Пояснение: импликацию «¬(p⊃q)» мы преобразили, по правилу отрицания импликации «¬(p⊃q)→(p˄¬q)», а импликацию «(¬q⊃¬p)» по эквивалентности «a⊃b↔¬a˅b».

2. Второе действие алгоритма мы опускаем, поскольку у нас нет отрицаний, стоящих перед скобками.
3. Устраняем двойные отрицания:

(p˄¬q)˅(¬¬q˅¬p)→(p˄¬q)˅(q˅¬p)

4. Раскрываем скобки, используя законы дистрибутивности (для удобства меняем местами скобки по закону ассоциативности):

(p˄¬q)˅(q˅¬p)→(q˅¬p)˅(p˄¬q) —  по закону ассоциативности;

(q˅¬p)˅(p˄¬q)→(q˅¬p˅p)˄(q˅¬p˅¬q) – по закону дистрибутивности дизъюнкции относительно конъюнкции.

Итак, нормальная конъюнктивная форма построена – «(q˅¬p˅p)˄(q˅¬p˅¬q)». Поскольку в каждой её дизъюнкции присутствует переменная и её отрицание, делаем вывод, что изначальная формула тождественно-истинная.

Попробуем построить нормальную форму тождественно-ложной формулы. Например, «¬(((a⊃b)˄a)⊃b)»

Нормальная дизъюнктивная форма «(a˄¬b˄¬a)˅(a˄¬b˄b)» соответствует всем признакам тождественно-ложной формулы, поскольку в каждом дизъюнкте присутствует противоречие.

Для закрепления навыков, попробуем решить какую-нибудь выполнимую формулу.

Предположим, дано умозаключение: «Чтобы приготовить вкусный борщ, в него обязательно надо добавить жареный лук и чеснок. А это означает, что для его приготовления нужна какая-нибудь готовая заправка».

Строим нормальную дизъюнктивную форму:

По полученной дизъюнктивной форме «(a˄¬b˄¬c)˅(¬a˅d)» видно, что анализируемое умозаключение не является тождественно-ложным.

Строим нормальную конъюнктивную форму:

По полученной конъюнктивной форме «(¬a˅d˅a)˄(¬a˅d˅¬b)˄(¬a˅d˅¬c)» видно, что анализируемое умозаключение не является тождественно-истинным. Следовательно, умозаключение формы «Чтобы приготовить вкусный борщ, в него обязательно надо добавить жареный лук и чеснок. А это означает, что для его приготовления нужна какая-нибудь готовая заправка» может быть истинным (или ложным) при определенных условиях.

Совет

2. Аналитические таблицы

Если приведение формулы в нормальную форму является разрешающей процедурой только в логике высказываний, то очень популярный сегодня метод проверки формул путем построения аналитических таблиц является полуразрешающей процедурой также и для логики предикатов первого порядка.

При построении аналитических таблиц используется несколько иной язык логики (по сравнению с тем, с которым мы с вами до сих пор сталкивались). Формула «a» обозначается как ложная выражением «Fa» (от английского «false» — ложный) и, соответственно в качестве истинной она обозначается как «Ta» (от английского «truth» — истинный).

Поскольку каждая формула в аналитических таблицах позиционируется как некое множество, она берется в фигурные скобки – «{Fa}». Методом построения аналитических таблиц всего служит метод от противного, т.е. изначально предполагается, что искомая формула ложна — «{Fa}». Затем, применяя к формуле определенные правила, мы пытаемся (как в случае с семантическими таблицами) «замкнуть» таблицу. Если нам это удается – искомая формула считается тождественно-истинной.

Правила, применяемые для аналитических таблиц, делятся на две группы – правила «истинности» и правила «ложности»:

Также существуют правила для кванторов:

Правила мы описали, теперь перейдем к практическому решению задач.

Предположим, дана формула «(a⊃b)⊃(¬a˅b)» — известная вам эквивалентность. Предполагаем, что она ложная, т.е «F»:

1. {{F((a⊃b)⊃(¬a˅b))}}

Вывод из ложной импликации мы производим, соответственно, по правило «F⊃»: {F(a⊃b)}⊨{Ta, Fb}:

2. {{T(a⊃b), F(¬a˅b)}} – из 1 по F⊃
3. {{T(a⊃b), F¬a, Fb}} – из 2 по F˅
4. {{T(a⊃b), Ta, Fb}} – из 3 по F¬
5. {{Fa, Ta, Fb}, +{Tb, Ta, Fb}=} – из 4 по F⊃

Пояснение действия 5: По правилу F⊃ мы должны разбить множество {T(a⊃b), Ta, Fb} надвое. Из «T(a⊃b)» по правилу F⊃ получаем {Fa} и {Tb}. Но, поскольку в действии 4 у нас остаётся множество {Ta, Fb}, мы его помещаем, и в правое, и в левое множества последовательности формул. Иными словами {Fa}+{Ta, Fb}={Fa, Ta, Fb} и {Tb}+{Ta, Fb}={Tb, Ta, Fb}. Теперь мы видим противоречия в обоих множествах. В левом {Fa} и {Ta}, а в правом – {Tb} и {Fb}. Таким образом, исходная формула тождественно-истинная.

Доказываем закон дистрибутивности конъюнкции относительно дизъюнкции – «a˄(b˅c)⊃(a˄b)˅(а˄c)»:

Аналитическая таблица замкнулась – в каждом конечном множестве мы имеем противоречие (для наглядности мы подчеркнули их).

Поясним переход от третьего действия к четвертому. Мы его совершили по правилу

Иными словами, нам было необходимо из одного множества перейти к двум. Соответственно, из «T(b˅c)» мы получили «Tb» и «Tc», которые необходимо распределить между двумя множествами: «Tb» слева и «Tc» справа:

Более сложной задачей является построение аналитической таблицы для формулы логики предикатов, поскольку здесь добавляются правила для кванторов. К правилам кванторов необходимо добавить некоторые пояснения.

Для T∃ и F∀, «β» — новый параметр, который не встречался в предшествующих конфигурациях.

Для F∃ и T∀, «β» — любой параметр из уже имеющихся, либо новый параметр, если параметров ещё нет.

Например, «¬∀x(S(x))⊃∃x¬(S(x))».

Таблица замкнулась.

Еще пример: «∃x∀y(S(x, y))⊃∀y∃x(S(x, y))».

3. Аксиоматические исчисления

В рамках аксиоматической системы используются схемы аксиом (или аксиомы), причем их количество может быть сведено к минимуму:

1. a⊃(b⊃a) – схема утверждения консеквента (и аксиомы, сформулированные на её основе);
2. (a⊃(b⊃c))⊃((a⊃b)⊃(a⊃c)) – схема самодистрибутивности импликации (и аксиомы, сформулированные на её основе);
3. (¬b⊃¬a)⊃(a⊃b) – схема обратной контрапозиции.

Добавляется лишь одно правило – Modus Ponens

Для работы с языком логики предикатов первого порядка, формулируются схемы аксиом для кванторов:

1. ∀xP(x) ⊧P(t) – схема удаления ∀ (У∀)
2. P(t) ⊧ƎхP(x) – схема введения Ǝ (ВƎ)
3. ∀x(А⊃P(x))⊧(А⊃∀xP(х)) – схема введения ∀ в консеквент (В∀вК).
4. ∀x(P(x)⊃А)⊧(ƎхP(х)⊃А) – схема введения Ǝ в антецедент (ВƎвА).

А также правило «P(t)⊧∀xP(x)» — правило обобщения (В∀)

Докажем аксиому «¬(a˄a)→¬a».

Для начала, преобразуем формулу путем логических эквивалентностей – «(a⊃¬a)⊃¬a»

1. a⊃(a⊃¬a)⊃¬a – аксиома, построенная на основе схемы утверждения консеквента.
2. 2. (a⊃(a⊃¬a)⊃¬a)⊃(((a⊃¬a)⊃(a⊃a))⊃((a⊃¬a)⊃¬a))) — аксиома, построенная на основе схемы самодистрибутивности материальной импликации.
3. ((a⊃¬a)⊃(a⊃a))⊃((a⊃¬a)⊃¬a)) – из 1 и 2 по Modus Ponens.
4. (a⊃¬a)⊃(a⊃a) — аксиома, построенная на основе схемы утверждения консеквента.
5. (a⊃¬a)⊃¬a – из 3 и 4 по Modus Ponens. ∎

С помощью системы аксиоматического вывода можно доказать любую тождественно-истинную формулу. И (если мы говорим о логике высказываний) в выводе неизменно будет сохраняться указанные пять действий (т.е. выше представлена «схема» доказательства). К безусловным преимуществам аксиоматического вывода можно отнести минимальное количество правил и схем аксиом. К неудобствам – поиск аксиом из правил консеквента и самодистрибутивности импликации, а также крайне длинные формулы, изобилующие множеством скобок. В приведенном примере мы доказывали формулу с одной пропозициональной переменной. Если бы переменных в формуле было бы четыре или пять, вывод мог бы растянуться на несколько страниц. Такое, прямо скажем, не самое изящное доказательство является «расплатой» за минимальное количество схем вывода.

Добавив к перечисленным схемам вывода всего одну схему, схему исключения конъюнкции– «ab⊃a», где написание «ab» есть сокращение от «a˄b», мы сможем доказывать формулы значительно компактнее.

Доказательство формулы «a⊃(b⊃c)⊨ab⊃c»:

1. + a⊃(b⊃c) – гипотеза.
2. (ab⊃(b⊃c))⊃((ab⊃b)⊃(ab⊃c)) – схема самодистрибутивности импликации;
3. (ab⊃(a⊃(b⊃c)))⊃((ab⊃a)⊃(ab⊃(b⊃c))) – схема на основе самодистрибутивности импликации;
4. (a⊃(b⊃c))⊃(ab⊃(a⊃(b⊃c))) – схема на основе утверждения консеквента;
5. ab⊃(a⊃(b⊃c)) – из 4 и 1 по Modus Ponens;
6. (ab⊃a)⊃(ab⊃(b⊃c)) – из 5 и 3 по Modus Ponens;
7. ab⊃a – схема исключения конъюнкции;
8. ab⊃(b⊃c) – из 6 и 7 по Modus Ponens;
9. (ab⊃b)⊃(ab⊃c) – из 2 и 8 по Modus Ponens;
10. ab⊃b — схема исключения конъюнкции;
11. ab⊃c – из 9 и 10 по Modus Ponens. ∎

Для облегчения работы в аксиоматической системе с языком логики предикатов можно взять из системы натурального вывода все правила первого и второго рода и интерпретировать их в качестве схем аксиом; однако вместо правил для кванторов рекомендуем использовать схемы аксиом для них:

1. ∀xP(x) ⊧P(t) – (У∀);
2. P(t) ⊧ƎхP(x) – (ВƎ);
3. ∀x(А⊃P(x))⊧(А⊃∀xP(х)) – (В∀вК);
4. ∀x(P(x)⊃А)⊧(ƎхP(х)⊃А) – (ВƎвА);

а также правило «P(t)⊧∀xP(x)» — (В∀).

Дано: «∀x(S(x)⊃P(x))⊃∃x(S(x)∧P(x))»

Решение:

1. + ∀x(S(x)⊃P(x)) – гипотеза;
2. + ∀xS(x) – гипотеза;
3. S(x)⊃P(x) – из 1 по схеме У∀;
4. S(x) – из 2 по схеме У∀;
5. P(x) – из 3 и 4 по схеме У⊃;
6. S(x)˄P(x) — из 4 и 5 по схеме В˄;
7. ∃x(S(x)∧P(x)) – из 6 по схеме ВƎ. ∎

Студент должен понимать, что аксиоматическая система может иметь в своем арсенале различные схемы аксиом. Только что решенную задачу можно было бы решить в два действия, имея в виду, что среди заявленных систем аксиом имелась бы «∀x(S(β)⊃P(γ))⊃∃x(S(β)∧P(γ))».

Дано: «∀x(S(x)⊃P(x))⊃∃x(S(x)∧P(x))»

Решение:

1. + ∀x(S(x)⊃P(x)) – гипотеза;
2. ∃x(S(x)∧P(x)) из 1 по схеме аксиом ∀x(S(β)⊃P(γ))⊃∃x(S(β)∧P(γ)). ∎

Попробуем решить задачу.

Дано высказывание: «Если неправда, что некоторые студенты наркоманы, следовательно, верно, что все студенты не наркоманы».

Переводим высказывание в символическую форму:

¬(ƎхP(х))→∀x¬P(x)

1. + ¬ ƎхP(х)
2. + P(x)
3. ƎхP(х) — из 2 по ВƎ
4. ¬ ƎхP(х)˄ ƎхP(х) из 1 и 3 по В˄
5. (¬ ƎхP(х)˄ ƎхP(х))→ P(x) из 4 и 2 по В→
6. ¬ P(х) – из 5 по ДОП
7. ∀x¬P(x) – из 6 по В∀вК
8. ¬ (ƎхP(х))→∀x¬P(x) – из 1 и 7 по В→.∎

Можно эту же задачу решить, используя доказательство от противного:

1. +¬(¬ ƎхP(х)→∀x¬P(x))
2. ¬ ƎхP(х)˄¬∀x¬P(x) из 1 по О→
3. ¬ ƎхP(х) – из 2 по У˄
4. ¬∀x¬P(x) – из 2 по У˄
5. ¬Ǝx¬P(x) из 4 по ВƎвА
6. ¬ ƎхP(х)˄ ¬Ǝx¬P(x) из 3 и 5 по В˄
7. (¬ ƎхP(х)˄ ¬Ǝx¬P(x))→ ¬(¬ ƎхP(х)→∀x¬P(x)) из 6 и 1 по В→
8. ¬ ƎхP(х)→∀x¬P(x)) из 7 по ДОП. ∎

В этом разделе мы привели несколько примеров систем аксиом, для решения некоторых логических формул. Студент должен понимать, что набор аксиом может быть абсолютно любым: главное, чтобы они помогали решить конкретную поставленную задачу. Предлагаем студентам самим поэкспериментировать в этом направлении. Главное, чтобы все аксиомы были тщательно проверенными, т.е. гарантированно являлись тождественно-истинными формулами.