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

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

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

Система Лукасевича из предыдущего урока состоит из трёх схем аксиом и единственного правила, modus ponens; при столь скудных средствах каждый вывод приходится строить от аксиом, и даже формула (φ→φ)(\varphi \rightarrow \varphi) требует пяти строк. Этот урок добавляет четыре приёма, которые доказываются один раз и затем используются повсюду: гипотетический силлогизм, сцепляющий импликации; перестановку посылок, позволяющую менять порядок антецедентов; двойное отрицание, позволяющее ставить и снимать два стоящих подряд отрицания, и контрапозицию в трёх её формах, позволяющую обращать импликацию, отрицая её члены. Каждый приём доказывается полностью, строка за строкой, с помощью трёх аксиом, modus ponens и метатеорем предыдущего урока и получается в трёх видах: как вывод из посылок, как теорема и как правило, применимое при любом множестве посылок. Доказав двойное отрицание, урок дополняет систему вторым исходным правилом, заменой двойного отрицания, которое позволяет ставить или снимать два отрицания в любом месте формулы, в том числе внутри стрелки Пирса, куда три аксиомы не достигают; урок объясняет, почему это правило нужно постулировать, проверяет, что свойства выводимости сохраняются, дополняет теорему о дедукции новым случаем и получает её первые следствия.

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

  1. Преобразовывать результат вида {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta в теорему с помощью теоремы о дедукции и в правило, применимое при любом множестве посылок Γ\Gamma, с помощью монотонности и сечения.
  2. Доказывать гипотетический силлогизм и перестановку посылок как прямым выводом из A1 и A2, так и рассуждением о выводах с теоремой о дедукции, и применять их, чтобы сцеплять импликации и менять в них порядок.
  3. Доказывать оба направления двойного отрицания с помощью A1, A2, A3 и modus ponens и применять их, чтобы ставить или снимать два стоящих подряд отрицания в выводе.
  4. Формулировать правило замены двойного отрицания, находить вхождения подформулы в цепочке базового языка, в том числе скрытые сокращением, и применять это правило в выводах.
  5. Объяснять с помощью разметки, почему замену двойного отрицания нужно постулировать, и доказывать, что свойства выводимости и теорема о дедукции сохраняются в расширенной системе.
  6. Доказывать контрапозицию в трёх её формах и выбирать для импликации с отрицаниями подходящую форму.
  7. Строить нетривиальные выводы, сочетая четыре приёма и новое правило с аксиомами, modus ponens и теоремой о дедукции, и обосновывать каждую строку соответствующим сокращением.

Исходные инструменты

В уроке о формальных дедуктивных системах была задана система Лукасевича. Её язык есть язык кружков и дисков, записанный с официальными сокращениями урока о языке логики высказываний; её аксиомы суть все частные случаи трёх следующих схем, где φ\varphi, ψ\psi и χ\chi обозначают произвольные формулы, а её единственное правило есть modus ponens.

  • 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)).
  • MP: из φ\varphi и (φ→ψ)(\varphi \rightarrow \psi) выводится ψ\psi.

Вывод φ\varphi из множества формул Γ\Gamma есть конечная последовательность формул, которая оканчивается формулой φ\varphi и в которой каждая формула является аксиомой, элементом Γ\Gamma или результатом применения modus ponens к двум предшествующим формулам; если такой вывод существует, пишут Γ⊢φ\Gamma \vdash \varphi, а если Γ\Gamma пусто, пишут ⊢φ\vdash \varphi и говорят, что φ\varphi является теоремой. В том же уроке были доказаны метатеоремы, которыми мы здесь воспользуемся: рефлексивность (Рефл: если φ∈Γ\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), сечение (Сеч: если Γ⊢φi\Gamma \vdash \varphi_{i} для каждого ii от 11 до nn и Γ∪{φ1,…,φn}⊢ψ\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi, то Γ⊢ψ\Gamma \vdash \psi), конечность (если Γ⊢φ\Gamma \vdash \varphi, то достаточно некоторого конечного подмножества Γ\Gamma), теорема о дедукции (ТД: если Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi, то Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi)) и обратная к ней (ОТД), а также теорема ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi), которую в обоснованиях мы будем сокращать как Тожд. Наконец, φ⊣⊢ψ\varphi \dashv\vdash \psi (доказуемая эквивалентность) означает, что {φ}⊢ψ\{\varphi\} \vdash \psi и {ψ}⊢φ\{\psi\} \vdash \varphi.

Стоит напомнить, что ¬\neg и →\rightarrow не являются символами базового языка: это сокращения; ¬φ\neg\varphi есть цепочка (φ↓φ)(\varphi \downarrow \varphi), а (φ→ψ)(\varphi \rightarrow \psi) есть (¬φ∨ψ)(\neg\varphi \vee \psi), то есть ¬(¬φ↓ψ)\neg(\neg\varphi \downarrow \psi). Три аксиомы говорят только об отрицаниях и импликациях, и тот же урок показал с помощью разметки значениями 00 и 11, которую они и modus ponens сохраняют, вытекающий отсюда предел: в системе Лукасевича из (v1↓v2)(v_{1} \downarrow v_{2}) не выводится (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}), и стрелка Пирса отчасти остаётся вне её досягаемости. Поэтому урок действует в два этапа. Вплоть до двойного отрицания включительно ⊢\vdash относится к системе Лукасевича, и ничто из доказанного не зависит от развёртывания сокращений. После доказательства двойного отрицания к системе добавляется второе исходное правило, замена двойного отрицания, которое действует на развёрнутую цепочку; с этого момента ⊢\vdash относится к системе курса, то есть к системе Лукасевича с этим правилом. Поскольку всякий вывод в первой является выводом и во второй, ничто из доказанного ранее не теряется.

Два стиля вывода

Вывод можно записывать двумя способами, и оба будут использоваться. Первый есть собственно вывод, последовательность формул, в которой каждая строка является аксиомой, посылкой или результатом modus ponens; каждая строка обосновывается как A1, A2, A3, Посылка или MP(i,j)(i, j), где строка ii есть антецедент, а строка jj есть импликация, антецедент которой в точности совпадает со строкой ii (а после введения нового правила также ЗДО(i)(i)). Второй есть вывод о выводах, строки которого суть не формулы, а утверждения вида Γ⊢φ\Gamma \vdash \varphi; каждая из них обосновывается уже доказанной метатеоремой, и вся последовательность есть рассуждение метаязыка, гарантирующее, что вывод первого стиля существует, хотя и не выписывающее его. Обоснования второго стиля читаются так.

  • Рефл: формула справа принадлежит множеству слева.
  • A1, A2, A3: формула справа есть частный случай схемы; частный случай аксиомы выводится из любого Γ\Gamma выводом в одну строку.
  • MP(i,j)(i, j): modus ponens для выводов, применённый к строке ii, Γ⊢φ\Gamma \vdash \varphi, и к строке jj, Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi), с одним и тем же Γ\Gamma.
  • ТД(i)(i) и ОТД(i)(i): теорема о дедукции или обратная к ней, применённая к строке ii.
  • Название уже доказанной теоремы, например Тожд или ДО: формула справа есть частный случай этой теоремы и выводится из любого Γ\Gamma по монотонности, поскольку пустое множество содержится в Γ\Gamma.
  • Посылка, в выводе о выводах: строка есть одна из гипотез доказываемого правила.

Каждый результат этого урока формулируется с метапеременными и потому верен для произвольных формул: его доказательство есть схема, и, подставляя в ней вместо каждой метапеременной формулу, получаем другое доказательство, поскольку частные случаи схемы аксиом остаются частными случаями, а каждое применение modus ponens остаётся таковым (то же будет верно для каждого применения нового правила). Так, из ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi) следует ⊢(¬ψ→¬ψ)\vdash (\neg\psi \rightarrow \neg\psi), с ¬ψ\neg\psi вместо φ\varphi. Этот приём, применение результата к формуле более сложной, чем в формулировке, приносит больше всего пользы в дальнейшем.

От результата к правилу

Приёмы этого урока доказываются из фиксированных посылок, например {(φ→ψ),(ψ→χ)}⊢(φ→χ)\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi); но применяются они посреди выводов с другими посылками, где (φ→ψ)(\varphi \rightarrow \psi) и (ψ→χ)(\psi \rightarrow \chi) не посылки, а уже выведенные формулы. Следующая лемма, прямое следствие монотонности и сечения, раз и навсегда разрешает такое применение.

ЛеммаОт результата к правилу

Если {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta, то для всякого множества формул Γ\Gamma из Γ⊢α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)).

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

  1. Γ∪{α1,…,αn}⊢β\dato{mon}{\Gamma \cup \{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta}

    По условию β\beta выводится из формул αi\alpha_{i}. Так как {α1,…,αn}\{\alpha_{1}, \ldots, \alpha_{n}\} содержится в Γ∪{α1,…,αn}\Gamma \cup \{\alpha_{1}, \ldots, \alpha_{n}\}, монотонность позволяет добавить Γ\Gamma к посылкам.

  2. Γ⊢β\Gamma \vdash \resaltar{\beta}

    Если, кроме того, каждая αi\alpha_{i} выводится из Γ\Gamma, сечение устраняет добавленные посылки.

  3. ⊢(α1→(α2→⋯(αn→β)⋯ ))\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots))

    Для вида теоремы теорема о дедукции, применённая nn раз, снимает посылки от последней к первой; каждое применение превращает снятую посылку в антецедент импликации.

Отсюда следует, что каждый приём, доказанный из посылок, имеет три вида: сам результат, теорему, получаемую снятием его посылок, и правило, применяемое при любом Γ\Gamma. В выводе о выводах правило вызывается по названию приёма с номерами строк, к которым оно применяется, например ГС(3,4)(3, 4), и лемма гарантирует законность такого шага.