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

Вывод: итоги и задачи повышенной трудности

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

Этот урок завершает раздел, посвящённый выводу. Он восстанавливает дедуктивную цепь, которая ведёт от определения системы Лукасевича (три схемы аксиом и modus ponens) к теореме о дедукции и к пределу этой системы в языке стрелки Пирса; оттуда к четырём основным приёмам и к правилу замены двойного отрицания, которое завершает систему курса; от основной леммы о стрелке Пирса к замене эквивалентных и к симметриям, а оттуда к правилам классической логики и к законам де Моргана и дистрибутивности, и указывает в каждом звене, какие результаты в нём используются и в каком уроке оно доказывается. Он отделяет то, что раздел доказал, от того, что раздел принял, соотносит достигнутое с планом курса и объясняет, почему вопрос, который раздел оставляет открытым, а именно совпадает ли выводимое с истинным, ведёт к разделу о семантике. В итоговой проверке он повторяет навыки входной проверки и заканчивается шестью задачами повышенной трудности, более сложными, чем задачи уроков, которые требуют соединять средства нескольких из них.

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

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

Чего достиг раздел

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

Система Лукасевича и её предел

Урок о формальных дедуктивных системах определил систему как язык, аксиомы и правила, которые все проверяются лишь по виду цепочек, и зафиксировал первый этап системы курса, систему Лукасевича: схемы A1, A2 и A3 и modus ponens как единственное правило, которое однозначность разбора делает применимым без двусмысленности. Он определил вывод из множества посылок Γ\Gamma и отношение Γ⊢φ\Gamma \vdash \varphi, вывел ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi) за пять строк и доказал структурные свойства: рефлексивность, монотонность, modus ponens для выводов, сечение и конечность. С их помощью и с помощью сильной индукции по числу строк он доказал теорему о дедукции, второй случай которой требует, чтобы (φ→φ)(\varphi \rightarrow \varphi) было выведено заранее, и обратную к ней теорему; из них он получил доказуемую эквивалентность, рефлексивную, симметричную и транзитивную. Наконец, он установил предел этой системы: разметка со значениями 00 и 11, определённая по рекурсии на исходной форме (α↓β)(\alpha \downarrow \beta), обращается с отрицанием и импликацией как обычно, сохраняется схемами A1, A2, A3 и modus ponens и оставляет свободным значение таких формул, как (v1↓v2)(v_{1} \downarrow v_{2}). Отсюда следует, что ((v1↓v2)→¬v1)((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1}) не является теоремой системы Лукасевича и что из (v1↓v2)(v_{1} \downarrow v_{2}) не выводится (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}), и наоборот. Поскольку всякая разметка даёт одно и то же значение формулам θ\theta и ¬¬θ\neg\neg\theta, урок заметил также, что даже двойное отрицание, будучи доказанным, не устранило бы этого предела.

Четыре приёма и новое правило

Урок о четырёх приёмах вывода сначала доказал лемму «от результата к правилу»: если {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta, то то же заключение получается из любого множества Γ\Gamma, из которого выводятся формулы αi\alpha_{i}, и, кроме того, ⊢(α1→(α2→⋯(αn→β)⋯ ))\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots)). Именно эта лемма позволяет пользоваться каждым приёмом в трёх видах (из посылок, как теоремой и как правилом), а уроки о симметриях и о законах де Моргана, которые сцепляют цепи эквивалентностей с сечением, опираются для этого на свойства доказуемой эквивалентности из первого урока, выражающие ту же идею для одной посылки; в цепи каждый результат фигурирует один раз, там, где он доказывается. С её помощью урок вывел гипотетический силлогизм из A1 и A2 за семь строк, перестановку посылок с помощью теоремы о дедукции, двойное отрицание (первое направление которого дважды применяет A3 к импликации, изготовленной с помощью A1, а второе применяет первое к ¬φ\neg\varphi и A3) и контрапозицию в трёх её формах, которые тремя способами распределяют отрицания импликации; все четыре верны уже в системе Лукасевича.

Доказав двойное отрицание, урок дополнил систему курса вторым исходным правилом, заменой двойного отрицания (ЗДО): из χ\chi выводится χ′\chi', когда χ′\chi' получается заменой в χ\chi одного вхождения подформулы θ\theta на ¬¬θ\neg\neg\theta или одного вхождения ¬¬θ\neg\neg\theta на θ\theta. Правило приходится постулировать, потому что разметка m1m_{1} даёт 11 теоремам двойного отрицания и тем не менее разделяет (v1↓v2)(v_{1} \downarrow v_{2}) и (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}); ЗДО не сохраняет m1m_{1} и потому расширяет выводимое, но сохраняет честную разметку и потому не расширяет его слишком сильно. Правило действует на цепочку базового языка, где отрицание удваивает свой аргумент: (φ→ψ)(\varphi \rightarrow \psi) дважды содержит подформулу ¬φ\neg\varphi, и чтобы поставить двойное отрицание перед её антецедентом, нужны два применения. То же наблюдение лежит в основе распространения теоремы о дедукции: если строка получена по правилу, предположение индукции даёт импликацию, консеквент которой есть предыдущая строка, и два применения правила, по одному в каждой копии этого консеквента, дают искомую импликацию; остальные структурные свойства верны с тем же доказательством. Первые следствия таковы: формула эквивалентна всякой формуле, получающейся из неё по правилу, в частности (φ↓ψ)⊣⊢(¬¬φ↓ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi) и (φ↓ψ)⊣⊢(φ↓¬¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi), а соответствующие импликации, которые другие системы принимают за аксиомы, здесь являются теоремами.

Связки и замена

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

Классические правила и законы

Урок о приёмах классической логики доказал, все с множеством посылок Γ\Gamma, которое переносится из строки в строку, введение и удаление дизъюнкции и конъюнкции, закон исключённого третьего и закон непротиворечия, принцип взрыва, доказательство от противного в двух его формах и разбор случаев, с формулой и её отрицанием и с произвольной дизъюнкцией. Порядок зависимостей строг: принцип взрыва опирается на правила дизъюнкции; классическое доказательство от противного, на принцип взрыва и A3; разбор случаев, на контрапозицию и доказательство от противного. Ни одно из этих доказательств не ссылается на правило ЗДО непосредственно: правило действует через эквивалентные формы и замену эквивалентных. Урок о законах де Моргана и дистрибутивности заставил эти правила работать вместе: первый закон де Моргана получается из определения конъюнкции и двойного отрицания; второй требует войти внутрь стрелки Пирса, где правило ЗДО вмешивается дважды, по разу в каждом аргументе и без надобности в симметрии, и из него следует, что (φ↓ψ)(\varphi \downarrow \psi) эквивалентна (¬φ∧¬ψ)(\neg\varphi \wedge \neg\psi), то есть прочтению «ни φ\varphi, ни ψ\psi», которое предыдущий раздел установил по соглашению; среди вариантов есть и ¬(φ→ψ)⊣⊢(φ∧¬ψ)\neg(\varphi \rightarrow \psi) \dashv\vdash (\varphi \wedge \neg\psi). Оба закона дистрибутивности были доказаны в обоих направлениях разбором случаев, причём в каждом выбиралась подходящая форма разбора случаев.

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

Опоры цепи

  • AОднозначность разбора и рекурсия. Если ∙φψ=∙φ′ψ′\sigI\varphi\psi = \sigI\varphi'\psi', где все четыре цепочки суть формулы, то φ=φ′\varphi = \varphi' и ψ=ψ′\psi = \psi'; отсюда правило, которое вычисляет значение ∙φψ\sigI\varphi\psi по φ\varphi, ψ\psi и их значениям, определяет единственную функцию на формулах. Доказано в предыдущем разделе. В этом модуле принимается без доказательства.
  • BСильная индукция. Если свойство выполняется для натурального числа всякий раз, когда оно выполняется для всех меньших, то оно выполняется для всех натуральных чисел. Она была выведена из простой индукции в предыдущем разделе и здесь применяется к числу строк вывода. В этом модуле принимается без доказательства.
  • CАксиомы Лукасевича. Схемы A1, (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)); A2, ((φ→(ψ→χ))→((φ→ψ)→(φ→χ)))((\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi))); и A3, ((¬ψ→¬φ)→(φ→ψ))((\neg\psi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \psi)). Принимаются. В этом модуле принимается без доказательства.
  • DЗамена двойного отрицания. Второе исходное правило системы курса: из χ\chi выводится χ′\chi', если χ′\chi' получается из χ\chi заменой одного вхождения подформулы θ\theta на ¬¬θ\neg\neg\theta или одного вхождения ¬¬θ\neg\neg\theta на θ\theta. Постулируется после доказательства двойного отрицания. Устанавливается в: 8. Замена двойного отрицания.
  • EТеорема о дедукции. Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi тогда и только тогда, когда Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi); доказывается в системе Лукасевича и верна, с одним дополнительным случаем, в системе курса. Устанавливается в: 3. Теорема о дедукции и доказуемая эквивалентность.
  • FОт результата к правилу. Если {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta и Γ⊢αi\Gamma \vdash \alpha_{i} для каждого ii, то Γ⊢β\Gamma \vdash \beta: всякий приём, доказанный из посылок, применим при любом множестве посылок. Устанавливается в: 5. От результата к правилу.
  • GДвойное отрицание. φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi, с теоремами ⊢(¬¬φ→φ)\vdash (\neg\neg\varphi \rightarrow \varphi) и ⊢(φ→¬¬φ)\vdash (\varphi \rightarrow \neg\neg\varphi). Устанавливается в: 7. Двойное отрицание.
  • HЗамена эквивалентных. Если φ⊣⊢φ′\varphi \dashv\vdash \varphi', то φ′\varphi' можно поставить вместо φ\varphi под отрицанием, по обе стороны импликации, стрелки Пирса, дизъюнкции и конъюнкции, не нарушая эквивалентности. Устанавливается в: 12. Замена эквивалентных.

  1. Участок 1 Система Лукасевича и её предел

    • Распознавать частные случаи схем и решать, является ли последовательность формул выводом из множества посылок.
    • Доказывать структурные свойства выводимости и теорему о дедукции сильной индукцией по числу строк.
    • Строить выводы о выводах с помощью рефлексивности, монотонности, сечения, теоремы о дедукции и обратной к ней.
    • Доказывать, что формула не выводится, с помощью разметки, которую сохраняют аксиомы и modus ponens, и объяснять с её помощью предел системы Лукасевича.

    1. Система, вывод и тождество. Аксиомы системы Лукасевича суть равномерные частные случаи схем от A1 до A3, а её единственное правило есть modus ponens. Γ⊢φ\Gamma \vdash \varphi, если существует конечная последовательность формул, которая оканчивается на φ\varphi и каждая формула которой есть аксиома, элемент Γ\Gamma или получена по modus ponens из двух предыдущих. Первая теорема, ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi), выводится за пять строк с помощью A1 и A2.

      Опирается на: A (Однозначность разбора и рекурсия), C (Аксиомы Лукасевича). Доказывается в уроке: Формальные дедуктивные системы.

    2. Структурные свойства. Если φ∈Γ\varphi \in \Gamma, то Γ⊢φ\Gamma \vdash \varphi; если Γ⊆Δ\Gamma \subseteq \Delta и Γ⊢φ\Gamma \vdash \varphi, то Δ⊢φ\Delta \vdash \varphi; из Γ⊢φ\Gamma \vdash \varphi и Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi) следует Γ⊢ψ\Gamma \vdash \psi; если Γ⊢φi\Gamma \vdash \varphi_{i} для каждого ii и Γ∪{φ1,…,φr}⊢ψ\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{r}\} \vdash \psi, то Γ⊢ψ\Gamma \vdash \psi; и если Γ⊢φ\Gamma \vdash \varphi, то достаточно некоторого конечного подмножества Γ\Gamma.

      Использует: 1. Система, вывод и тождество. Доказывается в уроке: Формальные дедуктивные системы.

    3. Теорема о дедукции и доказуемая эквивалентность. Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi тогда и только тогда, когда Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi), по сильной индукции по числу строк, с помощью A1, A2 и тождества. Отсюда доказуемая эквивалентность, φ⊣⊢ψ\varphi \dashv\vdash \psi, рефлексивна, симметрична и транзитивна, и две эквивалентные формулы выводятся из одних и тех же множеств.

      Использует: 1. Система, вывод и тождество, 2. Структурные свойства. Опирается на: B (Сильная индукция), C (Аксиомы Лукасевича). Доказывается в уроке: Формальные дедуктивные системы.

    4. Предел системы Лукасевича. Разметка со значениями 00 и 11, определённая по рекурсии, удовлетворяет условиям m(¬φ)=1−m(φ)m(\neg\varphi) = 1 - m(\varphi) и m((φ→ψ))=1−m(φ)(1−m(ψ))m((\varphi \rightarrow \psi)) = 1 - m(\varphi) \left( 1 - m(\psi) \right), а A1, A2, A3 и modus ponens сохраняют метку 11; отсюда ((v1↓v2)→¬v1)((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1}) не является теоремой системы Лукасевича, и {(v1↓v2)}⊬(¬¬v1↓v2)\{(v_{1} \downarrow v_{2})\} \nvdash (\neg\neg v_{1} \downarrow v_{2}), и наоборот. Поскольку всякая разметка даёт 11 двойному отрицанию, замену приходится постулировать.

      Использует: 1. Система, вывод и тождество. Опирается на: A (Однозначность разбора и рекурсия), B (Сильная индукция), C (Аксиомы Лукасевича). Доказывается в уроке: Формальные дедуктивные системы.

  2. Участок 2 Четыре приёма и новое правило

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

    1. От результата к правилу. Если {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta, то из Γ⊢α1\Gamma \vdash \alpha_{1}, …\ldots, Γ⊢αn\Gamma \vdash \alpha_{n} следует Γ⊢β\Gamma \vdash \beta, и ⊢(α1→(α2→⋯(αn→β)⋯ ))\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots)); в частности, если α⊣⊢α′\alpha \dashv\vdash \alpha', то Γ⊢α\Gamma \vdash \alpha тогда и только тогда, когда Γ⊢α′\Gamma \vdash \alpha'.

      Использует: 2. Структурные свойства. Опирается на: E (Теорема о дедукции). Доказывается в уроке: Четыре приёма вывода.

    2. Гипотетический силлогизм и перестановка. {(φ→ψ),(ψ→χ)}⊢(φ→χ)\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi), выводом из семи строк с помощью A1 и A2; и {(φ→(ψ→χ))}⊢(ψ→(φ→χ))\{(\varphi \rightarrow (\psi \rightarrow \chi))\} \vdash (\psi \rightarrow (\varphi \rightarrow \chi)).

      Использует: 1. Система, вывод и тождество. Опирается на: C (Аксиомы Лукасевича), E (Теорема о дедукции), F (От результата к правилу). Доказывается в уроке: Четыре приёма вывода.

    3. Двойное отрицание. ⊢(¬¬φ→φ)\vdash (\neg\neg\varphi \rightarrow \varphi), двукратным применением A3 к импликации, которую A1 изготавливает из ¬¬φ\neg\neg\varphi; ⊢(φ→¬¬φ)\vdash (\varphi \rightarrow \neg\neg\varphi), применением предыдущего к ¬φ\neg\varphi и A3; отсюда φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi, уже в системе Лукасевича.

      Опирается на: C (Аксиомы Лукасевича), E (Теорема о дедукции). Доказывается в уроке: Четыре приёма вывода.

    4. Замена двойного отрицания. Постулируется правило ЗДО, потому что разметка даёт 11 двойному отрицанию, но не замене внутри стрелки Пирса. Если χ′\chi' получается из χ\chi по правилу, то χ⊣⊢χ′\chi \dashv\vdash \chi'; в частности, (φ↓ψ)⊣⊢(¬¬φ↓ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi) и (φ↓ψ)⊣⊢(φ↓¬¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi).

      Использует: 3. Теорема о дедукции и доказуемая эквивалентность, 4. Предел системы Лукасевича. Опирается на: G (Двойное отрицание). Доказывается в уроке: Четыре приёма вывода.

    5. Теорема о дедукции в системе курса. Рефлексивность, монотонность, сечение и конечность верны с новым правилом, а также Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi тогда и только тогда, когда Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi): в новом случае, поскольку (φ→χ)(\varphi \rightarrow \chi) есть ((¬φ↓χ)↓(¬φ↓χ))((\neg\varphi \downarrow \chi) \downarrow (\neg\varphi \downarrow \chi)), правило применяется дважды, по разу в каждой копии χ\chi. Отсюда ⊢((φ↓ψ)→(¬¬φ↓ψ))\vdash ((\varphi \downarrow \psi) \rightarrow (\neg\neg\varphi \downarrow \psi)) и обратная к ней импликация являются теоремами.

      Использует: 2. Структурные свойства, 3. Теорема о дедукции и доказуемая эквивалентность. Опирается на: B (Сильная индукция), D (Замена двойного отрицания). Доказывается в уроке: Четыре приёма вывода.

    6. Контрапозиция. (φ→ψ)⊣⊢(¬ψ→¬φ)(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi), (¬φ→ψ)⊣⊢(¬ψ→φ)(\neg\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \varphi) и (φ→¬ψ)⊣⊢(ψ→¬φ)(\varphi \rightarrow \neg\psi) \dashv\vdash (\psi \rightarrow \neg\varphi): члены меняются местами, и каждый при переходе меняет знак.

      Использует: 6. Гипотетический силлогизм и перестановка. Опирается на: C (Аксиомы Лукасевича), E (Теорема о дедукции), G (Двойное отрицание), F (От результата к правилу). Доказывается в уроке: Четыре приёма вывода.

  3. Участок 3 Связки и замена

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

    1. Основная лемма. (φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi): поскольку ¬(¬φ→ψ)\neg(\neg\varphi \rightarrow \psi) есть ¬¬(¬¬φ↓ψ)\neg\neg(\neg\neg\varphi \downarrow \psi), правило ЗДО ставит внутреннее двойное отрицание, а двойное отрицание ставит внешнее; в обратном направлении двойное отрицание и правило их снимают.

      Опирается на: D (Замена двойного отрицания), G (Двойное отрицание). Доказывается в уроке: Симметрии связок.

    2. Замена эквивалентных. Если φ⊣⊢φ′\varphi \dashv\vdash \varphi', то ¬φ⊣⊢¬φ′\neg\varphi \dashv\vdash \neg\varphi', (φ→ψ)⊣⊢(φ′→ψ)(\varphi \rightarrow \psi) \dashv\vdash (\varphi' \rightarrow \psi) и (ψ→φ)⊣⊢(ψ→φ′)(\psi \rightarrow \varphi) \dashv\vdash (\psi \rightarrow \varphi'); с помощью основной леммы то же по обе стороны стрелки Пирса, а оттуда дизъюнкции и конъюнкции. В отличие от правила ЗДО, она допускает любые эквивалентные формулы.

      Использует: 6. Гипотетический силлогизм и перестановка, 10. Контрапозиция, 11. Основная лемма. Опирается на: E (Теорема о дедукции). Доказывается в уроке: Симметрии связок.

    3. Эквивалентные формы. (φ∨ψ)⊣⊢(¬φ→ψ)(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi), с двумя применениями правила ЗДО, по одному в каждой копии, которую создаёт внешнее отрицание; (φ∧ψ)⊣⊢(¬φ↓¬ψ)(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi), по двойному отрицанию; а (φ∧ψ)(\varphi \wedge \psi) есть та же цепочка, что и ¬(φ→¬ψ)\neg(\varphi \rightarrow \neg\psi).

      Опирается на: D (Замена двойного отрицания), G (Двойное отрицание). Доказывается в уроке: Симметрии связок.

    4. Пять симметрий. (φ↓ψ)⊣⊢(ψ↓φ)(\varphi \downarrow \psi) \dashv\vdash (\psi \downarrow \varphi), по основной лемме и контрапозиции; из неё последовательно симметрии ∨\vee, ∧\wedge, ↔\leftrightarrow и ⊻\veebar, каждая с помощью предыдущей, перенесённой заменой под отрицанием, когда это нужно.

      Использует: 11. Основная лемма, 10. Контрапозиция. Опирается на: H (Замена эквивалентных). Доказывается в уроке: Симметрии связок.

  4. Участок 4 Классические правила и законы

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

    1. Правила связок. При любом Γ\Gamma: из φ\varphi следует (φ∨ψ)(\varphi \vee \psi); из (φ∨ψ)(\varphi \vee \psi) и ¬φ\neg\varphi, ψ\psi; из φ\varphi и ψ\psi, (φ∧ψ)(\varphi \wedge \psi); из (φ∧ψ)(\varphi \wedge \psi), φ\varphi и ψ\psi; кроме того, ⊢(φ∨¬φ)\vdash (\varphi \vee \neg\varphi) и ⊢¬(φ∧¬φ)\vdash \neg(\varphi \wedge \neg\varphi).

      Использует: 1. Система, вывод и тождество, 2. Структурные свойства, 6. Гипотетический силлогизм и перестановка, 10. Контрапозиция, 13. Эквивалентные формы, 14. Пять симметрий. Опирается на: C (Аксиомы Лукасевича), E (Теорема о дедукции), F (От результата к правилу), G (Двойное отрицание). Доказывается в уроке: Приёмы классической логики.

    2. Принцип взрыва и доказательство от противного. Если Γ⊢φ\Gamma \vdash \varphi и Γ⊢¬φ\Gamma \vdash \neg\varphi, то Γ⊢ψ\Gamma \vdash \psi для всякой ψ\psi; если из Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} выводятся ψ\psi и ¬ψ\neg\psi, то Γ⊢φ\Gamma \vdash \varphi; и если они выводятся из Γ∪{φ}\Gamma \cup \{\varphi\}, то Γ⊢¬φ\Gamma \vdash \neg\varphi.

      Использует: 1. Система, вывод и тождество, 2. Структурные свойства, 15. Правила связок. Опирается на: C (Аксиомы Лукасевича), E (Теорема о дедукции), G (Двойное отрицание). Доказывается в уроке: Приёмы классической логики.

    3. Разбор случаев. Если Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi и Γ∪{¬φ}⊢ψ\Gamma \cup \{\neg\varphi\} \vdash \psi, то Γ⊢ψ\Gamma \vdash \psi; и если Γ∪{φ}⊢χ\Gamma \cup \{\varphi\} \vdash \chi, Γ∪{ψ}⊢χ\Gamma \cup \{\psi\} \vdash \chi и Γ⊢(φ∨ψ)\Gamma \vdash (\varphi \vee \psi), то Γ⊢χ\Gamma \vdash \chi.

      Использует: 2. Структурные свойства, 10. Контрапозиция, 15. Правила связок, 16. Принцип взрыва и доказательство от противного. Опирается на: E (Теорема о дедукции). Доказывается в уроке: Приёмы классической логики.

    4. Законы де Моргана. ¬(φ∧ψ)⊣⊢(¬φ∨¬ψ)\neg(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \vee \neg\psi), по определению и двойному отрицанию; ¬(φ∨ψ)⊣⊢(¬φ∧¬ψ)\neg(\varphi \vee \psi) \dashv\vdash (\neg\varphi \wedge \neg\psi), с одним применением правила ЗДО в каждом аргументе стрелки Пирса; отсюда (φ↓ψ)⊣⊢(¬φ∧¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\varphi \wedge \neg\psi) и ¬(φ→ψ)⊣⊢(φ∧¬ψ)\neg(\varphi \rightarrow \psi) \dashv\vdash (\varphi \wedge \neg\psi).

      Опирается на: D (Замена двойного отрицания), G (Двойное отрицание), H (Замена эквивалентных). Доказывается в уроке: Законы де Моргана и дистрибутивности.

    5. Законы дистрибутивности. (φ∧(ψ∨χ))⊣⊢((φ∧ψ)∨(φ∧χ))(\varphi \wedge (\psi \vee \chi)) \dashv\vdash ((\varphi \wedge \psi) \vee (\varphi \wedge \chi)) и (φ∨(ψ∧χ))⊣⊢((φ∨ψ)∧(φ∨χ))(\varphi \vee (\psi \wedge \chi)) \dashv\vdash ((\varphi \vee \psi) \wedge (\varphi \vee \chi)), каждый в обоих направлениях разбором случаев; с помощью симметрий также справа.

      Использует: 14. Пять симметрий, 15. Правила связок, 17. Разбор случаев. Опирается на: H (Замена эквивалентных). Доказывается в уроке: Законы де Моргана и дистрибутивности.

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

Сокращения в обоснованиях

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

  • Первый урок: A1, A2 и A3 (схемы аксиом); MP(i,j)(i, j) (modus ponens); Опр (определение: раскрытие или свёртывание сокращения, с раскрываемой связкой: «Опр ∨\vee», «Опр ⊣⊢\dashv\vdash»); Тожд (тождество, теорема ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi)); Рефл (рефлексивность: если φ∈Γ\varphi \in \Gamma, то Γ⊢φ\Gamma \vdash \varphi); Мон (монотонность); Сеч (сечение: выведенное можно использовать как посылку); Кон (конечность); ТД (теорема о дедукции) и ОТД (обратная к ней).
  • Второй урок: ГС (гипотетический силлогизм); ПП (перестановка посылок); ДО (двойное отрицание); ЗДО(i)(i) (замена двойного отрицания в строке ii; ЗДО без номера указывает эквивалентность формулы и формулы, получающейся из неё по правилу); Контр (контрапозиция, в любой из трёх её форм); «Решённая задача nn» (результат решённой задачи nn того же урока, записанный как строка).
  • Третий урок: ОЛ (основная лемма, (φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)); Зам (замена эквивалентных, в любой из её форм, за которой следует применяемая эквивалентность: «Зам, ДМ(i)(i)»); Экв (эквивалентные формы дизъюнкции и конъюнкции, (φ∨ψ)⊣⊢(¬φ→ψ)(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi) и (φ∧ψ)⊣⊢(¬φ↓¬ψ)(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi)); Сим (симметрия связки).
  • Четвёртый урок: ∨\veeв и ∨\veeу (введение и удаление дизъюнкции); ∧\wedgeв и ∧\wedgeу (введение и удаление конъюнкции); ИТ (закон исключённого третьего); НП (закон непротиворечия; сокращение называет теорему, но не обосновывает ни одной строки раздела); Взр (принцип взрыва); Случ(i,j)(i, j) и Случ(i,j,k)(i, j, k) (разбор случаев, с формулой и её отрицанием или с дизъюнкцией); «Случ без посылок» (разбор случаев без множества Γ\Gamma, который встречается только в одной задаче); ОП (доказательство от противного, в двух его формах).
  • Пятый урок: ДМ (законы де Моргана); Дистр (дистрибутивность); Асс (ассоциативность дизъюнкции); Подст(i)(i) (частный случай: строка ii, верная для любых формул, переписанная с другими формулами вместо её метапеременных; указывается, что на что подставлено).
  • Задачи повышенной трудности этого урока: M3 (схема, которую третья задача ставит на место A3).