Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 49
Текст из файла (страница 49)
Для любой заданной формулы соответствующей проверкой мы всегда сможем выяснить, является ли она 1-тоя<дественной, соответственно 1-выполнимой е). При этом всякая формула 1- тождественна тогда и только тогда, когда ее отрицание $-выполнимым пе является. Формулу, которая является 1-тождественной для любого мы,какираньше,назовем тон<дественной в конечн о м, а формулу, которая является 1-выполнимой для некоторых определенных 1, мы назовем выполнимой в конечн о м. Мы утверждаем, что обе формулы (11) и (1,) тождественны в конечном. Для формулы (1,) это ясно непосредственно.
Что же касается (1,), то, интерпретируя эту формулу в какой-либо 1-элементной индивидной области и производя подстановку вместо формульной переменной и индивидных переменных, мы придем к формуле й=« — (Я (6) — Я (1)). Теперь, если 6 совпадает с 1, то Я(6) тон<е совпадает с Я(1) и поэтому выражение Я (6) Я (1), а тем самым и вся формула в целом, получает значение «истина»„ если же 6 отлично от 1, то ' принимает значение «ложь», а вся формула в целом снова прини- мает значение «истинаю 233 РАСШИРЕННЫЙ ФОРМАЛИЗМ исчисление пРедикАтов с РАвенством 1гл, ч 234 С учетом приведенных в гл. 1У ') соображений отсюда можно заключить, что все формулы, выводимые в исчислении предикатов с участием аксиом равенства, являются тождественными в конечном.
Отсюда, далее, вытекает, что если мы помимо аксиом равенства добавим какие-нибудь новые 1-тождественные формулы (для произвольного фиксированного 1), то все выводимые в результате этого формулы снова будут $-тождественными. Таким образом, при добавлении одной или нескольких тождественных в конечном формул все выводимые формулы тоже будут тождественными в конечном. В связи со сказанным следует особенно отметить, что при добавлении к исчислению предикатов равенства и свяаанных спим аксиом мы опять не получаем полноты (в том, например, смысле, что всякая формула либо оказывается выводимой, либо, будучи добавлена в качестве исходной формулы, ведет к появлению противоречия).
Действительно, мы внаем '), что уже среди формул простого исчисления предикатов для л1обого числа 1 имеются такие, которые являются 1-тождественными, но не (1 + 1)-тождественными. Всякая такая формула, по только что доказанному, не может оказаться выводимой и в том случае, если мы дополнительно присоединим знак равенства и формулы (г,), (г,) [так как она не является (1 + 1)-тождественной).
С другой стороны, если формулу такого рода присоединить к числу исходных, то снова не получится никакого противоречия; более того, и в этом случае выводимыми окажутся только такие формулы, которые являются г-тождественными. Многообразие тех формул, которые являются 1-, но не (1 + 1)-тождественными, в результате добавления знака равенства становится значительно более широким. Вследствие этого тернет силу теорема о том, что всякая (1 + 1)-тождественная формула является в то же самое время и 1-тождественной, или— иными словами — что всякая 1-выполнимая формула заодно является и (1+ 1)-выполнимой.
В самом деле, используя знак равенства, мы для любого конечного числа 1 сможем при помощи соответствующей формулы выразить тот факт, что рассматриваемая индивидная область состоит в точности из 1 индивидов. И хотя в указанном смысле слова исчисление предикатов с добавленным знаком равенства и с аксиомами равенства окааывается неполным, тем не менее характеризация равенства посредством формул (у,) и (гв) оказывается однозначной в следующем смысле.
Если кроме знака равенства ввести еще один предикат- ') См. гл. 1Ч, с. 160. г) См. с. 159. ный символ а — Ь и ввести для него в качестве аксиом формулы а= — а, а = Ь -г- (А (а) -э А (Ь)), соответствующие формулам (г,) и (г,), то можно будет вывести формулу а =Ь а=Ь. Чтобы убедиться в этом, в силу соображений симметрии достаточно указать вывод формулы а = Ь -~- а =— Ь. В формуле (г,) вместо именной формы А (с) подставим выражение а е. Зто даст нам а = Ь -+. (а — а -~ а = Ь). Переставив посылки, получим а ~ а -~ (а = Ь -+ а = Ь), а эта формула совместно с формулой а е— м а по 'схеме ааключения даст нам требуемую формулу.
Подчеркнем, что вывод этот существенно опирается на то, что оба предиката а =Ь и аме Ь совмещаются в рамках одного и того же формализма. 5. Добавление функциональных знаков; понятие терма; выводимые формулы. На этом мы пока что закончим рассмотрение равенства и связанных с ним аксиом и обсудим расширение еще одного типа. Оно будет состоять в допущении символов для математических функций. До сих пор кроме переменных и логических знаков мы допускали в нашем формализме только предикатные и индивидные символы.
Предикатный символ мы разрешали подставлять вместо формульной переменной с тем же числом аргументов, а индивидный символ — вместо свободной инднвидной переменной. Теперь в качестве символов нового типа мы введем знаки для математических функций — мы будем называть их функциональными знаками. В качестве функциональных знаков мы, как правило (т. е. если не будет применяться какой-нибудь специальный общеупотребительный символ), будем использовать строчные 237 233 ИСЧИСЛЕНИЕ ПРЕДИКАТОВ С РАВЕНСТВОМ 1гл. т РАСШИРЕННЫН ФОРМАЛИЗИ буквы греческого алфавита. Функциональные знаки в формализме будут отличаться от предикатных символов в том отношении, что предикатяый символ с приданными ему аргументами представляет собой некоторую формулу (элементарную формулу), в то время как функциональный знак с приданными ему аргументами будет представлять собой пекоторый терм.
Слово «терм», начиная с этого места„мы будем использовать в качестве общего наименования для таких выражений, которые могут быть подставляемы вместо свободных индивидных переменных. Таким образом, правило подстановки вместо свободных индивидных переменных ') теперь должно быть нами расширено. В качестве тврмов, т. е. в качестве объектов, подставляемых вместо свободных индивидных переменных, мы допускаем: 1. Свободные ипдивидвые переменные.
2. Индивидпые символы. 3. Функциональные символы, у которых каждый аргумент представляет собой или свободную индивидную переменную, или какой-либо индивидный символ. 4. Выражения, которые можно получить, исходя из какого- либо выражения типа 3 (по крайней мере с одной встречающейся в нем свободной переменной), в результате однократного или многократного выполпения операции замены какой-нибудь свободной индивидной переменной выражением типа 3. Так, например, если мы вводим ф как функциональный знак с одним аргументом, «р — как функциональный знак с двумя аргументами, а 1 — как индивидный символ, то выражения ф (ф (а, 1)) ф (ф (а), ф (Ь, ф (1))) будут термами. Напротив, выражения типа ф (х) или ф (х, а), в которых встречаются связанные переменные, термами нв являются, хотя такие выражения могут, конечно, быть составными частями формул; например Зх (ф (х) = ф (а)) ' является формулой, так как по-прежнему будет действовать правило, заключающееся в том, что если в какой-либо формуле заменить встречающуюся в ней свободную переменную связанной, а затем связать всю формулу в целом одноименным квантором всеобщности или существования, то в результате снова получится некоторая формула.
») См. с. 123, 131. Вффект, проистекающий от обобщения нашего правила под- становки, мы поясним на примере вывода нескольких формул. Мы снова возьмем здесь ф в качестве функционального знака с одним, а ф — в качестве знака с двумя аргументами. Будем исходить из основной формулы (а) 17х А (х) -». А (а) исчисления предикатов и подставим в нев вместо а терм ф (а); тогда у нас получится 'т'х А (х) «- А (ф (а)).
К полученной формуле мы теперь можем применить схему (сс) и получить, таким образом, 17х А (х) -+- 'Ух А (ф (х)). Если же в исходную формулу (а) мы подставим не ф (а), а «р (а, Ь), а потом' опять применим схему (а), то получим формулу эхА(х) — ~- т'хА(ф(Ь, х)). В правой части этой импликации мы можем переименовать пере- менную х в у и подставить а вместо Ь; тогда у нас получится эх А (х) -» 'ту А (ф (а, у)). Применив схему (а) еще раз, мы получим формулу 'Ух А (х) — ». )рх)(у А (ф(х, у)). Эти выводы существенно используют то обстоятельство, что в формуле (а) имеется формульная переменная с аргументом.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
