Система аксиом и теория формального вывода

Размещено на http://www.allbest.ru/

Размещено на http://www.allbest.ru/

Система аксиом и теория формального вывода

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

К первоначальным, неопределяемым понятиям аксиоматической теории высказываний относятся следующие: Х₁, Х₂, …, Х_n,... -- пропозициональные переменные. Первоначальным понятием является также понятие формулы, которое определяется (как и в алгебре высказываний) индуктивным образом:

1) каждая пропозициональная переменная есть формула;

2) если F₁ и F₂ -- формулы, то выражения F₁, (F₁ F₂) также являются формулами;

3) никаких других формул, кроме получающихся согласно пунктам 1 и 2, нет.

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

(Al) (F (G F)),

(А2) ((F (G Н)) ((F G) (F Н)),

(A3) ((G F) (G F) G)),

где F, G, Н -- произвольные формулы. Таким образом, каждое из выражений (Al), (A2), (A3) задает лишь форму аксиомы. Они превращаются в аксиомы, если вместо F, G и Н подставить конкретные формулы (в частности, пропозициональные переменные). Следовательно, каждое из этих выражений задает бесконечное множество формул. Все они называются аксиомами. Поэтому каждое из выражений (А1), (А2), (A3) называют схемой аксиом.

Наконец, заключительный шаг, закладывающий основу аксиоматической теории высказываний, состоит в выборе правил вывода. Единственным правилом вывода будет служить правило заключения (или отделения, или modus роnens, или сокращенно МР): из формул F и F G непосредственно следует формула G.

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

Поскольку в аксиомах не участвуют связки , , , то придется определить их. Введем следующие определения:

(FG) означает (F G),

(FG) означает (FG),

(FG) означает ((FG) (GF))

Смысл, например, первого из определений состоит в том, что, каковы бы ни были формулы F и G, формула (FG) служит обозначением для формулы (F G).

2. Понятие вывода и его свойства

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

Определение 14.1. Доказательством или выводом формулы F из множества формул Г называется такая конечная последовательность В₁, В₂, …, B_s формул, каждая формула которой является либо аксиомой, либо формулой из Г, либо получена из двух предыдущих формул этой последовательности по правилу МР, а последняя формула B_s совпадает с F. Если имеется вывод формулы F из множества Г, то говорят, что F выводима из Г, или что Г выводит F, и пишут Г ? F. Элементы из Г называются гипотезами или посылками вывода. Если же имеется вывод формулы F из пустого множества гипотез, то говорят, что F выводима из аксиом, или что F доказуема, а последовательность В₁, В₂, …, B_s называется доказательством этой формулы. Саму F называют теоремой и пишут F. Таким образом, запись «F» служит сокращением утверждения «F есть теорема».

Если множество Г конечно: Г = {F₁, F₂, …, F_m}, то вместо {F₁, F₂, …, F_m? G будем писать F₁, F₂, …, F_mG.

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

Приведем пример доказательства какой-нибудь формулы.

Пример 14.2. Доказать: F F.

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

(F ((F F) F)) ((F (F F)) (F F)),

F ((F F) F),

(F (F F)) (F F),

F (F F),

F F.

Поясним. Формула (1) представляет собой аксиому (А2), в которой в качестве формул F и Н взята формула F, а в качестве формулы G взята формула FF. Формула (2) представляет собой аксиому (А1), в которой в качестве формулы G берется формула F F. Формула (3) получена из формул (1) и (2) по правилу МР. Формула (4) есть аксиома (А1). Наконец, формула (5) получена из формул (3) и (4) по правилу МР.

Таким образом, F F.

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

Теорема 14.3 (свойства выводимости).

а) Если ГF и Г , то F.

б) ГF тогда и только тогда, когда в Г существует такое конечное подмножество , что F.

в) Если G для любой формулы G из множества и ? F, то Г? F.

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

б) Достаточность вытекает из свойства (а). Обратно, если Г? F, то, по определению 14.1, существует вывод F из Г, то есть некоторая конечная последовательность формул, использующая, следовательно, лишь конечное число посылок из Г. Поэтому можно считать, что именно эта конечная часть формул из Г и выводит формулу F.

в) По условию, ? F. Тогда, ввиду предыдущего свойства (б), в существует такое конечное подмножество ₀, что ₀ ? F. Пусть ₀ = {В₁, В₂, …, B_k. По условию, кроме того, Г ? B₁, Г ? В₂,..., Г ? B_k, то есть имеются выводы каждой из формул В₁, В₂, …, B_k из множества гипотез Г, представляющие собой конечные последовательности формул. Выпишем эти последовательности одну за другой и добавим к ним последовательность, являющуюся выводом формулы Г из множества гипотез ₀ = {В₁, В₂, …, B_k. Полученная таким образом последовательность будет представлять собой вывод формулы F из множества гипотез Г, то есть Г F.

3. Теорема о дедукции и следствия из неё

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

Теорема 14.4 (о дедукции). Если F₁,..., F_m-1, F_m G, то F₁,..., F_m-1, F_m F_m G. В частности, если F G, то F G.

Доказательство. Предположим, что последовательность формул

В₁, В₂, …, В_i, …, B_s (1)

является выводом формулы G из гипотез F₁,..., F_m-1, F_m (такая последовательность существует, поскольку, по условию, F₁,..., F_m-1, F_m ? G). Следовательно, формула B_s есть формула G, B_S G (« » -- знак графического совпадения, одинаковости формул). Рассмотрим последовательность формул:

F_m В₁, F_m B₂,..., F_m В_i, …, F_m B_s (2)

На последнем месте данной последовательности стоит формула F_m G (так как B_s G). Но эта последовательность, вообще говоря, не является выводом из гипотез F₁,..., F_m-1. Тем не менее, её можно превратить в такой вывод, если перед каждой формулой последовательности добавить подходящие формулы. Для этого покажем методом математической индукции по й, что

F₁,..., F_m-1? F_m B_й (3)

1) й = 1. Покажем, что F₁,..., F_m-1F_m B_й. Для формулы В_й как первого члена последовательности (1), являющейся выводом G из F₁,..., F_m-1, F_m, могут представиться следующие возможности:

а) В_й есть либо одна из аксиом, либо одна из гипотез F₁,..., F_m-1. В этом случае вывод формулы F_m B_й из гипотез F₁,..., F_m-1 строится так:

В₁, B₁ (F_m B₁), F_m B₁ (4)

Вторая формула здесь есть аксиома (А1), а третья получена из первых двух по правилу МР. Таким образом, в последовательность (2) перед первой формулой нужно добавить первую и вторую формулы из последовательности (4).

б) В₁ есть гипотеза F_m. Тогда формула F_m В₁ принимает вид F_m F_m. Но, согласно примеру 14.2, эта формула выводима не только из гипотез F₁,..., F_m-1, а выводима просто из аксиом. Ее вывод (приведенный в примере 14.2) нужно вписать в последовательность (2) перед первой формулой в этом случае.

2) й ? k. Предположим, что утверждение (3) верно для всех й ? k и все необходимые выводы добавлены перед всеми k первыми формулами последовательности (2).

3) й = k + 1. Покажем теперь, что утверждение (3) верно для й = k + 1, то есть справедлива выводимость:

F₁,..., F_m-1 F_m В_{k + 1}

Для формулы В_{k + 1} как члена последовательности (1), являющейся выводом G из гипотез F₁,..., F_m-1, F_m, могут представиться следующие возможности:

а), б) В_{k + 1} есть либо одна из аксиом, либо одна из гипотез F₁,..., F_m-1, F_m. Данные возможности абсолютно аналогичны соответствующим возможностям из случая й = 1 (там лишь нужно В₁ заменить на В_{k + 1}).

в) В_{k + 1} получена из двух предыдущих формул В_i, В_j последовательности (1) по правилу МР. Следовательно, 1 ? i < k + 1, 1 ? j < k + 1 и формула В_j, имеет вид В_i В_{k + 1}, то есть В_j В_i В_{k + 1}. Поскольку 1 ? i < k + 1 и 1 ? j < k + 1, поэтому формулы F_m В_i и F_m В_j стоят в последовательности (2) перед формулой F_m B_{k + 1} и, следовательно, по предположению индукции, справедливы утверждения о том, что имеются выводы этих формул из гипотез F₁,..., F_m-1. Выпишем выводы последовательно друг за другом (они завершаются формулами F_m В_i и F_m (В_i B_{k + 1}) соответственно; напоминаем, что В_j В_i В_{k + 1}):

(б) F_m В_i

(б + в) F_m (В_i B_{k + 1})

Продолжим выводы следующими формулами:

(б + в + 1) (F_m (В_i B_{k + 1})) ((F_m В_i) (F_m B_{k + 1})),

(б + в + 2) (F_m В_i) (F_m B_{k + 1})),

(б + в + 3) F_m B_{k + 1}.

Первая из формул есть аксиома (А2), вторая формула получена из первой и формулы (б + в) по правилу МР, третья получена из второй и формулы (б) по правилу МР. Таким образом, построенная последовательность есть в этом случае вывод формулы F_m B_{k + 1} из гипотез F₁,..., F_m-1.

Итак, утверждение (3) верно для любого й = 1, 2,..., s. При й = s получаем (напоминаем, что B_s = G):

F₁,..., F_m-1 F_m G,

что и требовалось доказать.

Следствие 14.5. F₁,..., F_m-1, F_m G тогда и только тогда, когда F₁,..., F_m-1 F_m G.

Доказательство. Необходимость представляет собой теорему о дедукции. Обратно, если F₁,..., F_m-1 ? F_m G, то существует соответствующий вывод:

В₁, …, B_s-1, F_m G.

Дополним его двумя формулами F_m и G. Получим последовательность

В₁, …, B_s-1, F_m G, F_m, G,

представляющую собой вывод формулы G из гипотез F₁,..., F_m-1, F_m, потому что предпоследняя формула этой последовательности есть одна из гипотез, а последняя получена из двух предшествующих ей формул по правилу МР. Следовательно, F₁,..., F_m-1, F_m G.

Следствие 14.6. F₁,..., F_m-1, F_m G тогда и только тогда, когда F1 (F₂ … (F_m-1 (F_m G)) …).

Данное следствие получается в результате m-кратного применения предыдущего следствия.

4. Применение теоремы о дедукции

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

Лемма 14.7. Для любых формул F, G, H справедливы следующие выводимости:

а) F G, G Н F H;

б) F (G Н), G F H.

Доказательство. а) Покажем сначала, что F G, G H, F ? H. Для этого построим последовательность, являющуюся соответствующим выводом:

F G, G H, F, G, H.

Поясним. Первые три формулы последовательности суть гипотезы. Четвертая формула G получена из первой и третьей формул последовательности по правилу МР, а пятая -- из второй и четвертой по тому же правилу. Итак, FG, G H, F H. Отсюда, на основании теоремы о дедукции заключаем, что

F G, G H F H.

б) Нетрудно видеть, что F (G Н), G, FH, откуда требуемая выводимость следует на основании теоремы о дедукции.

Теорема 14.8. Для любых формул F, G следующие формулы являются теоремами формализованного исчисления высказываний:

а) F F;

б) F F;

в) F (F G);

г) (G F) (F G);

д) (F G) (G F);

е) F (G (F G);

ж) (F G) ((F G) G).

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

в) Покажем сначала, что F, F G. Приводим соответствующий вывод, обосновать который предлагается самостоятельно.

Итак, F, F G. Тогда, по теореме о дедукции, F F G. Применяя еще раз теорему о дедукции, получаем F (F G).

г) Покажем, что G F, F G. Для этого строим соответствующий вывод (в обоснование его укажем лишь, что формула (6) получена из формул (5) и (4) на основании леммы 14.7, а):

(1) G F,

(2) F,

(3) (G F) ((G F) G,

(4) (G F) G,

(5) F (G F),

(6) F G,

(7) G.

5. Производные правила вывода

аксиома дедукция производная

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

Теорема 14.9 (правила введения логических связок). Справедливы следующие производные правила вывода, называемые правилами введения логических связок (где Г -- некоторое, возможно, и пустое множество формул).

Доказательство. а) Данное правило есть не что иное, как теорема о дедукции (теорема 14.4).

б) Обосновать правило предлагается самостоятельно. Напомним только, что запись F G, согласно определению, означает ?(F ?G).

6. Доказуемость формулы и ее тождественная истинность (синтаксис и семантика)

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

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

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

Сформулируем и докажем первую часть теоремы полноты.

Теорема 15.1. Всякая доказуемая в формализованном исчислении высказываний формула является тождественно истинной формулой (или тавтологией) алгебры высказываний. Символически:

F ¦ F.

Доказательство. Пусть формула F доказуема в формализованном исчислении высказываний и последовательность В₁, В₂,..., B_s представляет собой вывод формулы F из аксиом. Покажем, что F -- тавтология. Доказательство будем вести индукцией по длине s вывода этой формулы.

s = 1. Тогда последовательность-вывод состоит из единственной формулы В₁, которая, следовательно, может быть на основании определения вывода только аксиомой. Все три аксиомы (Al), (A2) и (A3) являются тавтологиями алгебры высказываний на основании теорем 3.1,з, 3.3,а, 3.3,л соответственно.

s ? n. Предположим теперь, что все формулы, имеющие вывод длины s ? n, являются тавтологиями. Это предположение индукции.

s = n + l. Покажем, что всякая формула, имеющая вывод длины s = n + l, также является тавтологией. В самом деле, пусть F -- произвольная формула и В₁, В₂,..., B_n, В_n+1 F-- её вывод длины n + 1. На основании предположения индукции, первые n членов данной последовательности -- тавтологии. Рассмотрим формулу В_n+1. По определению вывода, она может быть либо аксиомой (и тогда она является тавтологией, как было отмечено в первой части доказательства), либо получена из двух предыдущих членов этой последовательности B_i и В_j (1 ? i ? n -- 1, 2 ? j ? n) по правилу modus ponens (МР). Во втором случае тогда В_j B_i В_n+1 и, кроме того, обе формулы B_i и В_j являются тавтологиями на основании предположения индукции. Итак, ¦ В_i, и ¦ В_i В_n+1. Следовательно, по теореме 3.5 (правило заключения), ¦ В_n+1.

Итак, какой бы длины ни имела вывод в формализованном исчислении высказываний формула, она будет тавтологией алгебры высказываний.

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

Размещено на Allbest.ru