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

Симметрии связок

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

Этот урок доказывает, что порядок аргументов не меняет того, что выводится из стрелки Пирса, дизъюнкции, конъюнкции, эквиваленции и строгой дизъюнкции. При официальных сокращениях курса эти симметрии не очевидны: стрелка Пирса есть исходная связка, аксиомы Лукасевича говорят только об отрицании и импликации, а правило замены двойного отрицания (ЗДО) лишь добавляет или снимает двойные отрицания. Поэтому урок сначала устанавливает три инструмента. Первый утверждает, что доказуемая эквивалентность ведёт себя как равенство. Второй, основная лемма, переводит стрелку Пирса на язык аксиом: (φ↓ψ)(\varphi \downarrow \psi) эквивалентна ¬(¬φ→ψ)\neg(\neg\varphi \rightarrow \psi) благодаря правилу ЗДО и двойному отрицанию. Третий, замена эквивалентных, которую правило ЗДО не делает излишней, позволяет заменить формулу любой эквивалентной ей формулой (а не только θ\theta формулой ¬¬θ\neg\neg\theta) под отрицанием, по обе стороны импликации и по обе стороны стрелки Пирса. С их помощью доказываются, как эквивалентности, эквивалентные формы дизъюнкции и конъюнкции, которые другие тексты принимают за определения, и пять симметрий, в обе стороны и в том порядке, который диктуют определения: сначала стрелка Пирса, а из неё последовательно остальные.

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

  1. Раскрывать официальные сокращения, чтобы решать, обозначают ли два выражения одну и ту же формулу или разные формулы, эквивалентность которых требует вывода.
  2. Доказывать основную лемму (φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi) с помощью правила замены двойного отрицания (ЗДО) и двойного отрицания, находя двойные отрицания, которые скрывают сокращения.
  3. Применять замену эквивалентных, чтобы переносить эквивалентность внутрь отрицания, импликации или стрелки Пирса, отличать её от правила ЗДО, которое лишь меняет местами θ\theta и ¬¬θ\neg\neg\theta, и пользоваться доказуемой эквивалентностью как равенством в цепях эквивалентностей.
  4. Доказывать эквивалентные формы дизъюнкции и конъюнкции и пять симметрий в обе стороны, сцепляя уже доказанные результаты.
  5. Распространять замену эквивалентных на любую формулу посредством индукции по сложности формул.

Что используется и что предстоит доказать

Урок о формальных дедуктивных системах зафиксировал систему Лукасевича: аксиомы A1, A2 и A3 и modus ponens. Кроме того, он установил рефлексивность (Рефл: если φ∈Γ\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; и показал с помощью разметки, которую аксиомы и modus ponens сохраняют, что эта система не выводит некоторых формул о стрелке Пирса. Урок о четырёх приёмах вывода добавил гипотетический силлогизм (ГС: {(φ→ψ),(ψ→χ)}⊢(φ→χ)\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)), перестановку посылок (ПП), двойное отрицание (ДО: φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi, с двумя его теоремами ⊢(¬¬φ→φ)\vdash (\neg\neg\varphi \rightarrow \varphi) и ⊢(φ→¬¬φ)\vdash (\varphi \rightarrow \neg\neg\varphi)) и контрапозицию (Контр) в трёх её формах:

(φ→ψ)⊣⊢(¬ψ→¬φ),(¬φ→ψ)⊣⊢(¬ψ→φ),(φ→¬ψ)⊣⊢(ψ→¬φ)(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi), \qquad (\neg\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \varphi), \qquad (\varphi \rightarrow \neg\psi) \dashv\vdash (\psi \rightarrow \neg\varphi)

Доказав двойное отрицание, тот же урок дополнил систему курса вторым исходным правилом, заменой двойного отрицания (ЗДО): если χ′\chi' получается из χ\chi заменой одного вхождения подформулы θ\theta на ¬¬θ\neg\neg\theta или одного вхождения подформулы ¬¬θ\neg\neg\theta на θ\theta, то из χ\chi выводится χ′\chi'. Полученная так из строки ii строка обосновывается как ЗДО(i)(i). С этого места ⊢\vdash относится к системе курса (A1, A2, A3, modus ponens и ЗДО), в которой по-прежнему верны Рефл, Мон, Сеч, ТД и ОТД. Правило действует на цепочку базового языка, так что достигает и тех вхождений, которые скрывает сокращение, причём в любом из двух аргументов стрелки Пирса; среди его непосредственных следствий

(φ↓ψ)⊣⊢(¬¬φ↓ψ),(φ↓ψ)⊣⊢(φ↓¬¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi), \qquad (\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi)

и вообще χ⊣⊢χ′\chi \dashv\vdash \chi' всякий раз, когда χ′\chi' получается из χ\chi по ЗДО. Строка эквивалентности такого вида обосновывается как «ЗДО», без номера строки, точно так же, как строка «ДО» или «Контр» ссылается на уже доказанную эквивалентность. Как и там, уже доказанную теорему можно записать строкой вывода, потому что её собственный вывод можно вставить на это место; а по лемме «от результата к правилу» того урока каждый приём применяется и как правило при любом множестве посылок Γ\Gamma, со ссылкой на номера строк, к которым оно применяется, как Контр(i)(i) или ГС(i,j)(i, j). В выводах о выводах «Посылка» обозначает одну из гипотез доказываемого правила.

Официальные сокращения, зафиксированные в уроке о языке логики высказываний, суть единственные определения связок:

¬φ:=(φ↓φ),(φ∨ψ):=¬(φ↓ψ),(φ∧ψ):=¬(¬φ∨¬ψ)\neg\varphi := (\varphi \downarrow \varphi), \qquad (\varphi \vee \psi) := \neg(\varphi \downarrow \psi), \qquad (\varphi \wedge \psi) := \neg(\neg\varphi \vee \neg\psi)
(φ→ψ):=(¬φ∨ψ),(φ↔ψ):=((φ→ψ)∧(ψ→φ)),(φ⊻ψ):=¬(φ↔ψ)(\varphi \rightarrow \psi) := (\neg\varphi \vee \psi), \qquad (\varphi \leftrightarrow \psi) := ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)), \qquad (\varphi \veebar \psi) := \neg(\varphi \leftrightarrow \psi)

Строка, обоснованная как «Опр», ничего не выводит: она записывает ту же формулу под другим именем, а пометка говорит, какое сокращение раскрывается или свёртывается («Опр →\rightarrow», «Опр ∨\vee»). Полезно вспомнить явление, отмеченное в уроке о формализации естественного языка: одна и та же формула допускает несколько имён, так что конъюнкция, как цепочка, есть также дизъюнкция. Например, раскрывая импликацию с ¬φ\neg\varphi вместо φ\varphi, получаем

(¬φ→ψ)=(¬¬φ∨ψ)=¬(¬¬φ↓ψ)(\neg\varphi \rightarrow \psi) = (\neg\neg\varphi \vee \psi) = \neg(\neg\neg\varphi \downarrow \psi)

и двойное отрицание, стоящее перед φ\varphi и скрытое сокращением, есть причина, по которой правило ЗДО будет участвовать во всём дальнейшем.

Доказуемая эквивалентность как равенство

Доказательства этого урока почти все суть цепи эквивалентностей: φ1⊣⊢φ2\varphi_{1} \dashv\vdash \varphi_{2}, φ2⊣⊢φ3\varphi_{2} \dashv\vdash \varphi_{3} и так далее. Чтобы из цепи заключить φ1⊣⊢φn\varphi_{1} \dashv\vdash \varphi_{n}, доказуемая эквивалентность должна вести себя как равенство, и именно это установило утверждение о свойствах доказуемой эквивалентности из урока о формальных дедуктивных системах: отношение рефлексивно (φ⊣⊢φ\varphi \dashv\vdash \varphi), симметрично (если φ⊣⊢ψ\varphi \dashv\vdash \psi, то ψ⊣⊢φ\psi \dashv\vdash \varphi) и транзитивно (если φ⊣⊢ψ\varphi \dashv\vdash \psi и ψ⊣⊢χ\psi \dashv\vdash \chi, то φ⊣⊢χ\varphi \dashv\vdash \chi), а две доказуемо эквивалентные формулы взаимозаменяемы как заключения (если Γ⊢φ\Gamma \vdash \varphi и φ⊣⊢φ′\varphi \dashv\vdash \varphi', то Γ⊢φ′\Gamma \vdash \varphi', для всякого множества Γ\Gamma формул). Полезно вспомнить, как были доказаны два последних свойства, потому что на них опирается весь урок: от {φ}⊢φ′\{\varphi\} \vdash \varphi' по монотонности переходим к Γ∪{φ}⊢φ′\Gamma \cup \{\varphi\} \vdash \varphi', а от него и от Γ⊢φ\Gamma \vdash \varphi по сечению к Γ⊢φ′\Gamma \vdash \varphi'; транзитивность получается применением этого с Γ={φ}\Gamma = \{\varphi\} в одну сторону и с Γ={χ}\Gamma = \{\chi\} в другую.

В дальнейшем шаг, который сводит цепь эквивалентностей в одну эквивалентность, обосновывается как «Сеч», потому что это инструмент того утверждения. Но каждое звено φi⊣⊢φi+1\varphi_{i} \dashv\vdash \varphi_{i+1} содержит оба вывода, прямой и обратный; откуда цепь эквивалентностей доказывает сразу оба направления своего заключения, и ничего не остаётся «в качестве упражнения».