Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 107
Текст из файла (страница 107)
Пусть к числу символов формализма Я относится функциональный знак гр с двумя аргументами; пусть этот знак встречается только в одной из наших аксиом, которая имеет вид й(а, Ь, е, гр (а, Ь), гр (а, с)) [это обозначение следует понимать таким образом, что функциональный знак гр (, ) фигурирует только в составе указанных термов гр (а, Ь) и гр (а, с)). Теперь введем какой-нибудь предикатный символ с тремя аргументами (например, Ф) при помощи явного определения Ф (а, Ь, е) гр (а, Ь) = с. Тогда из этого определения могут быть выведены формулы единственности для Ф (а, Ь, с) по аргументу е: ЗхФ (а, Ь, х), 'э>хгз у (Ф (а, Ь, х) 81 Ф (а, Ъ, у) -+ х = у). Воли мы воспользуемся теперь г-правилом, то у нас в качестве терма появится гхФ (а, Ь, х); при этом, с одной стороны, г-правило даст нам формулу Ф(а, Ь, г„Ф(а, Ь,х)), а с другой стороны, определение символа Ф (а, Ь, с) в сочетании с аксиомой (11) даст формулу Ф (а, Ь, >р (а, Ь))", ') Что здесь следует более точно понимать под «предстазимостью», станет ясио из дальнейшего.
тем самыы, с помощью второй из только что приведенных формул единственности, мы получим равенство гр (а, Ь) = г,Ф (а, Ь, х). Воспользовавшись этим равенством и аксиомой (з' з), мы по любой формуле 5, в которую входит функциональный знак гр (, ° ), получим формулу Я', являющуюся результатом замены в $ всякой составной части гр (и, Ь) соответствующим ей выражением г Ф (и, Ь, х). В частности, по аксиоме [((а, Ь, с, гр (а, Ь), гр (а, с)) мы получим формулу й(а, Ь,с, г„Ф(а, Ь,х), г„Ф(а,с,х)), которая переводима в формулу г((Му (Ф (а> Ь, х) 8> Ф (а, е, у) -«. й(а, Ь, с, х, у)).
Теперь, если вместо того, чтобы вводить предикатный символ Ф посредством явного определения, мы возьмем его в качестве основного анака, а обе относящиеся к г„Ф (а, Ь, х) формулы единственности и формулу т>х>Уу (Ф (а, Ь, х) 8г Ф (а, е, у) †« й'(а, Ь, с, х, у)) добавим к аксиомам и при этом опустим аксиому к(а, Ь, с, >р (а, Ь), гр (а, с)), а функциональный знак гр (, ), который ранее был у нас основным знаком, теперь [после введения г,Ф (а, Ь, х) при помощи г-правила) явно определим посредством равенства гр(а, Ь) =г,Ф(а, Ь,х), то совокупность выводимых формул не изменится.
В самом деле, в результате этого формулы й(а, Ь, е, гр (а, Ь), >р (а, с)) и Ф(а,Ь,С) >р(а,Ь)=с перейдут в некоторые выводимые формулы 1). г) См. сделанное ранее замечание отиосительио зызодимости формулы 6 (а, Ь) а = г„ Ю (х, Ь) (с. 472). Вообще, эквивалентность э( (а) — = г„з( (х) можзт быть таким образом зызедепа для любого терка г гй (х). б«о ПОНЯТИЕ етот, КОТОРЫПэ П ЕГО УСТРАНИМОСТЬ ~ГЛ УП1 следствия из устРАнимости хАРАктеРистик 541 Теперь устранение «-герма «„Ф (а, Ь, х) оказывается равносильным устранению ~р (а, Ь).
Если мы произведем устранение герма «„.Ф (а, Ь, х), то вместо любой построенной по правилам формализма 6 формулы, содержащей функциональный символ «р (,.), мы получим «представляющую» ее формулу формализма [й", получающегося из [Я опусканием функционального символа ~р (, ) и аксиомы К(а, Ь, с, <р (а, Ь), ~р (а, с)) и добавлением предикатного символа Ф, а также трех сформулированных для него аксиом. Если формула, построенная по правилам [й, выводима средствами этой системы, то представляющая ее формула будет выводима средствами [Я*, и наоборот. Действительно, одна выводимость следует из другой с учетом «-правила; но так как результирующая формула «-символов не содержит, то применение «-правила может быть устранено.
Тем же самым способом мы можем убедиться в том, что в формализме, получающемся иэ [Я путем присоединения явного определения Ф (а, Ь, с) ~р (а, Ь) = с, формула, не содержащая функционального знака ~р (, ), выводима тогда и только тогда, когда она выводима в [сэ. Таким образом, формализмы Я и [Яэ оказываются равносильными в этом смысле слова. Этот результат может быть немедленно распространен на случай произвольного числа функциональных знаков (с произвольным количеством аргументов) и произвольного числа аксиом для этих функций.
Под этот случай подпадают и индивидные символы, так как их можно рассматривать как функциональные знаки без аргументов. Итак, мы убеждаемся, что если за основу рассмотрения взять исчисление предикатов и аксиомы равенства, то всякая система аксиом, содеря«ащая только собственные аксиомы и, быть может, аксиому индукции, будет равносильна такой системе аксиом, в которой функциональные и индивидные символы отсутствуют.
Замена системы аксиом рассмотренного типа, формализованной с применением функциональных знаков, равносильной системой аксиом без функциональных знаков дает, в частности, возможность (в том случае, если аксиома индукции среди аксиом не встречается) свести проблемы выводимости в этой системе и ее непротиворечивости к некоторым частным проблемам раарешимости в исчислении предикатов ~).
Исключение индивидных символов не дает в этом смысле никаких преимуществ. Вообще, замена инднвидного символа представляющим его преднкатным символом по большей части ') См. гл. 1Ч с. 199 — 20О. нецелесообразна, и исключение такого символа мы будем производить лишь тогда, когда будет удаваться явным образом определить этот символ с помощью некоторого «-терма и, значит, беэ введения какого-либо нового предикатного символа. 3. Применение этой процедуры к системе (Х); перспективы дальнейших исследований.
Мы проиллюстрируем переход от функциональных знаков к представляющим их предикатным символам в том виде, как он происходит при помощи мтермов, а также и процедуру исключения индивидных символов при помощи явных определений на примере системы (Е). В системе (У) у нас имеются функциональные знаки а, а + Ь, а Ь. При помощи эквивалентностей (Ц Яц (а, Ь) а' = Ь, (2) Ай (а, Ь, с) а + Ь = с, (3) Мр (а, Ь, с) а- Ь = с мы сопоставим этим знакам предиватнме символы Яс[, Ай и Мр. Если эти эквивалентности рассматривать как явные определения указанных предикатных символов, то иэ них для каждого из этих символов с помощью аксиом равенства могут быть выведены соответствующие формулы единственности по последнему аргументу. Сейчас мы, наоборот, возьмем эти формулы единственности в качестве аксиом.
Тогда при помощи «-правила мы сможем ввести термы «„. Я «[ (а, х), «, Ай (а, Ь, х) и «„ Мр (а, Ь, х), и если мы возьмем равенства П1 а' = «„Я«[ (а, х), [2) а+Ь= «„Ай(а,Ь,х), [3] а Ь = «„ Мр (а, Ь, х) в качестве явных определений, то формулы (1), (2), (3) окажутся выводимыми. Теперь, для того чтобы из системы (Х) получить такую систему аксиом, в которой вместо указанных трех функциональных знаков фигурируют сопоставленные им предикатные символы, нам остается только удалить, применив эквивалентности (1), (2), (3) и равенства [11, [2], [31, эти функциональные знаки из аксиом, в которых они встречаются [т. е. из аксиом (Рг), (Р ), рекурсивных равенств для а + Ь и а Ь и аксиомы индукции[, а затем устранить «-термы.
Процедура эта принимает следующий вид: Аксиомы (Рг) и (Р,) с помощью эквивалентности (Ц могут быть переведены в формулы чЯц (а, 0) 545 ПОНЯТИЕ»ТОТ, КОТОРЫЙ» И ЕГО УСТРАНИМОСТЬ ИГЛ Чзп $ ы следстВия из устРАнимости хАРАктеРистик 543 Яч (а, ь') — а = ь, вторая из которых с помощью [1] может быть затем переведена в формулу ЯЧ (а, в„ БЧ (Ь, х)) †» а = Ь, а из нее, исключив ~-символ, мы получим формулу ЯЧ (Ь, с) -~- (ЯЧ (а, с) — ~- а = Ь), которая допускает элементарное преобразование в ЯЧ (а, с) А ЯЧ (Ь, с) -+.
а =- Ь. Рекурсивные равенства для а.+ Ь с помощью эквивалентности (2) могут быть переведены в Ай(а,О, а) Ай (а, Ь', (а + Ь)'); вторая из них с помощью [1] и [2] может быть переведена в формулу Ай (а, с„ЯЧ (Ь, х), с„ЯЧ (ьзАй (а, Ь, у), х)), из которой исключением 1-символов и элементарными преобразованиями мы получим формулу Ай(а, Ь,с)»ХЯЧ(Ь,Р)»ХЯЧ(с,г)-~Ай(а,г,г). Совершенно аналогичным образом вместо рекурсивных равенств для а Ь с помощью (3) и [1], [2], [3] могут быть получены формулы Мр (а, О, 0) Мр(а, Ь,с) 8»ЯЧ(Ь, г) 8 Ай(с, а,з) — »Мр(а, г,г). Аксиома индукции с помощью [1] может быть переведена в формулу А (0) 8с чх (А (х) -1- А (ЗРЯЧ (х, у))) — » А (а), а из нее в результате устранения ~-символа и простых преобразований мы получим формулу А (О) А 'Ух Чу (ЯЧ (х, у) 8~ А (х) -»- А (у)) »- А (а).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
