Cтраница 3
Далее, мы воспользуемся тем, что фактически подстановка в формулу с номером т вместо именной формы с номером k будет производиться только тогда, когда формула g содержит в качестве составной части какой-либо вариант этой именной формы или же она сама является ее вариантом. Если в каком-либо входящем в формулу g варианте этой именной формы каждую ( свободную или связанную) индивидную переменную и каждую цифру заменить переменной с номером 2р2т, то рассматриваемая формульная переменная будет иметь только такие аргументы, номера которых не меньше 2р2т и, следовательно, больше номеров аргументов именной формы. [31]
Именная форма для формульной переменной с аргументами состоит из формульной переменной, аргументами которой являются одни только попарно различные свободные индивидные или свободные функциональные переменные. Вариантом данной именной формы мы будем называть выражение, получающееся из этой именной формы в результате замены любой ее индивидной переменной каким-либо квазитермом и любой функциональной переменной - каким-либо квазифункционалом. Заменителем для данной именной формы является формула, содержащая все аргументные переменные этой именной формы. [32]
Именная форма для формульной переменной с аргументами состоит из формульной переменной, аргументами которой являются одни только попарно различные свободные индивидные или свободные функциональные переменные. Вариантом данной именной формы мы будем называть выражение, получающееся из этой именной формы в результате замены любой ее индивидной переменной каким-либо квазитермом и любой функциональной переменной - каким-либо квазифункционалом. Заменителем для данной именной формы является формула, содержащая все аргументные переменные этой именной формы. [33]
Теперь подстановка производится следующим образом. Сначала указывается формула, которая будет подставляться вместо именной формы; эта формула - мы будем кратко называть ее заменителем-должна содержать аргументы именной формы. Затем отыскиваются все вхождения в формулу g таких выражений, которые либо совпадают с именной формой, либо отличаются от нее тем, что вместо некоторых из аргументов именной формы или вместо каждого из них в качестве аргументов стоят другие квазитермы; выражения такого рода мы будем кратко называть вариантами этой именной формы. [34]
Теперь подстановка производится следующим образом. Сначала указывается формула, которая будет подставляться вместо именной формы; эта формула - мы будем кратко называть ее заменителем-должна содержать аргументы именной формы. Затем отыскиваются все вхождения в формулу g таких выражений, которые либо совпадают с именной формой, либо отличаются от нее тем, что вместо некоторых из аргументов именной формы или вместо каждого из них в качестве аргументов стоят другие квазитермы; выражения такого рода мы будем кратко называть вариантами этой именной формы. [35]
Теперь подстановка производится следующим образом. Сначала указывается формула, которая будет подставляться вместо именной формы; эта формула - мы будем кратко называть ее заменителем-должна содержать аргументы именной формы. Затем отыскиваются все вхождения в формулу g таких выражений, которые либо совпадают с именной формой, либо отличаются от нее тем, что вместо некоторых из аргументов именной формы или вместо каждого из них в качестве аргументов стоят другие квазитермы; выражения такого рода мы будем кратко называть вариантами этой именной формы. [36]