Перейти к содержимому
Topos Uranos
Русский

Законы де Моргана и дистрибутивности

Краткое содержание

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

Цели обучения

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

Предыдущие уроки этого раздела построили, один на основе другого, инструменты вывода: систему аксиом и modus ponens, четыре основных приёма и замену двойного отрицания, симметрии связок и приёмы классической логики. Этот урок не добавляет ни одного нового правила; он заставляет их работать вместе. Если это так, его интерес состоит не столько в формулировках, которые, возможно, известны из других курсов, сколько в способе их получения: каждая строка должна обосновываться аксиомой, посылкой, определением, одним из двух исходных правил или уже доказанным результатом, и ни одна не может опираться на то, что «кажется очевидным».

Что используется и как сцепляется

Из урока о формальных дедуктивных системах берутся аксиомы A1, A2 и A3 Лукасевича, modus ponens (MP), также с посылками, рефлексивность (Рефл: если φ∈Γ\varphi \in \Gamma, то Γ⊢φ\Gamma \vdash \varphi), монотонность (Мон), сечение (Сеч: если Γ⊢φi\Gamma \vdash \varphi_i для каждого ii и Γ∪{φ1,…,φn}⊢ψ\Gamma \cup \{\varphi_1, \ldots, \varphi_n\} \vdash \psi, то Γ⊢ψ\Gamma \vdash \psi), теорема о дедукции (ТД) и доказуемая эквивалентность (φ⊣⊢ψ\varphi \dashv\vdash \psi, если {φ}⊢ψ\{\varphi\} \vdash \psi и {ψ}⊢φ\{\psi\} \vdash \varphi) с её свойствами: она рефлексивна, симметрична и транзитивна, и если φ⊣⊢ψ\varphi \dashv\vdash \psi, то Γ⊢φ\Gamma \vdash \varphi тогда и только тогда, когда Γ⊢ψ\Gamma \vdash \psi. Из урока о четырёх приёмах вывода берутся двойное отрицание (ДО: φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi), контрапозиция (Контр), в частности (φ→ψ)⊣⊢(¬ψ→¬φ)(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi), и второе исходное правило системы курса, замена двойного отрицания (ЗДО), при которой теорема о дедукции остаётся верной: если χ′\chi' получается из χ\chi заменой одного вхождения подформулы θ\theta на ¬¬θ\neg\neg\theta или одного вхождения ¬¬θ\neg\neg\theta на θ\theta, то из χ\chi выводится χ′\chi'; строка, полученная так из строки ii, обосновывается как ЗДО(i)(i). Среди её непосредственных следствий: (φ↓ψ)⊣⊢(¬¬φ↓ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi), (φ↓ψ)⊣⊢(φ↓¬¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi) и, вообще, χ⊣⊢χ′\chi \dashv\vdash \chi', когда χ′\chi' получается из χ\chi по ЗДО; отсюда следует, что ЗДО(i)(i) применяется также к строке вида χ⊣⊢φ\chi \dashv\vdash \varphi, чтобы изменить двойное отрицание в φ\varphi. Из урока о симметриях связок берутся замена эквивалентных (Зам) и симметрии (Сим), среди них (φ∨ψ)⊣⊢(ψ∨φ)(\varphi \vee \psi) \dashv\vdash (\psi \vee \varphi) и (φ∧ψ)⊣⊢(ψ∧φ)(\varphi \wedge \psi) \dashv\vdash (\psi \wedge \varphi).

Из урока о приёмах классической логики берутся, все с множеством Γ\Gamma посылок, следующие правила. Введение дизъюнкции (∨\veeв): если Γ⊢φ\Gamma \vdash \varphi, то Γ⊢(φ∨ψ)\Gamma \vdash (\varphi \vee \psi) и Γ⊢(ψ∨φ)\Gamma \vdash (\psi \vee \varphi). Удаление дизъюнкции (∨\veeу, дизъюнктивный силлогизм): если Γ⊢(φ∨ψ)\Gamma \vdash (\varphi \vee \psi) и Γ⊢¬φ\Gamma \vdash \neg\varphi, то Γ⊢ψ\Gamma \vdash \psi. Введение конъюнкции (∧\wedgeв): если Γ⊢φ\Gamma \vdash \varphi и Γ⊢ψ\Gamma \vdash \psi, то Γ⊢(φ∧ψ)\Gamma \vdash (\varphi \wedge \psi). Удаление конъюнкции (∧\wedgeу): если Γ⊢(φ∧ψ)\Gamma \vdash (\varphi \wedge \psi), то Γ⊢φ\Gamma \vdash \varphi и Γ⊢ψ\Gamma \vdash \psi. Закон исключённого третьего (ИТ): ⊢(φ∨¬φ)\vdash (\varphi \vee \neg\varphi). И разбор случаев (Случ) в двух его формах: если Γ∪{φ}⊢χ\Gamma \cup \{\varphi\} \vdash \chi и Γ∪{¬φ}⊢χ\Gamma \cup \{\neg\varphi\} \vdash \chi, то Γ⊢χ\Gamma \vdash \chi; и если Γ∪{φ}⊢χ\Gamma \cup \{\varphi\} \vdash \chi, Γ∪{ψ}⊢χ\Gamma \cup \{\psi\} \vdash \chi и Γ⊢(φ∨ψ)\Gamma \vdash (\varphi \vee \psi), то Γ⊢χ\Gamma \vdash \chi. В выводах первая форма цитируется с двумя строками, Случ(i,j)(i, j), а вторая с тремя, Случ(i,j,k)(i, j, k), в порядке формулировки: два случая и, в конце, дизъюнкция. Тот урок напоминает также, что всякое уже доказанное правило верно внутри контекста Γ\Gamma, и так здесь применяются двойное отрицание и контрапозиция.

Имена цепочки и эквивалентные формулы

Напомним из урока о языке логики высказываний, что связки, отличные от ↓\downarrow, суть сокращения с официальным и единственным определением: ¬φ:=(φ↓φ)\neg\varphi := (\varphi \downarrow \varphi), (φ∨ψ):=¬(φ↓ψ)(\varphi \vee \psi) := \neg(\varphi \downarrow \psi), (φ∧ψ):=¬(¬φ∨¬ψ)(\varphi \wedge \psi) := \neg(\neg\varphi \vee \neg\psi), (φ→ψ):=(¬φ∨ψ)(\varphi \rightarrow \psi) := (\neg\varphi \vee \psi), (φ↔ψ):=((φ→ψ)∧(ψ→φ))(\varphi \leftrightarrow \psi) := ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)) и (φ⊻ψ):=¬(φ↔ψ)(\varphi \veebar \psi) := \neg(\varphi \leftrightarrow \psi). Определение ничего не утверждает о формулах: оно даёт второе имя цепочке, которая уже существовала. Отсюда следует, что если два выражения обозначают одну и ту же цепочку, одно можно поставить вместо другого в любом месте, также внутри большей формулы, потому что пишется одна и та же последовательность кружков и дисков. Так, ¬(φ∧ψ)\neg(\varphi \wedge \psi) и ¬¬(¬φ∨¬ψ)\neg\neg(\neg\varphi \vee \neg\psi) есть одна и та же цепочка: вторая получается, если внутри первой записать раскрытие конъюнкции. В выводах такая смена имени обосновывается как «Опр» с указанием связки, которая раскрывается или свёртывается.

Но доказуемая эквивалентность не есть тождество. То, что φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi, означает, что каждая из формул выводится из другой, а не что они суть одна и та же цепочка: ¬¬φ\neg\neg\varphi гораздо длиннее, чем φ\varphi. Поэтому знание того, что φ⊣⊢φ′\varphi \dashv\vdash \varphi', само по себе не позволяет писать φ′\varphi' вместо φ\varphi внутри большей формулы. Не позволяет оно и «отрицать обе стороны»: то, что из φ⊣⊢φ′\varphi \dashv\vdash \varphi' следует ¬φ⊣⊢¬φ′\neg\varphi \dashv\vdash \neg\varphi', есть теорема, замена эквивалентных, доказательство которой использует контрапозицию, а не очевидная операция. Есть единственный случай, когда система разрешает замену непосредственно, в любом месте формулы: замена θ\theta на ¬¬θ\neg\neg\theta или обратно, то есть правило ЗДО; и урок о дедуктивных системах показал с помощью разметки, что даже этот случай не выводится из аксиом и modus ponens, так что его пришлось постулировать. Эта осторожность не педантизм; именно она отличает доказательство от манипуляции символами, которая, будучи применена к другим связкам или в других системах, могла бы привести к ложным утверждениям.

Два результата точно фиксируют, что разрешено. Первый есть утверждение о свойствах доказуемой эквивалентности из урока о формальных дедуктивных системах: если Γ⊢φ\Gamma \vdash \varphi и φ⊣⊢φ′\varphi \dashv\vdash \varphi', то Γ⊢φ′\Gamma \vdash \varphi', так что доказуемую эквивалентность можно применять ко всей формуле строки; и доказуемая эквивалентность рефлексивна, симметрична и транзитивна, так что эквивалентности сцепляются (если χ⊣⊢φ\chi \dashv\vdash \varphi и φ⊣⊢φ′\varphi \dashv\vdash \varphi', то χ⊣⊢φ′\chi \dashv\vdash \varphi'), а два выражения, обозначающие одну и ту же цепочку, по рефлексивности доказуемо эквивалентны. Второй, следующая лемма, собирает, чтобы на неё было удобно ссылаться, распространение замены эквивалентных на дизъюнкцию и конъюнкцию; урок о симметриях доказывает эту замену для отрицания, импликации и стрелки Пирса и распространяет её на эти две связки в одной из своих решённых задач.

ЛеммаЗамена в дизъюнкции и в конъюнкции

Если φ⊣⊢φ′\varphi \dashv\vdash \varphi', то для всякой формулы ψ\psi имеют место (φ∨ψ)⊣⊢(φ′∨ψ)(\varphi \vee \psi) \dashv\vdash (\varphi' \vee \psi), (ψ∨φ)⊣⊢(ψ∨φ′)(\psi \vee \varphi) \dashv\vdash (\psi \vee \varphi'), (φ∧ψ)⊣⊢(φ′∧ψ)(\varphi \wedge \psi) \dashv\vdash (\varphi' \wedge \psi) и (ψ∧φ)⊣⊢(ψ∧φ′)(\psi \wedge \varphi) \dashv\vdash (\psi \wedge \varphi').

Доказательство

  1. (φ∨ψ)=¬(φ↓ψ)(\varphi \vee \psi) = \neg\resaltar{(\varphi \downarrow \psi)}

    Дизъюнкция есть по определению отрицание стрелки Пирса.

  2. (φ↓ψ)⊣⊢(φ′↓ψ)\dato{int}{(\varphi \downarrow \psi) \dashv\vdash (\varphi' \downarrow \psi)}

    Замена эквивалентных для стрелки Пирса даёт эквивалентность внутреннего слоя.

  3. (φ∨ψ)⊣⊢(φ′∨ψ)\dato{disy}{\resaltar{(\varphi \vee \psi)} \dashv\vdash \resaltar{(\varphi' \vee \psi)}}

    Замена эквивалентных для отрицания переносит её на внешний слой, ¬(φ↓ψ)⊣⊢¬(φ′↓ψ)\neg(\varphi \downarrow \psi) \dashv\vdash \neg(\varphi' \downarrow \psi), а это и есть дизъюнкция. Точно так же с (ψ↓φ)⊣⊢(ψ↓φ′)(\psi \downarrow \varphi) \dashv\vdash (\psi \downarrow \varphi') получается замена справа.

  4. (φ∧ψ)=¬(¬φ∨¬ψ),¬φ⊣⊢¬φ′(\varphi \wedge \psi) = \neg(\resaltar{\neg\varphi} \vee \neg\psi), \qquad \neg\varphi \dashv\vdash \neg\varphi'

    Конъюнкция есть отрицание дизъюнкции отрицаний. Замена для отрицания даёт сначала ¬φ⊣⊢¬φ′\neg\varphi \dashv\vdash \neg\varphi'.

  5. ¬(¬φ∨¬ψ)⊣⊢¬(¬φ′∨¬ψ),(φ∧ψ)⊣⊢(φ′∧ψ)\neg(\neg\varphi \vee \neg\psi) \dashv\vdash \neg(\neg\varphi' \vee \neg\psi), \qquad \resaltar{(\varphi \wedge \psi)} \dashv\vdash \resaltar{(\varphi' \wedge \psi)}

    Уже доказанная часть для дизъюнкции, применённая к ¬φ\neg\varphi и ¬φ′\neg\varphi', даёт (¬φ∨¬ψ)⊣⊢(¬φ′∨¬ψ)(\neg\varphi \vee \neg\psi) \dashv\vdash (\neg\varphi' \vee \neg\psi), и снова замена для отрицания переносит эквивалентность на конъюнкцию; справа рассуждают так же.

В дальнейшем «Зам» обозначает замену эквивалентных в любой её форме, также в формах этой леммы, и её можно применять несколько раз подряд, слой за слоем, чтобы добраться до подформулы на любой глубине. Когда строка получается из строки ii применением уже доказанной эквивалентности, ко всей формуле или, с Зам, к одной из её частей, она обосновывается именем этой эквивалентности и номером строки: ДО(i)(i), «Зам, ДМ(i)(i)». Смена имени, которая не применяет никакой эквивалентности, а переписывает ту же цепочку, обосновывается так же, как «Опр» с указанием связки, которая раскрывается или свёртывается: Опр ∧\wedge (i)(i). Утверждение из урока о формальных дедуктивных системах гарантирует, что такие строки обоснованы, утверждает ли строка ii, что Γ⊢φ\Gamma \vdash \varphi, или утверждает эквивалентность χ⊣⊢φ\chi \dashv\vdash \varphi, которая шаг за шагом продолжается.