Игошин Математическая логика и теория алгоритмов (1019110), страница 31
Текст из файла (страница 31)
Формула (1) представляет собой аксиому (А2), в которой в качестве формул Р и Н взята формула с", а в качестве формулы 6 взята формула Р— > Р Формула (2) представляет собой аксиому (А!), в которой в качестве формулы 6 берется формула Р— » Р. Формула (3) получена из формул (1) и (2) по правилу МР. Формула (4) есть аксиома (А1). Наконец, формула (5) получена из формул (3) и (4) по правилу МР.
Таким образом, ь- Р-» с. В следующей теореме отмечается несколько простых„ но важных свойств понятия выводимости из гипотез. !24 Теорема 15.3 (свойства выводимости). а) Если Г» — Г и Г ~ Ь, то Л»- Г; б) Г» — Г тогда и только тогда, когда в Г существует такое конечное подмножество Л, что Л»- Г; в) Если Г» — 6 для любой формулы 6 из множества Ь и Л» — Г, то Г»- Г. Доказательство. а) Данное свойство выражает следующий очевидный факт: если формула Г выводима из множества посылок Г, то она будет выводима и из всякого множества, получаюшегося добавлением к Г новых посылок.
б) Достаточность вытекает из свойства (а). Обратно, если Г»- Г, то, по определению 15.1, существует вывод Г из Г, т.е. некоторая конечная последовательность формул, использующая, следовательно, лишь конечное число посылок из Г. Поэтому можно считать, что именно эта конечная часть формул из Г и выводит формулу Г. в) По условию Л»- Г.
Тогда ввиду предыдущего свойства (б) в Л сушествует такое конечное подмножество Ьь, что Ль» — Г Пусть Ль = („„..., В,). По условию, кроме того, Г»- „û- В„..., Г» — Вь, т.е. имеются выводы каждой из формул Вп Вь ..., В„из множества гипотез Г, представляющие собой конечные последовательности формул.
Выпишем эти последовательности одну за другой и добавим к ним последовательность, являющуюся выводом формулы Г из множества гипотез Ль = (Вь Вн ..., Вг). Полученная таким образом последовательность будет представлять собой вывод формулы Гиз множества гипотез Г, т.е. Г»- Г П Теорема о дедукции и следствия из нее. Процесс построения доказательств для тех или иных формул может оказаться достаточно сложным как в идейном, так и в техническом плане Теорема о дедукции, о которой пойдет речь, выявляет некоторую обшую закономерность при таких построениях и тем самым облегчает процесс построения доказательства, что будет видно из последуюших примеров. Теорема 15.4 (о дедукции).
Если Гп ..., Г и Г»- 6, то Гь ..., Г»» — à — «6. В частности, если Г» — 6, то» вЂ” Г-«6. Доказательство. Пустьпоследовательностьформул является выводом формулы 6 из гипотез Гь ..., Г„ь Г (такая последовательность существует, поскольку, по условию, Г„ ..., », Г»- 6. Следовательно, формула В, есть формула 6, т.е. В, = 6 (- =— знак графического совпадения, одинаковости формул).
Рассмотрим последовательность формул: à — «Вп à — «Вг, ..., à — «В, Г «В. (2) 125 На последнем месте данной последовательности стоит формула à — «6 (так как В, и 6). Но эта последовательность, вообще говоря, не является выводом из гипотез Рь ..., Г„ь Тем не менее ее можно превратить в такой вывод, если перед каждой формулой последовательности добавить подходящие формулы. Для этого покажем методом математической индукции по 1, что Гп ..., Г, «- Г -«В,. (3) 1) 1=!. Покажем, что Гп ..., Г, «- Г -«В,.
Для формулы В, как первого члена последовательности (1), являющейся выводом б из Гп ..., Г„п Г, могут представиться следующие возможности: а) В, есть либо одна из аксиом, либо одна из гипотез Гп ..., В,. В этом случае вывод формулы à — «В, из гипотез Гп ..., Г строится так: Вн В, -«(Г -«В ), Г -«Вп (4) где вторая формула есть аксиома (А1), а третья получена из первых двух по правилу МР. Таким образом, в последовательность (2) перед первой формулой нужно добавить первую и вторую формулы из последовательности (4); б) В, есть гипотеза Г.
Тогда формула à — «В, принимает вид à — «Р. Но согласно примеру 15.2, эта формула выводима не только из гипотез Р;,, Г„п но и просто из аксиом. В этом случае ее вывод, приведенный в примере 15.2, нужно вписать в последовательность (2) перед первой формулой; 2) ! < lс. Предположим, что утверждение (3) верно для всех ! < /с и все необходимые выводы добавлены перед всеми !г первыми формулами последовательности (2); 3) ! = !»+ !.
Покажем теперь, что утверждение (3) верно для != /с+ 1, т.е. справедлива выводимост«к Уь ..., Г, «- à — «В»,, Для формулы В»„как члена последовательности (1), являющейся выводом 6 из гипотез Гь ..., Г и Г, могут представиться следующие возможности: а), б) В, „есть либо одна из аксиом, либо одна из гипотез Уь ..., Г„,, Г . Данные возможности абсолютно аналогичны соответствующим возможностям из случая 1= 1 (там лишь нужно В, заменить на В», ~); в) В»,, получена из двух предыдущих формул Во В, последовательности (1) по правилу МР. Следовательно, 1 < «< /с+ 1, 1 < < / < /с+ 1, а формула В, имеет вид: В; -«В», „т.е.
В, = В; — «В„,, Поскольку 1 < 1< /с+ 1 й 1 < «' < /с+ 1, то формулы à — «В, и Г -«В,. стоят в последовательности (2) перед формулой à — «В», „а следовательно, по предположению индукции, справедливы утверждения о том, что имеются выводы этих формул из гипотез Гп ..., 126 Г„,, Выпишем эти выводы последовательно один за другим, они завершаются формулами à — ~ В; и Г -ь (В; -~ Вл,,) соответственно (напоминаем, что В, и В; — ь Вь,,): (а) à — >В; (а+ 13) Г -ь (В; — ь В„,,). Продолжим выводы следующими формулами: (и+ 13+ 1) (à — > (В;-ь Вг,,)) — > ((Г„-+ В;) -+ (Г -ь Вг„,)); (а+ б+ 2) (Г„-ь В;) -ь (Г -ь Вь, ~); (а+ 13+ 3) Г -+ В„,, Первая из формул есть аксиома (А2), вторая формула получена из первой и формулы (а+ 13) по правилу МР, третья получена из второй и формулы (а) по правилу МР.
Таким образом, построенная последовательность есть в этом случае вывод формулы Г -ь В»„, из гипотез Гп ..., Г Итак, утверждение (3) верно для любого 1= 1, 2, ..., д При 1= л получаем (напоминаем, что В, и 6); Гп ..., Г, ~- à — ~ 6, что и требовалось доказать.
П В задаче Х~ 8.1! Задачника рассматривается процесс пополнения последовательности (2) до вывода (т.е. процесс восстановления вывода формулы Г -э 6 из формул Гп ..., Г,), исходя из данного вывода формулы 6 из формул Гп ..., Г „Г применительно к конкретным формулам Гь ..., Г и Г„, 6. Следствие 15.5. Г„..., Г и Г ь — 6 тогда и только тогда, когда Гп ...„Г, ь- Ä— > 6. До казател ьств о. Необходимость представляет собой теорему о дедукции.
Обратно, если Гп ..., Г, ~- Г ь 6, то существует соответствующий вывод: В„..., В, „à — > 6. Дополним его двумя формулами Г и 6. Получим последовательность В„..., В, и Г„-ь 6, Г, 6, представляющую собой вывод формулы 6 из гипотез Гп ..., Г и Г, потому что предпоследняя формула этой последовательности есть одна из гипотез, а последняя получена из двух предшествующих ей формул по правилу МР. Следовательно, Гп ..., Г„п Г ~- 6. П Следствие 15.6.
Г„„., Г „Г ~- 6 тогда и только тогда, когда ь- Г, -ь (Р~ — > ... -+ (Г, — э (Г -~ 6))...). Доказательство. Данное следствие получается в результате т-кратного применения предыдущего следствия. (3 Применение теоремы о дедукции. С помощью теоремы о дедукции сначала будет доказана одна лемма, которая затем вместе с теоремой о дедукции будет использована для доказательства того, что ряд формул являются теоремами формализованного исчисления высказываний. 127 Лемма 15.7.
Для любых формул Г, 6, Н справедливы следующие выводимости: о) à †» 6, 6 †» Н »- à †» Н; б) Г -» (6 -+ Н), 6» — Г -» Н. Доказательство, о) Покажем сначала, что à — » 6, 6-» Н, Г»- Н. Для этого построим последовательность, являющуюся соответствующим выводом: à — » 6, 6-+ Н, Г, 6, Н.
Поясним. Первые три формулы последовательности суть гипотезы. Четвертая формула 6 получена из первой и третьей формул последовательности по правилу МР, а пятая — из второй и четвертой по тому же правилу. Итак, à — » 6, 6 -» Н, Г»- Н. Отсюда на основании теоремы о дедукции заключаем, что à — » 6, 6-+ Н»- à — » Н. б) Нетрудно видеть, что Г-+ (6 — » Н), 6, Г» — Н, откуда требуемая выводимость следует на основании теоремы о дедукции.
(3 Теорема 15.8. Для любых формул Г, 6 следующие формулы являются теоремами формализованного исчисления высказываний: о) à — »Г; б) Г+ Г; в) — à — » (Г-» 6); г) (- 6 -+ — Г) -+ (à — » 6); д) (à — » 6) -» (-6-» -Г); е) à — » (- 6-+ -(à — » 6)); зк) (Г-» 6) -» ((- Г-» 6) -» 6). Доказательство. о) Обоснуем возможностьдоказательства (построения вывода из аксиом) этой формулы. Рассмотрим следующую последовательность формул: (1): (- Г-+ Г) — » ((- à — » — Г) -+ Г)) [аксиома (АЗ)]; (2): — Г-+ — Г [пример 15.2]; (3): (-à — » Г) -+ Г [(1), (2), лемма 15.7, б]; (4): à — » (- à — » Г) [аксиома (А1)]; (5): Г-+ Г [(4), (3), лемма 15.7, о].
Обратим внимание на то, что сама последовательность (1) — (5) не является выводом формулы — Г-» Гиз аксиом. Чтобы превратить ее в вывод, нужно перед формулами (2) и (5) вписать их выводы из аксиом. Для формулы (2) это сделать нетрудно. Обоснование формулы (5) опирается на утверждение леммы 15.7 о, которое, в свою очередь, обосновано с помощью теоремы о дедукции. Поэтому, чтобы это утверждение можно было использовать в формальном выводе, его необходимо превратить в некоторую формулу, вывод которой, в свою очередь, должен быть построен на основании теоремы о дедукции.