Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 117
Текст из файла (страница 117)
Явные определения мы поначалу не будем включать в этот формализм. У нас будут фигурировать следующие виды переменных: 1) сво-, бодные и связанные индивидные переменные, 2) свободные и связанные функциональные переменные, причем это будут исключительно переменные с одним аргументом, 3) свободные формульные переменные без аргументов и с аргументами. Индивидные и формульные переменные будут обозначаться так же, как и до сих пор) свободные и связанные функциональные переменные будут отличаться от индивидных точкой наверху.
3 а меч а н и е. Функциональные переменные будут играть роль переменных для Агагпелгалгпческих функций. Связанные формульные переменные мы здесь не вводим. В качестве символов у нас будут фигурировать индивидный, символ О, штрих-символ, одноместный функциональный знак б,; знак равенства, символы исчисления высказываний и е-символ. Связанная переменная, относящаяся к е-символу, может быть* либо индивидной, либо функциональной. Понятие формулы мы определим рекурсивно, совместно с понятиями терл!а и функ!(ионалав).
Замысел нашего определения состоит в том, что понятие терма должно будет формализовать у нас понятие числа, понятие функционала — понятие арифметической функции, а понятие формулы — понятие высказывания. В качестве терм о в мы сначала возьмем свободные индивидные переменные, символ О и выражения вида а' и 6(а), где а— ') А с 1г е г гп а п п гхг, Венгцпбцпя дев,1ег!Шгп поп да1цг' пг!!!е!в бег Н!! ° Ьегмсиеп тиеог!е бег цг!бегвргцсйв1ге!Ье!!.— Мапц Апп., !924, эа, № !!З, в) В первых гильбертовских публикациях по теории доказательств,' а также в диссертации Аинермана термин фу н к ц и о н а л употреблялсй' в том смысле, в каком мы здесь говорим о те р мах.
ОПИСАНИЕ ОДНОГО ФОРМАЛИЗМА 547 В качестве исходных формул н возьмем следующие формулы: 1) все тождественно истинные форму зываний; 2) формулы А(а) — А(з А (х)), А (а) -в- Е„А (х) Ф а', А(г!)- А(в;А (Р)), которые мы будем называть первой, второй и третьей е-формулами соответственно; 3) аксиомы равенства (дв) и ()в); 4) арифметические аксиомы а' = Ь' -ы а = Ь, а'~О, ач" О- 6(а)'=а, Выводы мы будем строить с помощью операций подетт а н о в к и вместо свободных переменных, п е р е и м е н о в а н и я связанных переменных и повторения формул.
Будет примениться также схема заключения. Переименование связанных индивидных переменных определяется, как прежде. Аналогично, переименование связанной функ- 18" терм, а в качестве ф у н к ц и о н а л о в — функциональные переменные сами по себе, т. е. без каких бы то ни было аргументов. Кроме того, термами будут считаться любые выражения вида а (Ь) или (о)(б), где а — функционал, а Ь вЂ” терм. (Скобки вокруг а требуются в том случае, когда а представляет собой какое-либо составное выражение.) Элементарными формулами мы будем считать: формульные переменные без аргументов, формульные переменные с аргументами, каждый из которых является либо термом, либо функционалом, и равенства между термами.
Формулами мы будем считать выражения, которые либо являются элементарными формулами, либо строятся из элементарных формул с помощью связок исчисления высказываний. И, наконец, в качестве термов мы будем также допускать выражения вида в 6(ф), где р!(и) получается из формулы р!(г), содержащей свободную индивидную переменную с и не содержащей связанной переменной р, в результате замены г посредством р. Аналогично в качестве функционалов мы будем допускать выражения вида е р((р), где 6(р) получается из формулы 6(!), содержащей свободную функциональную переменную г и не содержащей связанной переменной р, в результате замены г посредством е, ашего формализма мы лы исчисления выска- пм' ПРИЛОЖЕНИЕ 648 ОПИСАНИЕ ОДНОГО ФОРМАЛИЗМА 649 циональной переменной состоит в замене выражения е 6(х) выражением е Я())), где р — какая-либо отличная от е связанная р функциональная переменная. Подстановка вместо свободных индивидных переменных и вместо формульных переменных без аргументов определяется, как прежде.
При подстановках вместо формульных переменных с аргулсгнтами мы должны учитывать то обстоятельство, что различные их аргументные места могут заполняться по-своему. С этой целью мы введем следующие понятия. Две переменные — одну свободную и одну связанную — мы будем называть односортными, если они обе индивидные или обе функциональные. Выражение мы будем называть к в азитермом, если оно либо является термам, либо получается из терма в результате замены одной или нескольких его свободных переменных не входящими в данный терм, связанными переменными, односортными с заменяемыми перемен- ' ными. Выражение мы будем называть к в азифу н кцион алом, если оно либо является функционалом, либо получается из функ- ' ционала в результате замены одной или нескольких его свободных переменных не входящими в данный функционал связанными переменными, односортными с заменяемыми переменными.
Как легко убедиться, в качестве аргументов формульных пере-, менных любой формулы могут фигурировать лишь квазитермы и . квазифункционалы. Имен н а я форма для формульной переменной с аргументами состоит из формульной переменной, аргументами которой*: являются одни только попарно различные свободные индивидные или свободные функциональные переменные. В а р и а н т о м дан-: ной именной формы мы будем называть выражение, получающееся из этой именной формы в результате замены любой ее индивид- .
ной переменной каким-либо квазитермом и любой функциональной переменной — каким-либо квазифункционалом. 3 а м е н и т е л е м ' для данной именной формы является формула, содержащая все аргументные переменные этой именной формы. Подстановка вместо формульной переменной с аргументами в формулу о производится с помощью какой-либо именной формы, для которой указан соответствующий заменитель. Выполнение подстановки заключается в том, что вместо любого фигурирующего в 5 варианта этой именной формы подставляется выражение, которое получается из указанного заменителя при помощи тех же самых замен, при помощи которых из этой именной формы получается рассматриваемый нами ее вариант.
Если Я вЂ” именная форма, а Я вЂ” соответствующий заменитель, то мы будем говорить, что' производится подстановка в формулу 5 формулы Я вместо именной формы 81. Мы будем рассматривать два типа подргпаноок вместо функНиональных переменных. Подстановка первого типа состоит в замене данной переменной всюду, где она фигурирует в рассматриваемой формуле, данным функционалом (и од с т а н о в к а ф у н к ц и о н а л а). Подстановка второго типа (п од с т а н о в к а фун кци и) аналогична подстановке вместо формульной переменной с одним аргументом, являющимся квазитермом. Если а — рассматриваемая функциональная переменная, то для какой-либо ее именной формы о(с) со свободной индивидной переменной с указывается ее заменитель, т.
е. соответствующий терм 1(с), а затем в формуле, в которой производится подстановка, каждое входящее в нее выражение е (г) заменяется соответствующим выражением 1(г). При этом предполагается, что функциональная переменная в в рассматриваемой формуле не фигурирует сама по себе, а каждый раз встречается обязательно с (одннм) аргументом. Замечание. Мы могли бы обойтись без подстановкифункцнй, если бы вместо нее взяли схему формул :-(х)уг(х(г) =1(г)), применяемую ко всякому такому содержащему переменную г квазитерму 1(г), для которого 1(с) является термом'). С другой стороны, в принципе мы могли бы обойтись и одной подстановкой функций.
Правда, при этом мы лишились бы ряда удобных изобразительных возможностей. Допустимость подстановок и переименований, как обычно, связывается с условием недопущения коллизий между связанными переменными, так что внутри какого-либо выражения а 21(р) или е 6(г) никогда не должен встречаться какой-либо другой а-символ, относящийся к той же самой связанной переменной нли е. Во избежание коллизий между связанными переменными подстановки в любую из е-формул всегда будут производиться одновременно с необходимыми переименованиями связанных переменных. Описанный таким образом формализм мы будем называть формализмом Н,.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
