Реферат: Курс логики: хоть опыт и рискован, Начнут сейчас дрессировать ваш ум, Как бы в сапог испанский зашнурован, Чтоб тихо он без лишних дум

Исчисление высказываний и его свойства


«А потому, мой друг, на первый раз,

По мне, полезен был бы тут для вас

Курс логики: хоть опыт и рискован,

Начнут сейчас дрессировать ваш ум,

Как бы в сапог испанский зашнурован,

Чтоб тихо он без лишних дум

И без пустого нетерпенья,

Всползал по лестнице мышленья.

Чтоб вкривь и вкось, по всем путям,

Он не метался там и сям.»

И.В. Гете, «Фауст»


«Математическая логика издавна

считалась логикой Par excellence»

Э. А. По, Похищенное письмо,1844.)


Введение


Одним из основных инструментов построения математических теорий является аксиоматический метод. Впервые с достаточной последовательностью он был использован в знаменитом сочинении Евклида «Начала» (около 300г. до н. э.) для построения геометрии. Суть аксиоматического метода состоит в том, что некоторые положения конструируемой теории принимаются за основу (эти положения называют аксиомами), а все остальные ее утверждения выводятся из аксиом чисто логическими средствами, без каких-либо апелляций к их очевидности, правдоподобию, подтверждению экспериментом и т. п.

Причины, по которым для построения какой-либо конкретной теории используются те или иные аксиомы, в рамках самой этой теории не обсуждаются. Формально говоря, можно зафиксировать в качестве аксиом произвольный набор утверждений, описать логические средства, которые мы считаем допустимыми, и выводить с их помощью из выбранных аксиом всевозможные следствия – в результате получится некоторая аксиоматическая (или, как еще говорят, формальная) теория.

На практике, конечно, дело обстоит сложнее. Во-первых, неудачный выбор аксиом и правил вывода может привести к тому, что в нашей теории окажутся выводимыми утверждения, которые противоречат друг другу. Представьте себе, например, “арифметику”, в которой “дважды два” равно не только 4, но и 5, 6, 37 и т.д. Ясно, что от такой “науки” (хотя бы при ее построении были соблюдены все формальные требования) проку не будет. Такие теории называют противоречивыми, и, очевидно, внимания заслуживают только теории, противоречивыми не являющиеся, т.е. непротиворечивые. Следует отметить, что в процессе развития математики действительно возникала противоречивая теория, причем эта теория сразу же после своего появления в конце XIX века заняла в математике очень важное, в каком-то смысле центральное положение, – речь идет о теории множеств, с началами которой теперь знакомится каждый школьник. Очень скоро было обнаружено, что в этой теории имеются противоречия. Стремление избавиться от найденных противоречий и застраховаться от возникновения новых оказалось мощным стимулом к развитию математической логики вообще и теории формальных исчислений в частности.

Другая опасность при построении формальных теорий состоит в том, что опять-таки при соблюдении всех формальных правил может получиться “неинтересная” теория, т.е. такая, от которой математике и другим наукам мало пользы. Вывод прост: создавать, предлагать для изучения новые формальные теории – очень ответственная задача, требующая серьезного обдумывания на неформальном, содержательном уровне. Во всяком случае, это занятие отнюдь не для начинающих.

В этом пособии излагается общее определение формального исчисления и более подробно рассматривается исчисление высказываний – простейшее среди т.н. логических исчислений.


^ Общее понятие формального исчисления


Всякое формальное исчисление (далее для краткости будем опускать прилагательное “формальное”) задается своими

языком,

аксиомами и

правилами вывода.

Язык исчисления, в свою очередь определяется своими алфавитом и правилами построения выражений.

Алфавит исчисления есть множество символов, конечное или нет. Сразу отметим, что если имеется намерение рассматривать в строящемся исчислении функции того или иного типа, зависящие от произвольного числа переменных, то алфавит такого исчисления автоматически оказывается бесконечным: его алфавит должен содержать бесконечно много переменных. (Забегая вперед, заметим, что именно так обстоит дело уже с алфавитом исчисления высказываний.)

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

Обычно множество выражений задается индуктивно. Это значит, что, во-первых, задается некоторое сравнительно просто устроенное множество простейших выражений (их часто называют атомными) и, во-вторых, формулируются правила, позволяющие из одного или нескольких уже имеющихся выражений строить новые, более сложные.

Отметим также, что в некоторых исчислениях рассматриваются выражения нескольких различных типов (так обстоит дело, например, в исчислении предикатов, в котором выражения подразделяются на термы и формулы; исчисление предикатов здесь нами подробно не рассматривается). Отметим, что во всяком исчислении выражения одного из рассматриваемых типов – это формулы.

Для всякого “разумно устроенного” исчисления можно построить алгоритм, по произвольному слову в алфавите этого исчисления распознающий, является ли это слово выражением данного исчисления и, если “да”, то к какому типу относится это выражение (последнее, разумеется, имеет смысл, если в нашем исчислении имеются выражения различных типов). В теории алгоритмов (тесно связанной с математической логикой) множество, вопрос о принадлежности элементов к которому решается с помощью соответствующего алгоритма, называют разрешимым. Итак, множество выражений всякого “разумного” исчисления разрешимо.

Мы полностью описали, что представляет собой язык произвольного исчисления.

Некоторые из формул исчисления объявляются его аксиомами. Множество аксиом исчисления может быть как конечным, так и бесконечным.

Наконец, в каждом исчислении задаются правила вывода, множество которых опять-таки может быть как конечным, так и бесконечным. Всякое правило вывода есть функция одного или нескольких переменных, возможными значениями для каждого из которых служат формулы нашего исчисления; значениями самой функции являются все те же формулы. Отметим, что эти функции не обязаны быть всюду определенными (мы столкнемся с такой ситуацией уже в исчислении высказываний). Правила вывода служат для того, чтобы из уже выведенных формул путем применения к ним указанных функций получить новые выводимые формулы.

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

Формальным выводом в данном исчислении называется всякая конечная последовательность

1, 2 ,…, n

его формул, каждая из которых либо является одной из аксиом этого исчисления, либо получается из одной или нескольких формул этой последовательности, предшествующих ей (не обязательно непосредственно), путем применения к ним одного из правил вывода. Вывод 1, 2 ,…, nсчитается выводом своей последней формулы, т.е. n. Формула  называется выводимой в исчислении С, если для нее в этом исчислении имеется вывод. Тот факт, что  выводима в С, изображается метаформулой


 с ;


если из контекста ясно, о каком исчислении С идет речь, будем просто писать:  .

Замечание: в последнем предложении мы вынуждены были употребить термин “метаформула”. Это связано с тем, что в рассматриваемом исчислении С имеются выражения, называемые формулами этого исчисления. Предполагается, что символ  не входит в алфавит исчисления С, и потому запись  с  не может быть его формулой. И это соответствует существу дела, потому что запись  с  говорит о положении формулы  в этом исчислении, т.е. несет информацию, внешнюю по отношению к исчислению.

Приведем теперь простейший пример формального исчисления. Алфавит этого исчисления будет содержать только одну букву a. Его выражениями являются только формулы; формулами служат все слова в выбранном нами алфавите. (Мы говорили, что выражения обычно определяются индуктивно; читателю предлагается придумать некоторые правила, индуктивно порождающие множество W{a} из, например,пустого слова .)

Аксиома в нашем исчислении будет одна – все то же пустое слово . Одно будет и правило вывода:


r (W) = Waa.


Приведем примеры выводов в этом исчислении:

, aa, aaaa;

, aa, , aaaa (встречающееся на 3-м месте слово  “можно исключить” – оно ничуть не помогает вывести формулу aaaa, – но все требования к формальному выводу для этой последовательности выполнены, а никаких требований “минимальности” в этом определении нет);

, , .

В отличие от последовательностей 1) – 3), последовательность из двух формул

, aaaa

не является формальным выводом (хотя формула aaaa является, очевидно, выводимой). Наконец, для построенного нами исчисления нетрудно сформулировать и “критерий выводимости”: слово аn(n символов а подряд) выводимо в нем в точности тогда, когда n четно. Доказательство этого факта предоставляется читателю.

Заключая этот предварительный раздел об устройстве произвольных формальных исчислений, заметим, что построение выводов в них сходно с игрой в некоторые настольные игры, такие, как шахматы, шашки, раскладывание пасьянсов и т.п. Формулы исчисления соответствуют в этой аналогии позициям выбранной игры, правила вывода исчисления – правилам игры (позволяющим переходить от имеющейся позиции к другим). Подобно тому, как в этих играх почти любую позицию можно, следуя правилам, преобразовать несколькими различными способами, так и, перебирая различные продолжения частично построенного вывода, мы вправе применять различные правила вывода.


^ Исчисление высказываний

Это исчисление, конечно, намного сложнее единственного пока рассмотренного нами примера. Для краткости будем далее называть исчисление высказываний ИВ.

Алфавит ИВ бесконечен: он содержит бесконечно много переменных А1, А2, …, Аn,… (называемых иногда пропозициональными), логические связки , ,  и  , а также скобки ( и ).

В ИВ имеются выражения лишь одного типа, называемые формулами. Определение формул дается индуктивно:

всякая переменная есть (атомная) формула;

если 1 и 2 – формулы, то формулами являются также

(1  2), (1  2), (1 2) и  ;

иных формул, кроме определенных в 1) и 2), нет.

(Строго говоря, всякое индуктивное определение должно заканчиваться “ограничительным ” пунктом, подобным нашему 3); однако, именно из-за универсальности этого требования соответствующий пункт обычно опускается.)

Очевидно, что данное определение порождает бесконечное множество формул. Так, формулами ИВ являются

   A3, ((A1   A5 )  A1),

(((A4   A4)  A4)  A4) и т.д.

Убедимся, что множество всех формул ИВ разрешимо, т.е. что существует алгоритм, по произвольному слову в алфавите ИВ выясняющий, является ли это слово формулой. Действительно, однобуквенное слово является формулой в точности тогда, когда его единственная буква – одна из переменных. Если же длина исследуемого слова W больше 1, то W оказывается формулой либо если оно имеет вид  , где Ф – формула, либо представимо в одном из возможных видов

(1  2), (1  2) или (1  2),

где 1 и 2 являются формулами. Сказанное позволяет свести решение задачи, поставленной для одного, возможно, довольно длинного слова, к решению ряда подобных задач для все более коротких слов, что позволяет в конце концов дать ответ на поставленный вопрос.

Прежде, чем формулировать аксиомы ИВ, условимся о некоторых упрощениях в записи формул. Именно, мы позволим себе использовать в качестве переменных буквы А, В, С,… (без индексов), а также договоримся опускать внешние скобки в формулах, где наше определение требует их наличия. С учетом этих соглашений, аксиомами ИВ служат

А1. А  (В  А)

А2. (А  (В  С))  ((А В)  (А  С))

А3. (А  В)  А

А4. (А  В)  В

А5. (А  В)  ((А  С)  (А  (В  С)))

А6. А  (А  В)

А7. В  (А  В)

А8. (А  С)  ((В  С)  ((А  В)  С))

А9. А    А

А10.   А  А

А11. (А  В)  ( В   А).

С точки зрения удобства запоминания полезно все эти аксиомы разбить на 4 группы. Первую из них образуют аксиомы А1 и А2, в которые из логических связок входит только импликация , и потому эту группу называют группой импликации. Вторую (группу конъюнкции) образуют аксиомы А3, А4 и А5, содержащие, помимо , еще и  (конъюнкцию). Третья группа (дизъюнкции,  ) состоит из аксиом А6, А7 и А8. Стоит отметить “отраженное подобие” соответствующих аксиом из последних двух групп; их сходство влечет различные утверждения об одновременной выводимости сходным образом устроенных формул. Наконец, аксиомы А9 – А11 образуют группу отрицания ( ).

Правил вывода в ИВ имеется два. Первое из них, называемое правилом заключения или modus ponens (сокращенно mod pon) дает по паре формул Ф и Ф  Ψ формулу Ψ, или, в функциональных обозначениях,

R1 (Ф, Ф  Ψ) = Ψ.

Таким образом, mod pon – это функция двух переменных, причем определенная не всюду, а только для пар формул, очевидным образом согласованных друг с другом.

Второе из правил вывода – это правило подстановки. Операция подстановки Ψ естественно определяется для произвольных слов. Итак, пусть Ф и Ψ – слова в некотором алфавите А, а x – буква того же алфавита. Результатом подстановки слова Ψ вместо буквы х в слово Ф, обозначаемым SхΨ Ф, называют слово, получающееся из Ф в результате замены каждого вхождения в него буквы х на слово Ψ. Например,

Sлжирофл леля = жирофлежирофля.

(Отметим на всякий случай, что все вхождения символа х в Ф заменяются на Ψ, так сказать, “одновременно”: дело в том, что в слове Ψ тоже могут содержаться вхождения буквы х, но эти новые вхождения на Ψ уже не заменяются!)

Пусть теперь Ф и Ψ – формулы ИВ, а А – некоторая его переменная. Тогда правило подстановки r2 формулируется так:

r2 (Ф) = SАФ.

Очевидно, что это – “параметрическое” правило; иными словами, имеется целое семейство правил подстановки, зависящее от двух параметров, переменной А и формулы Ψ. Применять можно любое из них.

Замечания:

1. Мы оставляем без доказательства тот факт, что если Ф и Ψ – формулы ИВ, то и SАФ является формулой. Читатель, не готовый принять это утверждение на веру, может доказать его самостоятельно.

2. Подчеркнем, что формулы Ф и Ψ, участвующие в определении правила подстановки, по-разному связаны с выводом, в котором это правило применяется: формула Ф должна была появиться в этом выводе до применения правила подстановки, в то время как формула Ψ является произвольной и могла до этого в нашем выводе не появляться.

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

Пример формального вывода в ИВ

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

Ф1: А  (В  А) (акс. А1)

Ф2: (А  (В  С))  ((А  В)  (А  С))) (акс. А2)

Ф3: (А  (В  А))  ((А  В)  (А  А))) (SСА Ф2)

Ф4: (А  В)  (А А) (r1 (Ф1, Ф3))

Ф5: (А  (В  А))  (А А) (SВВА Ф4)

Ф6: А  А (r1 (Ф1, Ф5))


Согласно данным определениям, наш вывод является выводом формулы А А. Построив этот вывод, мы доказали, что

 ИВ (А  А).

Отсюда немедленно следует, что, какова бы ни была формула  в ИВ,

 ИВ (Ψ  Ψ)

(достаточно только что построенный вывод дополнить еще одним применением правила подстановки).

Отметим некоторые свойства выводов (их доказательства представляются очевидными). Хотя мы формулируем их в разделе, посвященном ИВ, они справедливы для любого формального исчисления.

Всякий вывод открывается одной из аксиом.

Начальный отрезок всякого вывода является выводом. т.е., если

Ф1, Ф2, …, Фк, …, Фn –

вывод, то и

Ф1, Ф2, …, Фк –

тоже вывод.

3. Если

Ф1, Ф2, …, Фn, и Ψ1, Ψ2, …, Ψm –

выводы, то и последовательность

Ф1, Ф2, …, Фn, Ψ1, Ψ2, …, Ψm –

тоже вывод.

4. Свойство 3 говорит, что, приписав один вывод за другим, мы получим снова вывод. Это утверждение можно обобщить: пусть Ф1, …, Фnи 1, …, m– выводы; тогда всякая последовательность

X1, X2, …, Xm+n,

для которой из того, что

Xi = Фi´, Xj´ = Фj´, i< j, или

Xi = Ψi´, Xj = Ψj´, i < j,

следует, что i´ < j´, сама является выводом.

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

Итак, пусть дана последовательность формул ИВ

Ф1, Ф2, …, Фn.

Будем последовательно исследовать ее начальные отрезки.

Чтобы данная последовательность была формальным выводом, начальная формула Ф1 должна быть одной из аксиом. Это выясняется путем непосредственного сравнения формулы Ф1 с аксиомами А1 – А11.

Пусть мы уже убедились, что начальный отрезок

Ф1, …, Фк

является выводом. Его продолжение

Ф1, …, Фк , Фк+1

является выводом в точности тогда, когда формула Фк+1 либо является одной из аксиом (о проверяемости этого условия уже сказано), либо получается из формул с меньшими номерами путем применения либо modus ponens, либо правила подстановки. С правилом modus ponens все просто: чтобы Фк+1 получалась с его помощью, в нашей последовательности должны существовать такие ФiиФj, что i, j ≤ k и Фj= Фi→Фк+1. Это условие, очевидно, проверяемо. Что же касается правила подстановки, то следует помнить, что это правило зависит от параметров А и Ψ, каждый из которых может принимать бесконечно много значений. Поэтому перебрать все возможные сочетания А и Ψ невозможно. Однако, оказывается, что можно ограничиться перебором лишь конечного числа возможностей. Действительно, если

 i ≤ к Фк+1 ≠Фi,

то, исследуя возможность получения формулы Фк+1 изФiс помощью правила подстановки, достаточно рассмотреть лишь те пары А, Ψ, для которых

переменная А входит в Фi,

каждая из переменных формулы Ψ входит в формулу Фк+1,

формула Ψ достаточно коротка для того, чтобы длина слова SАФiне превосходило длину слова Фк+1 (длиною слова мы называем, естественно, общее число букв в нем).

Но таких пар имеется лишь конечное множество, и, значит, требуемая проверка осуществима. Таким образом, мы доказали, что множество всех формальных выводов ИВ разрешимо (в множестве всех конечных последовательностей его формул).

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

В рамках только что изложенного алгоритма распознавания формальных выводов мы вынуждены были решать, можно ли ту или иную формулу получить из предшествующих ей по правилу подстановки или по правилу modus ponens. Но, может быть, какое – либо из этих правил является излишним, и на самом деле любую формулу, выводимую в ИВ, можно вывести, используя одни только подстановки (или, наоборот, применяя только modus ponens)? Будь это так, мы могли бы соответственно упростить и алгоритм распознавания выводов.

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

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

Рассмотрим сначала вопрос о применении modus ponens. Это правило, в отличие от правила подстановки, является «укорачивающим»: формула , получаемая с его помощью, короче, чем формула  (читатели, конечно, помнят, что для применения modus ponens нужна еще и формула ). Поэтому, вывод всякой формулы, длина которой меньше длин всех аксиом ИВ, неизбежно должен хотя бы однократно использовать это правило. Но такова уже формула А  А, вывод которой построен нами выше.

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

Подобным образом, нельзя обойтись и без правила подстановки. Это правило, наоборот, является, в понятном смысле, «удлинняющим» (точнее «неукорачивающим»). Чтобы убедиться в его неустранимости, нам, напротив, потребуется «очень длинная» выводимая формула. Но такова, например, формула

Фn = A  (A(A(A … A) … ))),

содержащая дизъюнкцию с n вхождениями переменной А (докажите, что  Фnпри всякомn). Если n достаточно велико, то Фnдлиннее всех аксиом ИВ, и поэтому ее вывод требует применения правила подстановки.

Итак, правила вывода ИВ независимы в том смысле, что отказ от любого из них приводит к уменьшению множества выводимых формул. Можно в том же смысле ставить вопрос и о независимости аксиом ИВ (как впрочем, и для любого другого формального исчисления). Известно, что аксиомы А1-А11 независимы; полученное доказательство этого факта содержится в книге П.С. Новикова [2].

Наконец, с только что рассмотренным вопросом об алгоритмическом распознавании формальных выводов связаны два других:

Существует ли алгоритм, по произвольной формуле исчисления высказываний распознающий, выводима ли эта формула?

Можно ли по произвольной формуле ИВ, про которую известно, что она выводима, эффективно (т.е. опять-таки с помощью некоторого алгоритма) найти ее вывод?

Располагая лишь теми сведениями об ИВ, которые изложены выше, дать ответ на первый вопрос невозможно. Действительно, мы умеем по произвольной последовательности формул ИВ решать, является ли она выводом. Мы легко поймем, выводом какой формулы (ясное дело, последней) является тот или иной вывод. Нетрудно представить себе, что мы можем последовательно выписывать все выводы на свете: придумаем какой-нибудь способ упорядочить все конечные последовательности формул ИВ и будем выписывать одну за другой лишь те из них, которые являются формальными выводами. Если данная нам формула Ф выводима, то мы рано или поздно доберемся до ее вывода (точнее, до одного из ее выводов: всякая выводимая формула может быть выведена многими способами! ) и поймем, что Ф выводима. Но если Ф не выводима, как обнаружить это? Ответить на этот вопрос наша процедура не позволяет. (Забегая вперед, заметим, что алгоритм распознавания выводимости формул существует, но построен он (см. ниже) на совсем иных соображениях.)

Что же до второго вопроса, то с помощью процедуры эффективного перебора всех формальных выводов в ИВ легко дать на этот вопрос положительный ответ: перебирай их один за другим и дожидайся, пока появиться вывод данной формулы Ф. Более того, ясно, что с помощью этой процедуры можно эффективно одну за другой порождать все выводимые формулы ИВ. Множества, все элементы которых можно порождать с помощью некоторой эффективной процедуры, называют перечислимыми. Итак, множество всех выводимых в ИВ формул перечислимо.

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

Приведем еще один пример формального вывода в ИВ и рассмотрим затем некоторые возможности рационализации построения таких выводов.

Выведем, например, формулу

(АВ) → (ВА)

Ее вывод таков:

Ф1: (А → С) → ((В → С) → ((АВ) → С)) (А8)

Ф2: (А → (ВА)) → ((В → (ВА)) → ((АВ) → (ВА))) (SСВА Ф1)

Ф3: В → (АВ) (А7)

Ф4: В → (СВ) (SАС Ф3)

Ф5: А → (СА) (SВА Ф4)

Ф6: А → (ВА) (SСВ Ф5)

Ф7: (В → (ВА)) → ((АВ) → (ВА)) (r1 (Ф6, Ф2))

Ф8: А → (АВ) (А6)

Ф9: А → (АС) (SВС Ф8)

Ф10: В → (ВС) (SАВ Ф9)

Ф11: В → (ВА) (SСА Ф10)

Ф12: (АВ) → (ВА) (r1 (Ф11, Ф7))

Задумаемся теперь, как можно “усовершенствовать” наше ИВ, чтобы строить выводы в нем стало легче. При этом мы, естественно, не будем менять его язык и потребуем, чтобы неизменным осталось и множество выводимых формул. Таким образом, изменения могут касаться только множеств аксиом и правил вывода. Очевидно, что добавляя к уже имеющимся новые аксиомы и правила вывода, мы расширим “дедуктивные возможности” системы: строить выводы станет легче.

Ответ на вопрос о том, какие новые аксиомы можно присоединить к исходным А1 – А11, не меняя при этом запас выводимых формул, очевиден: мы можем с этой целью присоединять к А1 – А11 любое число выводимых формул (действительно, помещая перед каждой новой аксиомой ее вывод в исходном исчислении высказываний, мы перестроим любой вывод в исчислении с расширенной аксиоматикой в формальный вывод в рамках исходного ИВ).

Подумаем теперь, какими новыми правилами вывода можно обогатить наше исчисление, по-прежнему следя за неизменностью множества выводимых формул; такие правила вывода называют производными. Здесь нет такого очевидного ответа, как в случае аксиом; каждый отдельный пример требует специального рассмотрения.

Разберем лишь один конкретный пример – т.н. правило одновременной подстановки. С полезностью такого правила мы, можно сказать, столкнулись, рассматривая недавно вывод формулы (АВ) → (ВА). В том выводе “четырехформульные фрагменты” Ф3 – Ф6 и Ф8 – Ф11 потребовались нам, чтобы в каждой из аксиом В → (АВ) и А → (АВ), соответственно, поменять местами входящие в них переменные. Назовем, вообще, результатом одновременной подстановки формул Ψ1, …, Ψк вместо переменных А1, …, Ак в формулу Ф (и будем обозначать его

SА1, …, Ак Ψ 1, …Ψ к Ф)

формулу, получающуюся из Ф, если каждое вхождение переменной А1 в Ф заменить на Ψ1,…,каждое вхождение Ак заменить на Ψк –и сделать это одновременно,так что новые вхождения тех же переменных А1, …, Ак, которые могут содержаться в Ψ1, …, Ψк,повторным заменам уже не подвергаются. Например,

SА, ВВ, А (А → (АВ)) = В → (ВА).
^ Следует иметь в виду, что равенство
SА1, А2 Ψ 1, Ψ 2 Ф = SА2Ψ 2 (SА1Ψ1 Ф)

может, вообще говоря, и не выполняться.

В частности,

SА, ВВ, А (А → (АВ)) ≠ S В А (SА В (А → (АВ))):

действительно,

SАВ (А → (А→ В)) = В → (ВВ))

и никакими дальнейшими подстановками одно только последнее вхождение В не превратить в А. Фактически, в нашем выводе Ф1 – Ф12 показано, как обходить это препятствие: следует сначала с помощью нескольких обычных подстановок заменить все (или хотя бы некоторые, как сделано в рассмотренном выводе) переменные А1, …, Ак на совершенно новые переменные С1, …, Ск , не входящие ни в Ф, ни в Ψ1, …, Ψк , а затем уже обычными же подстановками последовательно заменять С1, …, Ск на Ψ 1, …, Ψк. Тем самым показано, что правило одновременной подстановки является производным для ИВ.

С расширением дедуктивных возможностей ИВ связана и т.н. теорема дедукции и используемое в ней понятие вывода из гипотез.

Определение. Выводом из гипотез Ψ1, …, Ψк в ИВ называется всякая конечная последовательность

Ф1, …, Фn

его формул, в которой каждая формула

1) либо является выводимой в ИВ,

2) либо является одной из гипотез,

3) либо получается из двух предшествующих формул путем применения к ним правила modus ponens.

Замысел этого определения очевиден: допустить использование гипотез наравне с аксиомами при построении формальных выводов. С подобным использованием гипотез в реальной математической практике мы сталкиваемся по ходу доказательств от противного и по индукции.

Однако, это определение двумя обстоятельствами отличается от исходного определения формального вывода: в выводах из гипотез разрешается использовать лишь modus ponens (подстановки запрещены), зато можно без дополнительных обоснований вводить в рассуждение не только аксиомы, но и любые формулы, выводимые в ИВ. Первое сделано для того, чтобы принимая за гипотезу, например, какую-нибудь конкретную переменную, скажем, А (а вовсе не В, С и т.д.) не получить в качестве выводимых из нее все формулы ИВ (допущение правила подстановки неизбежно привело бы к этому!) Но, допустив применение к аксиомам и гипотезам только правила modus ponens, мы не смогли бы вывести даже все формулы, выводимые в ИВ в отсутствие каких-либо гипотез. Чтобы избежать этой неприятности, разрешено использовать в выводах из гипотез не только аксиомы, но любые выводимые в ИВ формулы.

Тот факт, что формула Ф выводится из гипотез Ψ 1, …, Ψк ,будем изображать метаформулой

Ψ1, …, Ψк Ф.
^ Теперь формула
 Ф

может использоваться двояко:

1) Ф выводима в ИВ (в первоначальном смысле),

2) Ф выводима из пустого множества гипотез.

По счастью, утверждения 1) и 2) равносильны (докажите это!), так что никакой путаницы не возникает.

Приведем, наконец, пример вывода из гипотез. Покажем, например, что

А, В, А → (В → С)  С

Действительно,

Ф1: А (гипотеза)

Ф2: А → (В → С) (гипотеза)

Ф3: В → С (r1 (Ф1, Ф2))

Ф4: В (гипотеза)

Ф5: С (r1 (Ф4, Ф3)) –

требуемый вывод.

Легко видеть, что если

Ψ1, …, Ψn-1  (Ψn→ Ф),

то

Ψ1, …, Ψn-1, Ψn Ф

(достаточно одного применения modus ponens).

Обратное утверждение известно как Теорема дедукции: если

Ψ1, …, Ψn-1, ΨnФ,

то

Ψ1, …, Ψn-1  (Ψn→ Ф).

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

Доказательство теоремы состоит в том, что вывод формулы Ф из гипотез Ψ1, …, Ψnперерабатывается в вывод импликации Ψn→ Ф из уменьшенного набора гипотез; оно проводится индукцией по длине исходного вывода.
^ Итак, пусть
Ф1, …, Фm–

вывод формулы Ф (так что Фm= Ф) из гипотез Ψ1, …, Ψn.Как всегда при использовании индукции, сначала рассмотрим случай m = 1.

В этом случае формула Ф стоит первой в имеющимся выводе и потому является либо одной из гипотез, либо выводимой в ИВ формулой. Возможны следующие ситуации:

1) Ф = Ψn, так что

(Ψn→ Ф) = ( Ф→ Ф).

Но эта формула получается очевидной подстановкой из выводимой в ИВ формулы

А→ А,

а потому и сама выводима в ИВ. Любая же выводимая (без гипотез!) формула может занимать любое место в выводе из любого множества гипотез. Поэтому “последовательность”

Ψn→ Ф

(состоящая всего из одной формулы ) есть вывод этой формулы из гипотез Ψ1, …, Ψn-1.


2) Ф = Ψk, k ≤ n-1, так что (Ψn→ Ф) = (Ψn→ Ψk).

Выводом этой формулы из гипотез Ψ1, …, Ψn-1 служит следующая последовательность формул:

1. Ψк (гипотеза)

2. Ψк → ( Ψn→ Ψк),(выводимая в ИВ формула: она получается одновременной подстановкой в аксиому А1)

3. Ψn→ Ψk(применили modus ponens к предшествующим формулам).

3) Пусть теперь Ф – формула, выводимая в ИВ, т.е.  Ф. Тогда вывод формулы Ψn→ Ф из гипотез Ψ1, …,Ψn-1 имеет вид:

1. Ф

2. Ф → (Ψn→ Ф)

3. Ψn→ Ф.

(Обоснование «законности» присутствия этих трех формул на своих местах предоставляется читателю.)

Мы построили вывод формулы Ψn→ Ф для всех случаев, возможных при m = 1. Поэтому можно перейти к т. н. индуктивному шагу, т.е. предполагая, что доказываемое утверждение верно для всех формул, для которых длина их вывода из гипотез Ψ1 , …,Ψnне превосходит числа m, распространить его на формулы, длина вывода которых из тех же гипотез равна m + 1. Итак, пусть

Ф1, …, Фm, Фm+1 –

вывод формулы Ф (теперь Фm+1 = Ф) из гипотез Ψ1, …, Ψn . Тогда Ф

либо является одной из гипотез,

либо выводима в ИВ (без всяких гипотез),

либо получается из формул Фi и Фj,

где i, j ≤ m, путем применения к ним правила modus ponens. Во всех этих случаях, кроме последнего, перестройка имеющегося вывода в требуемый происходит точно так же, как в рассмотренном выше случае m = 1 (заметим также, что в этих же случаях формула Ф обладает выводом из гипотез Ψ1, …, Ψn,длина которого равна 1: все формулы Ф1, …, Фmиз данного вывода можно удалить!).

Остается рассмотреть лишь ситуацию 3), когда Ф получается с помощью modus ponens из Фi и Фj . В этом случае, поскольку i, j, ≤ m, для формул Фi и Фj действует предположение индукции, т. е. мы можем утверждать, что

Ψ1, …, Ψn-1 