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