Математическая логика, основанная на теории типов (стр. 9 )

├ : . fx . ºx . yx : É : f{(fz)} . º . f{(yz)},

следовательно, применяя определение тождества к фиктивным объектам (fz) и (yz), данное выше, мы находим, что

├ : . fx . ºx . yx : É . (fz) = (yz).

Это утверждение, а также его конверсия (что также можно доказать), указывает отличительное свойство классов. Следовательно, мы вполне можем трактовать (fz) как класс, определяемый посредством f. Тем же самым способом мы устанавливаем

f{y(x, y)} . = : ($f) : f!(x, y) . ºx, y . y(x, y) : f{f!(, )} Df.

Здесь необходимо несколько слов относительно различия между f!(, ) и f!(, ). Мы будем принимать следующее соглашение: Когда функция (в противоположность своим значениям) представлена в форме, включающей и (или какие-то другие две буквы алфавита), значение этой функции для аргументов а и b должно обнаруживаться подстановкой а вместо и b вместо ; т. е. аргумент, упоминающийся первым, должен подставляться вместо буквы, которая встречается в алфавите раньше, а аргумент, упоминающийся вторым, – вместо буквы, которая встречается позднее. И это вполне удовлетворительно проводит различие между f!(, ) и f!(, ); например:

Значение f!(, ) для аргументов а и b есть f!(а, b).

Значение f!(, ) для аргументов b и а есть f!(b, а).

Значение f!(, ) для аргументов а и b есть f!(b, a).

Значение f!(, ) для аргументов b и a есть f!(a, b).

Мы устанавливаем:

хÎf! . = . f!х Df.,

следовательно,

├ : . xÎ(yz) . = : ($f) : f!y . ºy . yy : f!x.

К тому же, по аксиоме сводимости мы имеем

($f) : f!y . ºy . yy,

следовательно,

├ : xÎ(yz) . º . yx.

Это имеет силу при любом х. Предположим теперь, что мы хотим рассмотреть (yz)Î f{(f!z)}. Согласно изложенному выше, мы имеем

├ : . (yz)Î f{(f!z)} . º . f{(yz)} : º : ($f) : f!y . ºy . yy : f(f!z),

отсюда

├ : . (yz) = (cz) . É : (yz)Îx . ºc . (cz)Îx,

где х записывается вместо любого выражения формы f{(f!z)}.

Мы устанавливаем:

cls = {($f} . a = (f!z)} Df.

Здесь cls обладает значением, которое зависит от типа мнимой переменной f. Следовательно, пропозиция ‘cls Î cls’, например, являющаяся следствием приведённого выше определения, требует, что ‘cls’ должно обладать различным значением в двух местах, где оно встречается. Символ ‘cls’ может использоваться только там, где необходимо знать тип; он обладает неопределённостью, которая приспосабливается к обстоятельствам. Если мы вводим как неопределяемую функцию ‘Indiv!x’, означающую ‘x – индивид’, мы можем установить

Kl = {($f} . a = (f!z . Indiv!z)} Df.

Тогда, Kl – это определённый символ, означающий ‘класс индивидов’.

Мы будем использовать строчные буквы греческого алфавита (иные, чем Î, f, y, c, q), чтобы представлять классы любого типа, т. е. обозначать символы формы (f!z) или (fz).

С этого пункта теория классов во многом развивается как в системе Пеано; (fz) заменяет zэ(fz). Также, я устанавливаю:

a Ì b . = : xÎa . É . xÎb Df.,

$!a . = . ($x) . xÎa Df.,

V = (x = x) Df.,

L = {~(x = x)} Df.,