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

Формальные дедуктивные системы

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

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

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

  1. Распознавать частные случаи схем A1, A2 и A3 и решать, является ли последовательность формул выводом из множества посылок.
  2. Строить выводы в системе Лукасевича с помощью аксиом, посылок и modus ponens, а также выводы о выводах с помощью рефлексивности, монотонности, сечения, теоремы о дедукции и обратной к ней.
  3. Доказывать структурные свойства выводимости и теорему о дедукции сильной индукцией по числу строк.
  4. Устанавливать доказуемые эквивалентности и пользоваться тем, что доказуемая эквивалентность рефлексивна, симметрична и транзитивна.
  5. Доказывать, что формула невыводима, с помощью разметки, которую сохраняют аксиомы и modus ponens, и объяснять с её помощью предел системы Лукасевича в языке с одной связкой и то, почему нужно второе правило.

Что такое формальная дедуктивная система

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

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

Схемы аксиом и частные случаи

Системы логики высказываний формулируют свои аксиомы не по одной, поскольку их бесконечно много, а с помощью схем: выражений метаязыка, записанных метапеременными, таких как (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)). Схема не есть формула; она есть шаблон. Частный случай схемы есть формула, которая получается, если подставить вместо каждой метапеременной формулу равномерно: вместо всех вхождений одной и той же метапеременной подставляется одна и та же формула, тогда как разные метапеременные могут получить одну и ту же формулу или разные формулы.

ПримерЧастные случаи схемы

При φ:=v1\varphi := v_{1} и ψ:=¬v2\psi := \neg v_{2} схема (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)) даёт частный случай (v1→(¬v2→v1))(v_{1} \rightarrow (\neg v_{2} \rightarrow v_{1})); при φ:=(v1↓v2)\varphi := (v_{1} \downarrow v_{2}) и ψ:=(v1↓v2)\psi := (v_{1} \downarrow v_{2}) она даёт ((v1↓v2)→((v1↓v2)→(v1↓v2)))((v_{1} \downarrow v_{2}) \rightarrow ((v_{1} \downarrow v_{2}) \rightarrow (v_{1} \downarrow v_{2}))), поскольку ничто не мешает двум метапеременным получить одну и ту же формулу. Напротив, (v1→(v2→v3))(v_{1} \rightarrow (v_{2} \rightarrow v_{3})) не является частным случаем этой схемы: первое и последнее вхождения φ\varphi получили бы разные формулы, и подстановка не была бы равномерной. Каждый частный случай после развёртывания сокращений есть цепочка из кружков и дисков; схема же живёт только в метаязыке.