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

Вид материала

Документы

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

Подобный материал:

• Сказка валенок, Сапог и Туфелька, 17.55kb.
• Я знал, что ты у меня умничка, сказал Джордан, и поцеловал возлюбленную, 77.65kb.
• Сейчас не лучшее время писать о Тимуре Новикове, ихи и так хватает, 208.74kb.
• Из сочинений Владимира Владимировича Маяковского (1893-1930), 13.95kb.
• Великий Декоратор, 337.79kb.
• Том не мучаться с переездами, с упаковкой и распаковкой чемоданов, не платить лишних, 200.65kb.
• Моя деревня Сейчас тихо, в этот поздний декабрьский вечер, все сидят по своим хатам, 64.2kb.
• Решили поменять свое авто на более новое или просто продать? Конечно же, нормальным, 68.13kb.
• И станет живою "мертвая" вода, 836.9kb.
• Жажда приключений… Амстердам и Париж Львов- берлин – Амстердам- дельфт –Гаага- схевиненген-, 387.37kb.

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


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

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

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

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

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

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

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

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

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

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

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


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

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

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

Введение

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

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

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

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

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

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

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

1. языком,
   
2. аксиомами и
   
3. правилами вывода.
   

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

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

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

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

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

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

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

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

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

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

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

₁, ₂ ,…, _n

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


 _с ;


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

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

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

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


r (W) = Waa.


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

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

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

, aaaa

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

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

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

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

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

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

1. всякая переменная есть (атомная) формула;
   
2. если ₁ и ₂ – формулы, то формулами являются также
   

(₁  ₂), (₁  ₂), (₁ ₂) и  ;

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

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

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

   A₃, ((A₁   A₅ )  A₁),

((( A₄   A₄)  A₄)  A₄) и т.д.

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

(₁  ₂), (₁  ₂) или (₁  ₂),

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

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

А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) дает по паре формул Ф и Ф  Ψ формулу Ψ, или, в функциональных обозначениях,

R₁ (Ф, Ф  Ψ) = Ψ.

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

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

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

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

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

r₂ (Ф) = S^А_ Ф.

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

Замечания:

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

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

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

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

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

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

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

Ф3: (А  (В  А))  ((А  В)  (А  А))) (S^С_А Ф₂)

Ф4: (А  В)  (А А) (r₁ (Ф₁, Ф₃))

Ф5: (А  (В  А))  (А А) (S^В_ВА Ф₄)

Ф6: А  А (r₁ (Ф₁, Ф₅))


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

 _ИВ (А  А).

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

 _ИВ (Ψ  Ψ)

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

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

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

Ф₁, Ф₂, …, Ф_к, …, Ф_n –

вывод, то и

Ф₁, Ф₂, …, Ф_к –

тоже вывод.

3. Если

Ф₁, Ф₂, …, Ф_n, и Ψ₁, Ψ₂, …, Ψ _m –

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

Ф₁, Ф₂, …, Ф_n, Ψ₁, Ψ₂, …, Ψ_m –

тоже вывод.

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

X₁, X₂, …, X_m+n,

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

X_i = Ф_i´, X_j´ = Ф_j´, i < j, или

X_i = Ψ_i´, X_j = Ψ_j´, i < j,

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

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

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

Ф₁, Ф₂, …, Ф_n .

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

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

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

Ф₁, …, Ф_к

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

Ф₁, …, Ф_{к ,} Ф_к+1

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

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

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

1. переменная А входит в Ф_i,
   
2. каждая из переменных формулы Ψ входит в формулу Ф_к+1,
   
3. формула Ψ достаточно коротка для того, чтобы длина слова 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. Существует ли алгоритм, по произвольной формуле исчисления высказываний распознающий, выводима ли эта формула?
   
2. Можно ли по произвольной формуле ИВ, про которую известно, что она выводима, эффективно (т.е. опять-таки с помощью некоторого алгоритма) найти ее вывод?
   

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

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

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

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

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

(АВ) → (ВА)

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

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

Ф2: (А → (ВА)) → ((В → (ВА)) → ((АВ) → (ВА))) (S^С_ВА Ф₁)

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

Ф4: В → (СВ) (S^А_С Ф₃)

Ф5: А → (СА) (S^В_А Ф₄)

Ф6: А → (ВА) (S^С_В Ф₅)

Ф7: (В → (ВА)) → ((АВ) → (ВА)) (r₁ (Ф₆, Ф₂))

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

Ф9: А → (АС) (S^В_С Ф₈)

Ф10: В → (ВС) (S^А_В Ф₉)

Ф11: В → (ВА) (S^С_А Ф₁₀)

Ф12: (АВ) → (ВА) (r₁ (Ф₁₁, Ф₇))

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

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

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

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

S^{А1, …, Ак} _{Ψ 1, … Ψ к} Ф)

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

S^{А, В}_{В, А} (А → (АВ)) = В → (ВА).

Следует иметь в виду, что равенство

S^{А1, А2} _{Ψ 1, Ψ 2} Ф = S^А2 _{Ψ 2} (S^А1 _{Ψ 1} Ф)

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

В частности,

S^{А, В}_{В, А} (А → (АВ)) ≠ S ^В _А ( S^А _В (А → (АВ))):

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

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

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

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

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

Ф₁, …, Ф _n

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

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

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

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

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

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

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

Ψ₁, …, Ψ_к  Ф.

Теперь формула

 Ф

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

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

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

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

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

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

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

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

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

Ф3: В → С (r₁ (Ф1, Ф2))

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

Ф5: С (r₁ (Ф4, Ф3)) –

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

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

Ψ₁, …, Ψ_n-1  (Ψ_n → Ф),

то

Ψ₁, …, Ψ _n-1, Ψ_n  Ф

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

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

Ψ₁, …, Ψ_n-1, Ψ_n  Ф,

то

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

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

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

Итак, пусть

Ф₁, …, Ф_m –

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

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

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

(Ψ _n → Ф) = ( Ф → Ф).

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

А → А,

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

Ψ_n → Ф

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


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

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

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

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

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

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

1. Ф

2. Ф → (Ψ_n → Ф)

3. Ψ_n → Ф.

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

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

Ф₁, …, Ф _m , Ф_m+1 –

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

1. либо является одной из гипотез,
   
2. либо выводима в ИВ (без всяких гипотез),
   
3. либо получается из формул Ф_i и Ф_j ,
   

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

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

Ψ₁, …, Ψ_n-1  (Ψ_n → Ф_i),

Ψ₁, …, Ψ_n-1  (Ψ_n → Ф_j).

С другой стороны, раз Ф получается из Ф_i и Ф_j с помощью modus ponens , значит, эти три формулы должны быть соответствующим образом согласованы друг с другом, например,

Ф_j = Ф_i → Ф.

Построим теперь вывод формулы Ψ_n → Ф из гипотез Ψ₁, …, Ψ_n-1. Используем для этого (существующие по предположению индукции) выводы из гипотез Ψ₁, …, Ψ_n-1

Ф_1, Ф_{2, … ,} Ф_к = Ψ_n → Ф_i и

Ф″₁, Ф"_{2, … ,} Ф"_l = Ψ_n →Ф_j = Ψ_n → (Ф_i → Ф).

Поместим их один за другим, т. е. построим последовательность


Х_{1, … ,} Х_к , Х_к+1, … , Х_к+l,

где




Как и в случае “абсолютных” (без гипотез) выводов, эта последовательность также является выводом из гипотез Ψ₁, …, Ψ_n-1. Дополним теперь ее еще формулами:

Х_к+l+1 = (Ψ_n→ (Ф_i → Ф)) → (( Ψ_n → Ф_i) → ( Ψ_n → Ф))

(  Х_к+l+1: она получается из аксиомы А2 очевидной одновременной подстановкой)


Х_к+l+2 = (Ψ_n→ Ф_i) →( Ψ_n → Ф) (Х_к+l+2 = r₁(Х_{к+l ,} Х_к+l+1 ))


Х_к+l+3 = Ψ_n→ Ф (Х_к+l+3 = r₁(Х_{к ,} Х_к+l+2 )).


Формулы


Х₁, …, Х_к , Х_к+1, …, Х_к+l, …, Х_к+l+3

и образуют вывод формулы Ψ_n → Ф из гипотез Ψ₁, …, Ψ_n-1. Теорема дедукции доказана.

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

Следствие теоремы дедукции: если

Ψ₁, … , Ψ_n-2, Ψ_n-1, Ψ_n  Ф,

то

Ψ₁, … , Ψ_n-2  Ψ_n-1 → (Ψ_n → Ф)),

. . . . . . . . .

 Ψ₁ → (Ψ₂ → (… → (Ψ_n → Ф)…))).

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

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

Примеры:

1. Докажем, что
   

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

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

А → В, В → С и А.

Вывод формулы С из этих гипотез получается очень просто:

1. А
   
2. А → В
   
3. В (modus ponens)
   
4. В → С
   
5. С (modus ponens)
   

Итак,

А → В, В → С, А  С.

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

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

и т. п.

Формула

(А → В) → ((В → С) → (А → С)) (*),

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

 (А  В) → (А  В).

Применяя к формуле (*) очевидную одновременную подстановку, получим

 ((А  В) → А) → (А → (А  В) → ((А  В) → (А  В)).

Выпишем вслед за этой формулой аксиомы

А  В → А и

А → А  В,

применим дважды к последним трем формулам правило modus ponens, и требуемый вывод (точнее, его набросок) готов!

Наконец, формулу (*) можно «превратить» в новое правило вывода

r₃ (А → В, В → С) = А → С.

Из сказанного выше с очевидностью следует, что правило r₃ является производным для нашего ИВ.

2) Во втором из наших примеров, так сказать, явным образом фиксируется возможность перестановки посылок в сложных импликациях:

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

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

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

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

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

Тем не менее, такой алгоритм существует, и вскоре мы его сформулируем. Он основан на интерпретации логических связок , , → и , используемых в ИВ, в качестве булевых функций. Напомним связанные с этим факты.

Поставим в соответствие каждой из указанных связок некоторую булеву функцию, т. е. функцию, аргументы которой, ровно как и она сама, могут принимать значения 0 или 1. Отрицанию , естественно, соответствует функция одного переменного, а остальным связкам , , → соответствуют функции двух переменных. Как всякую функцию, определенную на конечном множестве и принимающую конечное число значений, каждую из наших булевых функций можно задать таблицей ее значений. Приведем эти таблицы:

А	A
0	1
1	0

А	В	АВ	АВ	А→В
0	0	0	0	1
0	1	0	1	1
1	0	0	1	0
1	1	1	1	1

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

Ф = ((А  В) → А)  В

Имеем

Ф₁ = А  В,

Ф₂ = А,

Ф₃ = Ф₁ → Ф₂,

Ф = Ф₃  В

и, последовательно вычисляя значения этих функций, получим

А	В	Ф1	Ф2	Ф3	Ф
0	0	0	1	1	1
0	1	0	1	1	1
1	0	0	0	1	1
1	1	1	0	0	1

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

Теорема (критерий выводимости для ИВ):

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

Мы здесь докажем лишь, что выводимость формулы влечет за собой ее тавтологичность. Доказательство обратного утверждения требует большего объема довольно рутинной работы и потому нами опускается. Интересующийся читатель может найти его в книге П.С. Новикова [2].

Итак, пусть ├ Ф; доказательство того факта, что Ф ≡ 1, будем проводить индукцией по длине вывода формулы Ф.

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

Предположим теперь, что доказываемое утверждение справедливо для всех формул, обладающих выводом, длина которого не более n, и докажем его для формул Ф, имеющих вывод длиною n + 1. Если Ф – одна из аксиом, то о ее тавтологичности нам уже известно. В противном случае Ф получается либо по правилу подстановки, либо с помощью modus ponens. Рассмотрим эти случаи.

Итак, возможно

Ф = S^A _Ψ Ф,

причем формула Ф предшествует формуле Ф в выводе последней, а потому для Ф существует вывод, длина которого не превосходит n. Предположение индукции гарантирует нам, что Ф является тавтологией. Но тогда тавтологична и формула Ф, потому что формула Ψ, подставляемая в Ф вместо переменной А, может принимать только те же значения, 0 или 1, что и А, а Ф для любых сочетаний любого из этих значений с любыми значениями остальных переменных обращается в 1.

Пусть, наконец, Ф получается по правилу mod. pon. из формул Ψ₁ и Ψ₂, каждая из которых встречается в выводе формулы Ф и. значит, сами они обладают выводами длиною не более n. Значит, Ψ₁ и Ψ ₂ – тавтологии. Кроме того, имеем

Ψ₂ = Ψ₁ → Ф.

Если Ф не является тавтологией, то Ф должна обратиться в 0 на некотором наборе значений (всех переменных, входящих в Ψ₁ и Ψ₂). Но Ψ₁, будучи тавтологией, равно 1 и на этом наборе. Вычисляя на этом наборе значение импликации Ψ ₁ → Ф, получаем (согласно таблице значений функции →) 0 – а это противоречит тавтологичности Ψ₂. Тем самым утверждение

├ Ф Ф ≡ 1

окончательно доказано.

Критерий выводимости имеет два важных следствия.

Следствие 1: существует алгоритм, по произвольной формуле ИВ выясняющий, выводима ли она в ИВ.

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

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

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

Определение 1: формальное исчисление называется 1-непротиворечивым, если в нем выводимы не все формулы этого исчисления.

Определение 2: формальное исчисление, алфавит которого содержит символ и в котором для всякой формулы Ф формулой является и Ф, называется 2-непротиворечивым, если ни для какой формулы Ф этого исчисления невозможно одновременное выполнение условий ├ Ф и ├ Ф.

Очевидно, что если язык какого–либо исчисления удовлетворяет требованиям, содержащимся в определении 2, то из 2-непротиворечивости такого исчисления вытекает и его 1-непротиворечивость.

Следствие 2: исчисление высказываний является 2-непротиворечивым (а потому и 1- непротиворечивым).

Доказательство: пусть├ Ф. Согласно критерию выводимости для ИВ, имеем

Ф ≡ 1

Но тогда, согласно таблице истинности для , имеем

Ф ≡ 0,

а потому, в силу критерия выводимости, неверно, что

├Ф,

ч.т.д.

Заключительные замечания


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

алгоритм, распознающий формулы ИВ среди произвольных слов в соответствующем алфавите;

алгоритм распознавания формальных выводов среди произвольных последовательностей формул;

алгоритм распознавания выводимых формул.

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

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

В настоящем пособии мы следовали формулировке классического ИВ, предложенной в книге П.С. Новикова [2].

Литература

1. Верещагин Н.К., Шень А., Языки и исчисления, М., МЦНМО, 2000.
   
2. Новиков П.С., Элементы математической логики, М., Наука, 1973.
   
3. Успенский В.А., Верещагин Н.К., Плиско В.Е., Вводный курс мате-
   

матической логики, М., Физматлит, 2002.

4. Математическая энциклопедия: статьи “Аксиоматический метод”,
   

т.1, М., 1977, стр. 109-113; “Логические исчисления”, Т.3, М., 1982,

стр. 416-420.