Мы достигли поворотного момента в нашем изучении логики, так как здесь мы начинаем обзор Формальных Дедуктивных Систем Предикативной Логики. Здесь все, что мы видели до сих пор, начинает работать и проявляется истинный дух логики, потому что мы будем изучать суть доказательств. На этом этапе предполагается, что вы уже знаете, как писать выражения и понимаете, что такое предикативная логика; и если это еще не совсем ясно, рекомендуется пересмотреть предыдущие уроки.

Сделав это, следующим шагом будет рассмотрение того, как выражения предикативной логики связаны друг с другом для формирования вывода. Механизм, с помощью которого строятся эти отношения, — это формальная дедуктивная система.

Что такое Формальная Дедуктивная Система?

Формальные дедуктивные системы, или системы дедуктивного исчисления, имеют три основных элемента:

1. Формальный Язык.
2. Аксиоматическая Схема.
3. Элементарные Правила Вывода.

Мы уже рассмотрели все, что связано с формальными языками. Теперь наша задача — ввести аксиоматические схемы и элементарные правила вывода.

Для построения формальной дедуктивной системы предикативного исчисления мы начнем с Аксиом Лукасевича, и в качестве элементарного правила вывода будем использовать Модус Поненс.

Аксиомы Лукасевича для Предикативной Логики

Если \alpha, \beta и \gamma являются выражениями предикативного исчисления, то следующие являются аксиомами предикативного исчисления:

Модус Поненс: Дедуктивный Двигатель Предикативного Исчисления

Если \alpha и \beta являются действительными выражениями предикативного исчисления, то модус поненс устанавливает, что из \alpha и (\alpha \rightarrow \beta) следует \beta. В форме рассуждения это записывается следующим образом:

Здесь сокращенно представлен модус поненс между шагами (1) и (2) с помощью записи «MP(1,2)», а синтез всего этого представлен следующей нотацией:

Следовательно, \{\alpha, (\alpha \rightarrow \beta)\}\vdash \beta

Вскоре мы увидим, что на основе аксиом Лукасевича и модус поненс можно построить все техники вывода предикативного исчисления, которые синтезируют основные правила обычного рассуждения и служат фундаментом для классической логики.

Рассуждения, Теоремы и Предпосылки

В формальных дедуктивных системах предикативной логики осуществляются рассуждения (или выводы), и они представляют собой любую последовательность выражений, где каждое из них является либо предпосылкой, либо выражением, полученным из предпосылок, используя только аксиомы Лукасевича и модус поненс. Теорема — это результат вывода без предпосылок. Предпосылка может быть любым выражением, которое не является аксиомой и не выводится из них. В общем, когда у нас есть набор предпосылок \Gamma и выражение \alpha, полученное с использованием некоторого элемента \Gamma, аксиом и модус поненс, записывается «\Gamma \vdash \alpha» и говорится, что

из \Gamma выводится \alpha

Если \Gamma представляет собой пустое множество, то вместо записи «\emptyset\vdash \alpha» пишется « \vdash \alpha .» Это читается как «\alpha является теоремой». Этот способ представления теорем может быть расширен для представления аксиом таким образом, что если \alpha, \beta и \gamma являются выражениями, то аксиомы Лукасевича могут быть записаны в форме

Исходя из этого говорится, что аксиомы являются самоочевидными утверждениями, или что теоремы являются выражениями, выводимыми из пустоты, или что аксиомы и теоремы являются свойствами предикативного исчисления.

Как Выполняется Доказательство в Предикативной Логике?

На этом этапе мы перестаем говорить о теории и переходим к практике. И хотя о выполнении доказательства можно сказать многое, но даже если мы понимаем все блестящие идеи о дедуктивных системах и предикативной логике, это еще не означает, что мы развиваем необходимые навыки для выполнения доказательства. Поэтому для обучения способам доказательства мы рассмотрим доказательство простой теоремы.

Теорема

Если \alpha является выражением предикативной логики, то выполняется следующее

\vdash (\alpha\rightarrow \alpha)

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

Следовательно, \vdash (\alpha\rightarrow\alpha)

Как видно, в дедуктивных системах и предикативной логике доказательства не являются тривиальными, но после их построения они легко воспроизводятся.

Теперь, прежде чем мы начнем делать выводы с использованием этих техник, сначала мы разработаем некоторые свойства и определения, которые будут чрезвычайно полезны для этой работы, потому что если мы будем рассуждать только с их помощью, мы столкнемся с серьезными проблемами.

Концепция Доказанного Равенства

Если \alpha и \beta являются любыми выражениями и одновременно выполняется что \{\alpha\}\vdash \beta и \{\beta\} \vdash \alpha, то говорят, что \alpha и \beta доказанно эквивалентны, и это записывается как \alpha \dashv \vdash \beta. Это символически обобщается как:

\left(\{\alpha\}\vdash\beta \wedge \{\beta\}\vdash\alpha \right) \Leftrightarrow \left(\alpha\dashv\vdash\beta\right)

Это читается: из \alpha выводится \beta, и из \beta выводится \alpha, если и только если \alpha и \beta доказанно эквивалентны.

Это мета-свойство предикативной логики

(Мета)Теорема Вывода

Если \alpha и \beta являются выражениями предикативного исчисления, и \Gamma — это набор предпосылок, то считается, что если из \Gamma \cup \{\alpha\} следует \beta, то из \Gamma следует (\alpha \rightarrow \beta). Символически это выражается как:

\left(\Gamma \cup \{\alpha\}\vdash \beta \right) \Rightarrow \left( \Gamma\vdash(\alpha\rightarrow\beta)\right)

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

Для того чтобы выполнялось \Gamma \cup \{\alpha\}\vdash \beta, необходимо иметь вывод следующего вида:

Следовательно, \Gamma\cup\{\alpha\} \vdash \beta

Для того чтобы это было возможно, необходимо, чтобы хотя бы одно из выражений \gamma_1, \cdots \gamma_n,\overline{\gamma_1},\cdots,\overline{\gamma_m} имело форму (\alpha\rightarrow \beta), но все эти строки включают только элементы \Gamma и аксиомы Лукасевича в их выводе, поэтому должно выполняться, что \Gamma\vdash (\alpha \rightarrow \beta). Таким образом, теорема доказана.

Конец доказательства.

Обратная Теорема Вывода

В тех же условиях, что и теорема вывода, считается, что

\left(\Gamma\vdash(\alpha \rightarrow \beta)\right) \Rightarrow \left( \Gamma \cup \{\alpha\}\vdash \beta \right)

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

Если выполняется, что \Gamma\vdash (\alpha\rightarrow \beta), то имеется вывод следующего вида:

Теперь, если мы добавим \alpha как предпосылку к этому рассуждению, то получим следующие строки:

Следовательно, \Gamma \cup \{\alpha\} \vdash \beta

Это и было необходимо доказать.

Конец доказательства.

Выводы о Выражениях и Выводы о Выводах

Доказательства, как те, что были сделаны ранее для достижения результата \vdash (\alpha\rightarrow \alpha), являются случаями выводов на основе выражений, потому что каждый шаг содержит конкретное выражение. Аналогичным образом можно делать выводы на основе других выводов, где каждый шаг является выводом сам по себе. На практике оба этих подхода выполняются аналогично, но второй позволяет нам использовать теорему вывода и её обратную форму, что придаёт большую гибкость технике рассуждений. Чтобы увидеть это, давайте снова докажем, что \vdash (\alpha \rightarrow \alpha), но теперь используя выводы вместо выражений. Одна из возможностей для этого следующая:

Заметим, что этот рассуждение не короче, чем то, которое мы проводили ранее, но оно намного проще в выполнении, так как нам достаточно использовать только теорему вывода, её обратную форму и аксиоматическую схему A1 для построения доказательства.

Казалось бы, в развёрнутом нами рассуждении мы использовали только одну аксиому Лукасевича и забыли как о других аксиомах, так и о модусе поненс. Означает ли это, что мы забыли о других аксиомах и модусе поненс при таком рассуждении? Ответ двоякий. С одной стороны, мы можем действовать, как если бы забыли о некоторых аксиомах и модусе поненс, потому что мы не используем их явно, однако следует помнить, что как теорема вывода, так и её обратная форма являются следствием именно аксиом Лукасевича и модуса поненс, что подразумевает, что при использовании их, как мы это делали в рассуждении, которое мы только что рассмотрели, мы неявно используем их.

Правило Монотонности

Если \tau является теоремой, то, для любого выражения \beta, будет соблюдаться следующее:

\{\beta\}\vdash\tau

На самом деле это правило очень просто доказать, так как если \tau является теоремой, то соблюдается \vdash \tau. Это означает, что существует рассуждение, которое без необходимости добавления предпосылок приводит к выражению \tau, поэтому добавление дополнительного выражения к предпосылкам (пустым) не создаст разницы.

Аналогичным образом можно представить следующий результат: если из множества предпосылок \Gamma делается вывод \gamma, то будет соблюдаться следующее:

\Gamma\cup\{\alpha\}\vdash\gamma

Где \alpha — это любое выражение.

Синтез и Размышления о Дедуктивных Системах и Предикативной Логике

Когда мы предоставляем языку предикативной логики правило вывода и основные выражения: Modus Ponens и аксиомы Лукасевича, то это аналогично созданию «дедуктивной машины» и «двигателя, который обеспечивает ее движение». Отсюда начинают естественным образом появляться все основные правила вывода, которые мы начнем рассматривать в следующих публикациях.

Ещё одна деталь. Выражения предикативной логики на самом деле являются мета-выражениями языка двух символов, который мы видели ранее. Вспомним, что суть этих мета-выражений заключается в том, что они позволяют нам заменять их мета-переменные любым выражением языка, чтобы получить новое, соответствующее такой структуре. Когда мы наделяем язык предикативной логики аксиоматическими схемами и правилами вывода, мы создаем Дедуктивные Системы предикативной логики, позволяющие генерировать выводы, соединяющие выражения. В результате у нас есть дедуктивная схема, способная охватить бесконечное количество выводов: все, которые мы можем получить, заменяя мета-переменные на выражения, которые мы хотим. Сила логики на самом деле раскрывается, когда мы понимаем, что, кроме этих выражений языка двух символов, которые мы использовали в начале, интересно наблюдать, что происходит, когда мы заменяем их обычными выражениями нашего языка, и, как следствие, испытываем восторг.