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

Приёмы классической логики

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

Рассуждая в математике, вводят и удаляют конъюнкции и дизъюнкции, ссылаются на исключённое третье, отбрасывают противоречивое, разбирают случаи и приводят к абсурду, почти никогда этого не замечая. Этот урок доказывает, что все эти приёмы суть производные правила дедуктивной системы курса, и доказывает их в том виде, в каком ими пользуются: с множеством Γ\Gamma посылок, которое сохраняется на протяжении всего вывода. Сначала он напоминает, что всякое уже доказанное правило действует внутри контекста Γ\Gamma; затем доказывает введение и удаление дизъюнкции и конъюнкции, исключённое третье и непротиворечие, взрыв, доказательство от противного в двух его формах и разбор случаев, сначала с формулой и её отрицанием, а затем с произвольной дизъюнкцией. Задачи применяют эти приёмы к классическим законам, таким как закон Пирса и дилеммы, и показывают, почему недостаточно доказать их без посылок.

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

  1. Применять к строкам вида Γ⊢φ\Gamma \vdash \varphi правила и эквивалентности, доказанные ранее, обосновывая шаг монотонностью и сечением.
  2. Доказывать с посылками правила введения и удаления дизъюнкции и конъюнкции, раскрывая официальные сокращения только там, где это допустимо.
  3. Выводить закон исключённого третьего и закон непротиворечия и различать на каждом шаге, что есть определение, а что теорема.
  4. Доказывать принцип взрыва, доказательство от противного в двух его формах и разбор случаев с посылками и объяснять, почему варианты без посылок недостаточны.
  5. Строить выводы классических законов (Пирса, экспортации, дилемм), сочетая эти приёмы, и связывать выводимость формулы с противоречивостью множества посылок.

Правила внутри контекста

В уроке о формальных дедуктивных системах была задана система Лукасевича: схемы аксиом A1, A2 и A3, правило modus ponens (MP) и понятие вывода из множества Γ\Gamma посылок с его первыми свойствами: рефлексивностью (Рефл: если φ∈Γ\varphi \in \Gamma, то Γ⊢φ\Gamma \vdash \varphi), монотонностью (Мон: если Γ⊆Δ\Gamma \subseteq \Delta и Γ⊢φ\Gamma \vdash \varphi, то Δ⊢φ\Delta \vdash \varphi), сечением (Сеч), modus ponens для выводов (если Γ⊢φ\Gamma \vdash \varphi и Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi), то Γ⊢ψ\Gamma \vdash \psi; на него также ссылаются как на MP), теоремой о дедукции (ТД: если Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi, то Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi)) и обратной к ней (ОТД). Уроки о четырёх приёмах вывода и о симметриях связок добавили гипотетический силлогизм (ГС), перестановку посылок (ПП), двойное отрицание (ДО), контрапозицию (Контр) в трёх её формах, замену эквивалентных (Зам), симметрии (Сим) и эквивалентные формы дизъюнкции и конъюнкции. Первый из них, доказав двойное отрицание, дополнил к тому же систему курса вторым исходным правилом, заменой двойного отрицания (ЗДО): если χ′\chi' получается из χ\chi заменой одного вхождения подформулы θ\theta на ¬¬θ\neg\neg\theta или одного вхождения ¬¬θ\neg\neg\theta на θ\theta, то из χ\chi выводится χ′\chi'. В дальнейшем ⊢\vdash относится к этой системе (от A1 до A3, MP и ЗДО), в которой по-прежнему верны рефлексивность, монотонность, сечение, теорема о дедукции и обратная к ней; приёмы этого урока суть её производные правила, хотя ни одно из их доказательств не ссылается на ЗДО непосредственно: правило действует через эквивалентные формы и замену эквивалентных, которые урок о симметриях доказал с его помощью.

Однако в математике никто не рассуждает без посылок: рассуждают исходя из аксиом, из условий теоремы и из того, что допущено для разбора случая. Если это так, приём рассуждения полезен лишь тогда, когда он формулируется с множеством Γ\Gamma посылок, которое переносится от строки к строке. Отсюда следует, что каждое правило этого урока формулируется и доказывается для произвольного Γ\Gamma; случай без посылок есть частный случай Γ=∅\Gamma = \emptyset, а не наоборот.

Доказательства суть выводы о выводах: каждая строка утверждает, что нечто выводимо из множества, Γ⊢φ\Gamma \vdash \varphi, и её обоснование ссылается на предшествующие строки. В них «Посылка» отмечает строки, которые формулировка правила принимает как данные, а название аксиомы (A1, A3) или уже доказанной теоремы (например, Тожд, теорема ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi)) отмечает строку Γ⊢φ\Gamma \vdash \varphi, в которой φ\varphi есть частный случай этой схемы или этой теоремы, выводимый из любого множества.

Урок о четырёх приёмах вывода доказал с помощью монотонности и сечения лемму «от результата к правилу», которая делает возможным такой способ работы: если {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta и Γ⊢αi\Gamma \vdash \alpha_{i} для каждого ii, то Γ⊢β\Gamma \vdash \beta. При n=1n = 1, применённая в каждую сторону эквивалентности α⊣⊢α′\alpha \dashv\vdash \alpha', она говорит, что Γ⊢α\Gamma \vdash \alpha тогда и только тогда, когда Γ⊢α′\Gamma \vdash \alpha'. Следовательно, всякое уже доказанное правило и всякая уже доказанная эквивалентность применяются к строкам вывода с посылками: если строка гласит Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi), контрапозиция позволяет записать под ней Γ⊢(¬ψ→¬φ)\Gamma \vdash (\neg\psi \rightarrow \neg\varphi) и обосновать её ссылкой «Контр» и номером строки. Для двух эквивалентных форм из урока о симметриях, которые будут применяться постоянно, пишется «Экв»:

(φ∨ψ)⊣⊢(¬φ→ψ)(φ∧ψ)⊣⊢¬(φ→¬ψ)(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi) \qquad (\varphi \wedge \psi) \dashv\vdash \neg(\varphi \rightarrow \neg\psi)

Следует подчеркнуть, что первая из этих эквивалентностей не является определением; вторая, как показал урок о симметриях, есть тождество цепочек, но на неё ссылаются как на Экв вместе с первой. По определению (φ∨ψ)(\varphi \vee \psi) есть ¬(φ↓ψ)\neg(\varphi \downarrow \psi), а (¬φ→ψ)(\neg\varphi \rightarrow \psi) есть (¬¬φ∨ψ)(\neg\neg\varphi \vee \psi), и это разные цепочки; читать одну как другую «по определению импликации» и есть та ошибка, которой этот урок избегает. «Опр», напротив, оставляется для записи той же цепочки под другим именем, как когда (φ→ψ)(\varphi \rightarrow \psi) читается как (¬φ∨ψ)(\neg\varphi \vee \psi).