Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 110
Текст из файла (страница 110)
ц Это утверждение тесно связано с теоремой 1 части П моногрзфнн А. Мостовского, Р. М. Робинсона н А. Тарского: Мое!о«)зй( А., КОЬ1нв Й. М., Т а г з К ! А. 11нбес!баые Тьеопез,— Ашз!еп4аш, 1953, р. 46. з) Приведенное здесь рассужденке ванмствовано нз доказательства Чйрча, Поэтому число и является номером какой-либо выводимой в (Еее) формулы тогда н только тогда, когда можно указать такое число ш, для которого выполняется равенство (е ()н) = и Но это имеет место тогда и только тогда, когда формула Чх(1з(х)=п) выводима в некотором формализме 6, получающемся из исчисления предикатов добавлением к нему равенств, использованных при определении 1»(п), и аксиом равенства (йз) а=а и (йз) а = Ь -)- (А (а) -+- А (Ь)).
Действительно, в случае выполнения равенства (е(ш)=п оно, а тем самым и формула (к(1з(х)=п), выводимо в 6. И обратно: в случае выводимости этой формулы в 6 по доказанной в гл. 1 нп-теореме' ) может быть указано число ш, для которого выполняется равенство 1,(ш) = п. Далее, в соответствии с полученными в гл.
111 результатами, касающимися возможности исключения функциональных знаков при исследовании выводимости формул' ), выводимость в 6 формУлы 3х(1е(х) = и) Равносильна вывоДимости некотоРой фоРмУлы й без функциональных знаков в некотором формализме б„который получается из 6, если сначала исключить из 6 штрих-символ и остальные функциональные символы и ввести вместо ннх соответствующие предикатные символы, содержащие по одному дополнительному аргументу каждый, а затем для каждого предикатного символа 4)(аз, ..., а„а) с Дополнительным аРгУментом а, ввеДенного вместо функционального знака ((а„..., а,), взять в качестве аксиом «формулы единственности» Зх$(аз, ..., а„х) и )з(х)й)у(Ч)(аз, ..., а„х)8(4)(ам ..., а„у)-Рх у), а рекурсивные равенства заменить теми не содержащими функ- циональных знаков аксиомами, в которые переходят зги равенства в результате использования для каждого исключаемого функцио- нального знака соответствующей эквивалентности з((( - .))-» (в( ".
ь ) з(")) ) )" ) )")" "" Ф)" "" ° ° )! З 1 (з частности, с. 81). з) См, с, 183 — 186 нлн соответственно т. 1, с. 538-544, 510 4 31 ПРИЛОЖЕНИЕ и! Прп этом рассматриваемая формула К в 6, с применением только что упомянутой эквивалентности может быть переведена в формулу (х(!е(х)=п). Если предикатный символ, введенный вместо штрих-символа, обозначить через ЗЧ(а, Ь), то формулу К можно будет взять в виде )Ует ... е!!$ 11!7х (ЗЧ (О, 51) е' ЗЧ (ет, 5~) 5! ° ° ° л! ЗЧ(Г! 5!+1)5:".~ЗЧ(Хп — ы 5п-1)~ЗЧ(5п — ! х)-~6(х)).
ЗДесь 5„..., 5п ! — отличные ДРУГ от ДРУга и от х свЯзанные переменные, а выражение О. (х) не зависит от числа и, а значит, оно определяется уже рекурсивным определением функции 1,(и). Впрочем, формула К не содержит свободных переменных.
Наконец, — ввиду теоремы о представимости общей аксиомы равенства ()и) с помощью собственных аксиом') — здесь вместо формализма 6, можно рассмотреть формзлизм б„получающийся из 6, в результате замены исходной формулы а = Ь-«(А(а) — «А(Ь)) специальными формулами равенства, относящимися к предикатным символам из 6, (или к их различным аргументам), включая и формулу а=Ь-«(а=с — Ь=с).
Это означает, что формула К выводима в 6, тогда и только тогда, когда она выводима в 6п Но по одной ранее доказанной теореме') выводимость К в формализме 6„который получается из исчисления преднкатов добавлением ряда предикатных символов и символа О, равносильна выводимости в исчислении предикатов некоторой конкретной формулы е, которая получается из К, если во всех аксиомах формализма 6, все свободные переменные заменить связанными (т. е. связанными соответствукпцими кванторами всеобщности), затем по так модифицированным аксиомам 61, ..., !7(4 построить формулу и в ней заменить символ О переменной а, а различные предикатные символы — различными формульными переменными, причем для каждого предикатного символа нужно брать соответствующую формульную переменную с тем же числом аргументов.
Если мы теперь примем во внимание, что рекурсивное определение функции 1е(а) может быть задано в явном виде и что с помощью этого определения могут быть явно написаны аксиомы 6, равно как и аксиомы б„а потому и формулы Я„..., Яе, и что с помощью этого определения может быть также построено выражение 6. (х), то станет ясно, что номер, который при нашей !) См. т. 1, с.
456 — 450 плк Прпложекке 1 к данному тому, е. 472-473. и) См, е. 185. неРАЗРешимость пРОБлемы РАЗРБшимости 511 нумерации исчисления предикатов получит формула е, в его зависимости от числа и определится некоторой рекурсивной (я даже достаточно простой) функцией Ь(п), Таким образом, значение Ь(п) этой функции для числа и является номером такой формулы исчисления предикатов, которая выводима тогда и только тогда, когда и является номером формулы, выводимой в (2ее).
Если мы теперь допустим, что для исчисления предикатов можно указать регулярно вычислимую разрешающую функцию (, то функция ((Ь(п)) каждому числу, являющемуся при нашей нумерации (Еее) номером некоторой выводимой в (Хее) формулы, будет сопоставлять значение О, а всякому другому числу — значение 1. Кроме того, эта функция, как и (, будет регулярно вычислимой. Таким образом, мы получаем регулярно вычислимую разрешающую функцию для (2ео), что, однако, невозможно. ПРИЛОЖЕНИЕ П1 О НЕКОТОРЫХ ФРАГМЕНТАХ ИСЧИСЛЕНИЯ ВЫСКАЗЫВАНИЙ И ИХ ДЕДУКТИВНОМ ОПИСАНИИ С ПОМОЩЪЮ СХЕМ й 1.
Позитивно тождественные импликативные формулы В гл. 111 т. 1 при рассмотрении исчисления высказываний из всей логики высказываний в целом нами была особо выделена так называемая поз и т и в н а я лог и к а, представляющая собой совокупность таких способов умозаключений, которые не зависят от допущения о том, что для каждого суждения имеется другое, ему противоположное. Первоначально зто выделение носило эвристический характер. Затем для импликативной логики оно было формально уточнено посредством понятия позитивно тождественной имп- ликатив формулы'), которое было введено о помощью следующего определения: Под импликативной формулой понимается формула, которая строится из переменных исчисления высказываний (т.
е. из формульных переменных без аргументов) с помощью одного только символа импликации. Импликативная формула называется р е г уля р ной, если она имеет вид Ях -ь- (Яа -+ ...-ь (Я и -ь. 6)...), где посылка любой входящей в формулы Я, ..., Я„, Е импликации представляет собой некоторую переменную, а формула д) либо совпадает с одной из формул Ях, ..., 'Ли, либо выводится из этих формул с использованием одной только схемы заключения Я, Я-ь~ Импликативная формула называется позитивно тождест-. венной, если она либо является регулярной формулой, либо получается из какой-либо регулярной формулы в результате:.
подстановки, либо выводится из формул этого рода с помощью) схемы заключения. ! Из этого определения следует, что совокупность позитивно, тождественных формул совпадает с совокупностью тех формул, х) См. т. 1, с. !СС. $ Н ПОЗИТИВНО ТОЖДЕСТВЕННЫЕ ИМПЛИКАТИВНЫЕ ФОРМУЛЫ 613 которые могут быть выведены из регулярных формул в результате применения подстановок и схем заключения. В самом деле, это вытекает из того, что в любом выводе, производимом с помощью подстановок и схем заключения, все подстановки могут быть перенесены в исходные формулы'). Поэтому, если под в ы во до м мы будем понимать вывод с помощью подстановок и схемы заключения, то в качестве системы исходных формул (аксиом) для вывода всех позитивно тождественных импликативных формул (и только их) можно будет взять любую систему регулярных импликативных формул, из которой выводятся все регулярные импликативные формулы.
В качестве такой системы аксиом можно взять систему, состоящую из следующих трех регулярных формул: А -~-(В-ь. А), (А -1-(А -+ В)) -ь(А -ь В), (А -ь В)-+ ((В -+С)-+(А -э-С)), т. е. из формул 1 1) — 3) приведенной в гл. 1П т. 1 системы аксиом для исчисления высказываний'), а также систему, состоя- щую из двух формул < А — ( — ь А), (А-+ (В-ь С))-ь((А-ьВ)- (А-ьС)). Сказанное мы дополним в нескольких направлениях. Во-пер- вых, мы дадим более простую характеристику позитивно тождест- венных импликативных формул. Во-вторых, докажем, что обе только что приведенные системы формул действительно достаточны для вывода всех регулярных, а тем самым и всех позитивно тождественных формул.
И, в-третьих, мы распространим понятие позитивно тождественной формулы на формулы исчисления выска- зываний, строящиеся с помощью нмпликации и конъюнкции. В качестве общего средства, помогающего провести все эти рассмотрения, мы используем одну весьма общую теорему, пред- ставляющую собой некоторое обобщение доказанной в гл. !У т. 1 дедукционной теоремы'). Впрочем, возможности применения этой теоремы не ограничиваются приводимыми здесь рассуждениями (и даже исчислением высказываний).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
