5. Добавление функциональных знаков; понятие терма; выводимые формулы.

На этом мы пока что закончим рассмотрение равенства и связанных с ним аксиом и обсудим расширение еще одного типа. Оно будет состоять в допущении символов для математических функций.

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

Теперь в качестве символов нового типа мы введем знаки для математических функций — мы будем называть их функциональными знаками. В качестве функциональных знаков мы, как правило (т. е. если не будет применяться какой-нибудь специальный общеупотребительный символ), будем использовать строчные

буквы греческого алфавита. Функциональные знаки в формализме будут отличаться от предикатных символов в том отношении, что предикатный символ с приданными ему аргументами представляет собой некоторую формулу (элементарную формулу), в то время как функциональный знак с приданными ему аргументами будет представлять собой некоторый терм. Слово «терм», начиная с этого места, мы будем использовать в качестве общего наименования для таких выражений, которые могут быть подставляемы вместо свободных индивидных переменных.

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

1. Свободные индивидные переменные.

2. Индивидные символы.

3. Функциональные символы, у которых каждый аргумент представляет собой или свободную индивидную переменную, или какой-либо индивидный символ.

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

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

и

будут термами.

Напротив, выражения типа или в которых встречаются связанные переменные, термами не являются, хотя такие выражения могут, конечно, быть составными частями формул; например,

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

Эффект, проистекающий от обобщения нашего правила подстановки, мы поясним на примере вывода нескольких формул. Мы снова возьмем здесь в качестве функционального знака с одним, а в качестве знака с двумя аргументами. Будем исходить из основной формулы (а)

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

К полученной формуле мы теперь можем применить схему (а) и получить, таким образом,

Если же в исходную формулу (а) мы подставим не а потом опять применим схему то получим формулу

В правой части этой импликации мы можем переименовать переменную х в у и подставить а вместо тогда у нас получится

Применив схему (а) еще раз, мы получим формулу

Эти выводы существенно используют то обстоятельство, что в формуле (а) имеется формульная переменная с аргументом. Аналогичные выводы можно построить, основываясь на формуле (Ь) и схеме

Еще одной исходной формулой, содержащей формульную переменную с аргументом, является вторая аксиома равенства

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

то получится формула

а из этой последней — перестановкой посылок —

Если мы теперь учтем формулу

которая получается из формулы в результате подстановки, то, применив схему заключения, получим формулу

Совершенно аналогичным образом можно вывести следующие две формулы:

производя подстановки во второй из них, мы получим

а из формулы

в результате подстановок получается

Эта формула вместе с двумя предшествующими

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

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

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

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

а отсюда подстановками получим

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

На этом мы закончим рассмотрение формального аспекта введения функциональных знаков. Что же касается содержательного истолкования, то надо сказать, что с этой точки зрения функциональным знакам будут соответствовать математические функции. Эти функции отличаются от логических функций, т. е. от предикатов, тем, что значения их снова являются элементами индивидной области, в то время как значение любой логической функции всегда представляет собой одно из двух истинностных значений -«истина» или «ложь».