2. Вложение и подчинение; символы для сокращений.

Теперь посмотрим, какое влияние оказывает i-правило на наш формализм и что мы благодаря этому правилу выигрываем. Прежде всего, мы должны произвести обзор различных термов вида

возникающих на основе применения -правила (такие термы мы будем кратко называть -термами). Большое разнообразие этих термов получается благодаря возможности комбинированных применений -символа; мы будем отличать друг от друга два различных способа комбинирования этих символов: вложение и подчинение.

Речь здесь идет о следующем. Мы исходим из некоторой формулы

Предположим, что в эту формулу вместо мы подставили некоторый -терм Пусть для получившейся в результате этого формулы

которую мы сокращенно обозначим оказались выводимыми формулы единственности, так что в соответствии с -правилом может быть введен терм

Если переменная а не входит в то при связывании 1-символом переменной а в формуле этот терм не затрагивается, т. е. он без изменений входит в в качестве составной части; тогда терм будет иметь вид

В этом случае мы будем говорить, что терм вложен в терм Вообще, мы будем говорить о вложении -терма, когда он в качестве составной части входит в какой-либо объемлющий его -терм.

Если же, напротив, терм содержит переменную а, так что точнее было бы записать его в виде то терм будет иметь вид

В этом случае мы будем говорить, что внешний -символ подчиняет -символ, стоящий внутри формулы, или соответственно, что внутренний -символ подчинен внешнему.

При этом следует заметить, что составная часть

из-за входящей в нее переменной х не является термом, так что мы должны называть ее не -термом, а разве лишь -выражением.

Относительно вложения мы заметим также, что кроме только что указанного случая оно может возникнуть и в результате подстановки. Действительно, такой терм, как

может быть, например, получен в результате подстановки терма вместо какой-либо свободной переменной (скажем, из но, разумеется, только тогда, когда для формулы могут быть выведены формулы единственности по переменной а.

Мы продемонстрируем различные упоминавшиеся возможности комбинирования -выражений на совсем простых примерах относящихся к формализму аксиом равенства и пеановских аксиом

В качестве возьмем сначала формулу

Для нее формулы единственности, относящиеся к переменной а, имеют вид

и могут быть выведены с помощью аксиом равенства. В качестве возьмем формулу

формулы единственности для которой также можно получить при помощи аксиом равенства.

Мы можем теперь построить термы

и

и, подставив второй терм вместо переменной в первый, мы получим терм

в котором выступает в роли вложенного -терма.

Однако этот терм мы можем ввести и непосредственно, выведя формулы единственности для т. е. для

Если мы в качестве возьмем формулу

то соответствующие формулы единственности по переменной а уже не будут выводимы. Но формулы единственности для формулы

будут выводимы, и поэтому выражение

также может быть введено в качестве терма.

В обопх рассмотренных нами примерах мы встречаемся с вложением -термов, но только в первом из них вложение может быть получено также и в результате подстановки.

Если мы теперь возьмем в качестве формулу

а в качестве формулу а, то с помощью -правила выражение

может быть введено в качестве терма и затем с помощью -правила мы получим формулу

При помощи этой формулы с использованием аксиом равенства и аксиомы могут быть выведены соответствующие формулы единственности для формулы

Тем самым мы можем ввести в качестве терма выражение

Мы имеем здесь пример подчинения. Внешний, подчиняющий -символ связывает свободную переменную, входящую в подчиненный терм

Кроме такого способа подчинения, когда переменная какого-либо -выражения непосредственно связывается подчиняющим его 1-символом, существует еще и косвенный способ подчинения, который заключается в том, что какая-либо переменная -выраже-ния свяэывается снаружи каким-нибудь квантором (всеобщности или существования) или же каким-нибудь -символом, а этот в свою очередь находится в области действия какого-нибудь другого -символа.

Подчинение такого типа имеет, например, место в случае терма вида

где переменная у в выражении связывается квантором всеобщности который сам находится внутри рассматриваемого нами -терма.

Другой пример косвенного подчинения представляет собой терм

в котором выражение подчинено всему рассматриваемому -терму через посредство вложенного терма

Возможны и такие случаи, когда прямое подчинение имеет место наряду с косвенным; действительно, различные переменные какого-либо -выражения могут быть связаны по-разному. Так, например, терму

встречающееся в нем -выражение подчинено, с одной стороны, непосредственно (связыванием переменной а с другой стороны, косвенно (связыванием

Как можно видеть уже из этих примеров, в результате комбинирования различных способов сочетания -символов на свет могут появиться чрезвычайно запутанные структуры.

Уже в случае сравнительно простых образований -термы становятся трудно обозримыми. Поэтому для тех или иных часто встречающихся -термов целесообразно вводить с помощью явных определений сокращающие их символы. Такой сокращающий символ в том случае, когда заменяемый им -терм не содержит свободных переменных, будет символом без аргумента, играющим роль индивидного символа. Если же заменяемый -терм содержит свободные переменные, то в соответствии с нашим общим соглашением относительно явных определений сокращающий символ будет содержать встречающиеся в этом -терме свободные переменные в качестве аргументов. При содержательном истолковании этот символ будет изображать некоторую функцию, и если в качестве аргументов будут фигурировать лишь индивидные переменные, то это будет обычная математическая функция.

Если в качестве аргументов будут фигурировать формульные переменные, у которых в свою очередь в качестве аргументов имеется одна или несколько индивидных переменных, то аргументы этих формульных переменных мы будем указывать при помощи связанных переменных, которые будут записываться в виде нижних индексов у зависящего от этих аргументов вводимого знака. Таким способом мы получим символы типа

при этом с содержательной точки зрения

будет изображать функцию, которая всякому предикату с одним аргументом ставит в соответствие некоторый индивид, а

будет изображать функцию, которая любой тройке, состоящей из индивида, предиката с одним аргументом и предиката с двумя аргументами, ставит в соответствие некоторый новый индивид.