Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 40
Текст из файла (страница 40)
К числу этих символов могут принадлежать и некоторые функциональные знаки. Пусть эти функциональные знаки будут (л(а„..., а1,), ..., «лв(а„..., ат ). Мы построим по Р некоторый расширенный формализм Р„ сопоставив указанным функциональным знакам предикатные символы л414(Ь, а,, ..., а1), ..., флв(Ь, а,, ..., а1 ) и сформулировав для этих символов следующие явные опреде- ления: «1) 4),(Ь, а,, ..., а1!л) Ь = 11(а,, ..., а,.) (! = 1, ..., ж). Зто расширение формализма Р до Р, является несущественным, ') В связи с этим см. ээмсчэнис н- с, 29 -30. э) См.
т. 1, с 541 — 543. 185 184 Е СИМВОЛ И ЛОГИЧГСКИП ЭОГ114ЛИЗМ [ ГЛ 1П включиниа лксномгя пв во втогяю е.теогямэ потому что оно состоит всего лишь в добавлении явно определенных символов. Если формализм Р непротиворечив, то непременно будет непротиворечивым и Р,. Из формул (1) с помощью аксиом равенства могут быть выведены формулы с Зх());(х, и,, ..., аь) (1=1, ..., а1).
12) Ч),(Ь, а,, ..., а~,~ й!В,(с, а,, ..., ао)- Ь =с, а также эквивалентности (3) А1(;(а,, ай)) Ух~ел);(х, а,, ..., а~'1-эА(х)) (1=1, ..., 1п). (,(и1, ..., о,) а„ф~(х, а„..., аь) выражением или "~('" "'') соответственно (при этом мы пользуемся свободой выбора связанных переменных для предотвращения коллизий между ними). С помощью эквивалентностей (3) каждая формула 6 из формализма Р, может быть переведена в некоторую формулу 6*, не содержа:цую функциональных знаков. В частности, аксиомы 81„..., Л„могут быть переведены в некоторые формулы Л*,, ..., 81„', в которых функциональные знаки уже фигурировать не будут. Мы будем считать такого рода формулы 81",, ..., 'Л'„построенными.
Пусть теперь 6— какая-либо формула, выводимая в формализме Р„ и пусть 6'— формула без функциональных знаков, в которую переводится формула 6. Тогда 6* с помощью исчисления предикатов и аксиом равенства может быть выведена из формул 'Л',, ..., Л„ *и формул (1). В любом таком выводе, вообще говоря, встречаются функциональные знаки. Однако мы покажем, что зти функциональные знаки могут быть устранены, если в качестве аксиом ввести (выводимые в формализме Р,) формулы (2).
В самом деле, пусть 6* — какая-либо формула формализма Р„ не содержащая функциональных знаков, и пусть нам дан какой- либо вывод этой формулы из формул 11,*, ..., Л„"и (1), использующий средства исчисления предикатов и аксиомы равенства (31) и (31). Тогда функциональные знаки 1„ ..., 1 можно будет устранить введением е-символа и е-формулы и заменой каждого выра- жения Тогда формулы (1) перейдут а формулы (4) 141;(Ь, а1, ..., ай) Ь=е,4);(х, а„..., аа) (1=1,, 1я), которые выводимы из формул (2) с помощью исчисления предикатов, е-формулы и аксиомы равенства (Юе). Тем самым мы получаем некоторый вывод формулы 6* из формул 'Л;, ..., 81„*, (2) и аксиом равенства с помощью исчисления преднкатов и е-формулы. А так как формулы (2), равно как и формулы 81*„..., 1Л„", не содержат ни формульных переменных, ни е-символа, то по второй е-теореме из этого вывода е-символ можно исключить, так что у нас получится вывод формулы 6ь из формул 81;, ..., 1Лю (31), (31) и (2) с помощью средств исчисления предикатов.
Обозначим посредством Р~ формализм, который получится из Р, если мы возьмем формулы Л,", ..., 1Л*„ вместо формул 811, ..., Л„, а формулы (2) в качестве аксиом и исключим функциональные знаки (аксиомы равенства (31) и (31) сохраняются). Тогда в силу вышеизложенного будет верна следующая Теорема, По всякой формуле 6 формализма Р можно построить некоторую формулу 6'* формализма Рь, переводимую в 6 с помощью эквивалентностей (3), т.
е. внутри Р1, При этом, если формула 6 будет выводима в Р, то всякая формула 6"', находящаяся к 6 в укпзанном отношении, п1оже будет выводимо в Р*. Верно и обратное: Если формула 6* выводима в Рь, то 6 тоже можно будет вывести в Р. Действительно, пусть нам дан некоторый вывод формулы цк в формализме Рь.
Заменим в этом выводе каждое выражение 9~(Ь, а„..., а1,.) равенством Ь=(,(аз, "., а,,), вследствие чего вместо предикатных символов $,, ..., 9ы снова появятся функциональные знаки („..., ( . Тогда у нас получится некоторая последовательность формул, которую можно будет дополнить до вывода формулы 6 в формализме Р. В самом деле, в результате указанной замены формула 6* перейдет в некоторую формулу 6ь*, каждая из аксиом Л*; перейдет в некоторую формулу Л~", аксиомы равенства останутся без изменений, а из формул (2) получатся такие формулы, которые можно будет вывести с помощью аксиом равенства (31) и (Д1). Тем самым мы получим вывод формулы 6"* из формул 211**, ..., 21„" средствами [г'л ги е-СИМВОЛ И ЛОГИЧЕСКИЙ ФОРМАЛИЗМ $2! включение Аксиомы сь! во втоРКЮ е.теОРЕМГ 1зт исчисления предикатов, а кроме того из формул (3) средствами исчисления предикатов можно будет вывести эквивалентности 6 6 е й( 11е 31 е)е Если в выводах этих эквивалентностей выражени $ % я !(, а„..., аг) !) всюду заменить соответствующими им равенствами е=( (, ...,,), =,(а„..., ай), то результирующие формулы этих выводов перейду лентности т в эквива- 6 6**, 31, У1*,", ..., Л„атее П ° а из формул (3) получатся такие формулы, которые можно будет вывести из аксиом равенства.
Поэтому у нас получатся выводы 6 6 е е э( э)ее э( э)ее и использующие средства исчисления предикатов и аксиомы рав ( е) (,), а эти выводы в сочетании с ранее полученным равен- выводом формулы 6ее из формул Й*" ... 'Д"*, (Л ), (Л вывод формулы 6 из аксиом 31„..., й)е.
(Л!), (Л,) средствами исчисления предикатов, т. е. вывод 6 в формализме Р. Таким об азом, и р, мест место определенный параллелизм между выводами в формализме Р и выводами в формализме Р*: Во-первых, всякая формула формализма Р с помощью явных определений (1) и аксиом равенства переводима в некоторую формулу формализма Р*, и обратно, всякая формула формализ Р* п и заме р замене всех входящих в нее выражений ч)!(е, а„..., аг) м лизма соответствующими им равенствами 1 = 1! ( !, ...,,) =;(!„..., а~.,) переходит в некоторую формулу формализма Р, в которую она переводима с помощью формул (1) и аксиом равенства; во-вторых, если из переводимы друг какие-либо две формулы 6 из Р и 6* из Р" в друга с помощью формул (1) и аксиом равенства то бом выво б в у ду ( формализме Р мы получим некоторый вывод 6* в, то по люв формализме Р* и наоборот.
Тем самым исследование выводимостей в формализме Р сводится к исследованию выводимостей в Р'. Но формализм Ре является более узким, поскольку он не содержит функци ональТак что мы вновь приходим к заключению, что теоретикодоказательственное исследование формализованных систем аксиом первой ступени, содержащих аксиомы равенства (Л ) и (Л ) вс может быть све е знаков, д но к исследованию систем без функциойальных Недостатком сформулированного результата является ограничивающее его предположение о том, что рассматриваемый формализм должен обязательно содержать аксиомы равенства (Лд) и (Ле).
Но с помощью доказанной ранее теоремы об исключении аксиом равенства ') можно получить соответствующий результат и для тех случаев, когда заданный формализм либо вообще не содержит знака равенства, либо хотя и содержит его, но имеет только собственные аксиомы и, следовательно, не включает в себя аксиому (Ле). Рассмотрим сначала первый случай. Пусть нам дан формализм Р„получающийся нз исчисления предикатов добавлением некоторых символов (индивидных, функциональных и преднкатных) и некоторых собственных аксиом й!» ..., Ле. Пусть знак равенства в число перечисленных символов не входит, Так как по условию в Ре могут содержаться некоторые функциональные знаки (! (а„..., а!!) (! = 1 "° ° а'). то путем добавления знака равенства и аксиом (ЛА) и (Ле) можно будет расширить этот формализм Р, до некоторого формализма Р только что рассмотренного типа, а от Р описанным выше способом можно будет перейти к формализму Ре, не содержащему функциональных знаков.
Каждая формула 6 формализма Р, — как формула формализма Р— с использованием эквивалентностей (3) может быть переведена в некоторую формулу 6* формализма Р* и по выводу 6 в Р„мы получим некоторый вывод 6* в Р*. Но верно и обратное. Действительно, по выводу 6* в Ре мы сначала получим вывод 6 в Р, т. е. вывод 6 из аксиом е(„..., 6е с помощью исчисления предикатов и аксиом равенства (Л,) и (Ле).
Но так как ни формула 6, ни аксиомы е(,, ..., е(е (которые все принадлежат Ре) знака равенства не содержат, то по ранее доказанному из этого вывода можно исключить применение аксиом равенства, и тогда мы получим вывод формулы 6 в формализме Р„. Таким образом, исследование выводимостей в Ре может быть сведено к исследованию некоторых выводимостей в формализме Р*, не содержащем функциональных знаков. Остается еще рассмотреть случай, когда в формализме хотя и присутствует знак равенства, но для него имеются только собственные аксиомы, и, значит, нет аксиомы (Л,). Этот случай можно свести к только что рассмотренному, взяв вместо знака равенства какой-нибудь другой символ, например 1б(а, Ь). Так е) См, с.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
