Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 111
Текст из файла (страница 111)
Зта теорема о посылках, как мы ее будем называть, л лУ ф Р Д " "" Р ') См. Приложение 1, с, ПЗ, е) См. т. 1, с. 96. а) См. т, 1, с. !94 — 199 нли Приложение 1, с. 472. Правда, приводнмаи теорема в определенном смысле носит несколько более частный характер, чем дедукнионная теорема !7 Д. Гильаерь П, Вернаас 514 ПРИЛОЖЕНИЕ нп определено понятие ф о р м у л ы и в которых производятся выводы при помощи тех или иных исходных формул, схем для исходных формул н схем вида (й)1»), ..., (й)1!) (Я) (г) 2), где (Щ, ..., (Щ, (21) следует понимать как задания определенных видов формул, в которых совпадающие составные части формул обозначены одинаковыми буквами. Кроме этих схем, принадлежащих к числу первоначальных правил данного дедуктивного формализма [г и называемых соответственно основными схемами формул и основ ными с х е м а м и в ы в о д а этого формализма, мы рассматриваем также выводимые схемы формул и производные схемы вывода.
Схему формул 5д мы будем называть выводимой в [г, если каждая формула описываемого этой схемой йо вида выводима в формализме [,[, а (т+1)-членную схему вида (й)1,), ..., (И„) (91) мы будем называть производной схемой вывода в [Е, если формула 3 выводима из формул Я„..., Я, средствами формализма [[ всякий раз, когда формулы Я„..., Я„З графически находятся в отношении, выраженном обозначениями (Щ, ...
..., (2)Ц, (Я). Теорема о посылках может быть сформулирована следующим образом: Пусть Ц вЂ” дедуктивный формализм указанного выше типа, содержащий импликацию (т. е. связку, сопоставляющую формулам Я и 6 формулу Я-и-6). Пусть, во-первых, среди основных или выводимых схем формул формализма [г содержится схема формул Я-~Я; во-вторых, среди основных или производных схем вывода содерзсится схема вь[вода Я и, кроме того, для каждой (!+1)-пленной овновной схемы вывода формализма [г' (1) (%!)., .. (61!) (51 ) при некотором выборе буквы 9, не входяи[ей в 3)1м ..., Ю1! и э[, и ц ПОЗИТИВНО ТОЖВЕСТВЕННЫЕ ИМПЛИКАТИВНЫЕ ФОРМУЛЫ 515 !хема вывода 6-~(й)1»), ..., 6-и (Я[Ц (2) является либо основной, либо производной схемой вывода в ф Тогда формула Я! ~'(Яп ~(Яп ! 6) ) выводима в [г всякий раз, когда формула З выводима из формул Я„..., Яп средствами формализма [г.
Доказательство этого утверждения почти очевидно. Рассмотрим сначала частный случай, когда Я и З суть такие формулы из [г, что имеется вывод 6 из Я по правилам формализма [г. Если к каждой формуле этого вывода мы импликативно добавим посылку Я, то на том месте, где формула Я используется в качестве исходной формулы, окажется выводимая формула Я -п-Я, на месте каждой исходной формулы 6 формализма 9 окажется выводимая нз нее формула Я -~ 6, а на месте, где применяется какая-либо основная схема (1) формализма [;[, будет применяться соответствующая производная схема (2) формализма 9.
Заключительная формула вывода 6 перейдет при этом в формулу Я-п.З. Значит, эта формула выводима в [г. Теперь теорему о посылках в ее общей формулировке мы сведем к рассмотренному частному случаю. В самом деле, пусть А[! — формализм, получающийся из [г в результате присоединения формул Я„ ..., Яп , к числу исходных. Тогда [г! также удовлетворяет условиям нашей теоремы, а формула 6 средствами формализма (е! выводима из формулы Яп и, значит, по только что доказанному формула Яп-~6 выводима в !гп. Тем же самым способом мы убеждаемся, что в формализме 0„получающемся нз [',[ присоединением формул Я,, ..., Яп, к числу исходных, выводима формула Яп-! (Яп 6).
Продолжая это рассуждение дальше, мы через и шагов получим, что в [г выводима формула ~(Я» +' ' '('1» ~6)'' )' Установленная таким образом теорема о посылках имеет разнообразные применения. Сначала мы используем ее для рассмотРения формализма, в котором формулами являются импликативные формулы исчисления высказываний, а выводимость определяется 17» 5!6 ПРИЛОЖЕНИЕ [1П на основе схем формул 6-«(Š— «6), (Я-«(6-««з)) -« ((6 -«3) -« (6 -« 6)) и схемы заключения Я, Я-«~ Условия теоремы о посылках для этого формализма выполняются. В самом деле, схема вывода 6 6-«6 является производной схемой, и факт этот устанавливается непосредственно прн помощи первой схемы формул и схемы заключения.
Схема вывода ф -«Я, ф -«(Я -« ~) ф -« ~ является производной схел«ой, и этот факт устанавливается при помощи второй схемы формул и схемы заключения, а каждая формула вида 6-«6 может быть выведена следующим образом: 6 -«((6 61 -«6), (Я -» ((6 -«Я) -«6)) -«((6 — «(6 -«6)) -«(6-«6)) (Я -«(6 -«'Л)) -«(6 -«6) 6 -«(6 -~-6), (6 -1-(6 -«6)) †.(6 -« 6) (здесь исходные формулы получаются из указанных выше схем формул — две нз первой схемы и одна из второй — и дважды применяется схема заключения). Согласно теореме о посылках нмплнкатнвная формула 6, -'(6,-«...-«(6„-1-е)...) Выводима в рассматриваемом формализме всякий раз, когда формула 6 выводима средствами этого формализма нз формул Я„...
,,„, Я„и, значит, в частности, когда формула «) совпадает с одной нз формул 6„..., Я„нли выводится при помощи схемы заключения из всех этих формул. Вообще, формулу исчисления высказываний (и, в частности, импликативную формулу) мы будем называть н е п о с р е д с твен но «Н ПОЗИТИВНО ТОЖДЕСТВЕННЫЕ ИМПЛИКАТИВНЫЕ ФОРМУЛЫ тождественной, если она имеет вид 6,— (6,, (Л„- Е).„), где формула 3 совпадает с одной из формул Я„ ..., 6„ или может быть выведена из ннх прн помощи схемы заключения.
Чтобы оправдать эту терминологию, заметим, что, согласно данному определению, всякая непосредственно тождественная формула исчисления высказываний является тождественно истинной, или, как мы иногда говорим, тождественной формулой. В самом деле, если в какой-либо такого рода формуле 61-+.(6»-+ " -+.(Яи -~8) " ) приписать входящим в нее переменным значения «истина» и «ложь», то, в соответствии с истолкованием связок исчисления высказываний как истинностных функций, либо одна из формул 6„..., Я„примет значение «ложь», и тогда вся формула примет значение «истина», либо каждая из этих формул примет значение «истина», и тогда его примет также и формула Е, так как по условию она выводится из ннх в результате применения схемы заключения или же совпадает с одной из них. Тем самым и вся рассматриваемая формула примет значение «истина».
Из определения непосредственно тождественной формулы сразу следует, что всякая регулярная импликативная формула является непосредственно тождественной. Далее, легко видеть, что формулы, получающиеся из непосредственно тождественных формул в результате подстановок, также являются непосредственно тождественными. Для этого достаточно заметить, что если какую-либо формульную переменную, фигурирующую в схеме заключения, заменить всюду, где оиа в этой схеме встречается, одной и той же формулой, то снова получится некоторая схема заключения. Поэтому всякая формула, получающаяся из какой-либо регулярной импликативной формулы в результате подстановки, является непосредственно тождественной, а следовательно, всякая позитивно тождественная импликативная формула выводится из непосредственно тождественных импликативных формул с помощью одной только схемы заключения. Но мы пока не установили, что всякая непосредственно тождественная формула является позитивно тождественной.
А кроме того, например, неверно, что любая непосредственно тождественная имплнкативная формула получается из какой-либо регулярной нмпликативной формулы в результате подстайовки. Так, например, импликативная формула ((А «В) -«(В -«С)) -«((А — «В) -«(А -«С)) явлпется непосредственно тождественной, так как формула С б1В Е Ц ПОЗИТИВНО ТОЖДЕСТВЕННЫЕ ИМПЛИКАТИВНЫЕ ФОРМУЛЫ ПРИЛОЖЕНИЕ может быть выведена из формул (А-РВ)-ь(В-ьС), А-ьВ, А троекратным применением схемы заключения; но тем не менее она не является регулярной и, как показывает разбор могущих здесь представиться случаев, не может быть получена в результате подстановки из какой-либо регулярной импликативной формулы.
И все же утверждение о том, что всякая непосредственно тождественная импликативная формула является позитивно тождественной, имеет место, и его можно извлечь из нашего недавнего результата, полученного с помощью теоремы о посылках. В самом деле, этот результат утверждает, что всякая непосредственно тождественная импликативная формула выводима из схем Я -ь (9 -ь 6) и (й -ь (Е -ь- Я)) -+ ((Я -ь 6) -э- (Я -э- Я)) о помощью схемы заключения, а значит, она выводима из формул А -ь(В -ь А) и (А -ь- ',В -ь С)) -ь ((А — ь В) -ь (А — ь С)) (т, е. из формул 1*) с помощью подстановок и схемы заключения.
Но формулы 1* регулярны и потому каждая формула, выводимая из них с помощью подстаиовок и схем заключения, является позитивно тождественной. Поэтому каждая непосредственно тождественная формула, а тем самым и каждая формула, выводимая из таких формул с помощью схемы заключения, является позитивно тождественной, С другой стороны, ранее мы установили, что всякая позитивно тождественная формула Выводима из непосредственно тождественных формул с помощью схемы заключения. Тем самым позитивно тождественные формулы могут быть охарактеризованы как такие импликативные формулы, которые либо являются непосредственно тождественными формулами, либо выводимы из них с помощью схемы заключения '). Эта характеристика позитивно тождественных импликативных формул проще нашего первоначального определения в двух отношениях; во-первых, в ней нет речи о подстановках и, во-вторых, в определении.
непосредственно тождественных импликативных т) Первую из зтих возможиостей здесь можно было бы особо и ие упомяиать. Дейетвительио, любая непосредственно тождеетвеииая формула % выводима с помощью схемы ваилючеиия из иепосредствеиио тождеетвееиыа формул й и к -еп. Я -.-ь (6-ь 6), (Я-Р (Я -ь Е)) — ь (Я-ьа), (6 -+ иВ) -т- ((В.-ьб ) -+ (6-ь 6)), (4) (5) удовлетворяет условиям теоремы о посылках, т.
е. что схема формул 6-эй является выводимой, а схемы $-ьС, $-ь(Я-+.'ь) являются производными схемами этого формализма. Это может быть проделано без особого труда. 1(ействительно, схему Я мы получаем из схемы (3) и схемы заключения; вывод любой формулы вида 6-эй мы получаем с помощью схем (3) и (4) и схемы заключения следующим образом: й-ь-(Я -ю- Л), (6 -ь(6 -ьй)) -« (й -ьй) й-~6 формул отсутствует ограничение, налагаемое на струитуру регулярных импликативных формул. Наряду с этим упрощением характеризации позитивно тождественных импликативных формул, доказанная нами теорема о выводимости непосредственно тождественных импликативных формул из формул 1* с помощью подстановок и схем заключения позволяет получить еще один обещанный нами результат, а именно, утверждение, что формулы 1' представляют собой систему аксиом, достаточную для вывода (с помощью подстановок и схемы заключения) всех позитивно тождественных формул.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
