Использование Расселом типичной двусмысленности

Теория типов, описанная в [18], является разветвленной теорией, но то, что существенно для его
использования типичной неоднозначности, там лучше всего объясняется в терминах простой теории типов
(СТТ) с аксиомой Бесконечности. Таким образом, типы индексируются натуральными числами
0

, 1, 2,... с объектами типа 0, интерпретируемыми как индивиды (бесконечное число)

и для каждого из них

n, объекты типа n + 1 интерпретируются как все классы объектов типа n.

Мы используем:

x, y, z,... в качестве переменных для любого типа n = 0 и соответствующий список переменных

X, Y, Z,... типа n + 1.

3

Только атомарные формулы вида

u ∈ W, где u имеет вид

некоторый тип

N и W следующего типа n + 1 считаются значимыми.

Первое место, на котором возникает вопрос о двусмысленности в [18], находится на стр. 251 (или стр. 174

в его переиздании в [20]). Для любого типа

n = 0, он определяет Cls

4

чтобы быть классом всех

классы объектов типа

n-1 и затем пишет::

... предложение ' Cls

∈ Cls '... требует, чтобы " Cls " имел разное
значение в двух местах, где это происходит. Символ " Cls " может
использоваться только там, где нет необходимости знать тип; он имеет двусмысленность, которая
приспосабливается к обстоятельствам.

Чуть ниже он определяет пустой класс

и универсальный класс

V и говорит
, что, как и Cls, эти символы неоднозначны “и только тогда приобретают определенное значение, когда
соответствующий тип указан иначе.” В нашей обстановке это конкретные объекты
типа

n. переходя оттуда, Рассел определяет булевы операции x ∪ y, x ∩ y,

и

- x; это последнее, конечно, дополнение относительно V. Позже в этой статье он написал:

определяет Cl

(x) быть классом всех подклассов x; это, таким образом, объект типа n + 1.

Экстенсионально Cls - это то же самое, что и Cl

(В).

Теория типов была создана для того, чтобы сохранить логистическую программу от incon-

системность, в частности, чтобы избежать парадокса Рассела. Использование переменных

x, y, z,...
неопределенного типа и только что объясненные понятия иллюстрируют использование, когда это необходимо,
типичной двусмысленности, чтобы вернуться к базовой структуре типа для обеспечения безопасности, которую она
обеспечивает (“имея свой торт”), возвращая как можно больше свободы неформальной
теории классов (“съедая его тоже”).

Расширение вышеупомянутой формы STT до теории отношений (как в теории Рассела)

можно определить отношение

x ∼ y для удержания, когда классы x и y находятся один к одному

переписка. Затем Рассел определяет:

N c(x), чтобы быть классом всех y таких, что x ∼ y,

т.е.,

Nc(x) - это класс эквивалентности x под ∼; Он имеет тип один выше, чем это

от

x. класс кардинальных чисел NC затем принимается за класс всех Nc(x)

для

X ∈ Cls; он имеет тип n + 2 для x типа n. члены 0, 1, 2,... из НК

далее вводятся, соответственно как

N c (), Nc ({0}), N c ({0, 1}) и так далее. Из них:

определения, пишет Рассел:

3

Рассел использует

α, β, γ,... для переменных класса и x, y, z,... для переменных для их элементов. Наш

на выбор:

X, Y, Z,... для переменных класса типа n + 1 было сделано так, чтобы можно было легче сравнивать

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

4

В [18] Рассел писал: ‘

cls', где я пишу " Cls "; последнее используется в Principia Mathematica.

138

С. Феферман

Следует отметить... что 0 и 1 и все остальные кардиналы... являются
неоднозначными символами, такими как Cls, и имеют столько же значений, сколько
и типов. Начнем с 0: значение 0 зависит от того, что из

, и

значение этого слова

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

Частичный выход Рассела из этой неловкой ситуации заключается в том, чтобы отметить, что если классы

икс

и

y имеют различные типы, например x типа n и y типа n + 1, то мы можем

говорят о том, что

x и y, имеющие одинаковое кардинальное число или один, имеющий больший кардинал

номер чем другое путем сравнивать

y с классом синглетов {u} для u ∈ x.но
это все еще не выходит из того факта, что у одного есть множество представителей
кардиналов и, в частности, натуральных чисел. В какой-то степени использование типичной
двусмысленности является способом сохранения лица в этом отношении.

5

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

форма

A ∈ B, которые имеют неопределенный тип, но где prima facie тип A является

больше или равно этому из

Б. Рассел сам сигнализировал об этом вопросе, когда предлагал

как обращаться с псевдо-оператором Cls

CL Cls; один просто интерпретирует второй

возникновение ' Cls ' как класса всех классов типа

n + 1, когда первый

возникновение интерпретируется как класс всех классов типа

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

V ∈ V, снова узаконенный путем смещения интерпретации

второй ‘

V ' на один тип выше.

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

Inf

∈ Inf, Fin ∈ Inf, Inf /

∈ Fin, Fin /

∈ Плавник,

(1)

где Fin, Inf определяются соответственно как класс всех конечных классов и
класс всех бесконечных классов. То же самое можно сказать и о высказываниях:

{1}

∈ 1, {2} ∈ 1, {1} /

∈ 2, {1, 2} ∈ 2.

(2)

5

Ссылка предположил, что что-то вроде лечения смысл indexicals на естественном языке
(как указано в примечании 3 выше), могут быть применены к понятию числа в теории типов: можно
сказать, что смысл ряда терминов, всегда такое же, как определено с помощью выражения со связанными класса
переменных, но это только в “типичных” условиях (а именно данного типа уровень) определяет, какие классы
связаны. Хотя я не выдвигаю здесь никакой теории значения, в некотором смысле это то, что сделано в разделе 3,
где значение определяется формулой

ϕ. Но дополнительная проблема возникает при встрече с такими
примерами, как (1), (2) в п. 2, поэтому необходимо сделать еще кое-что для уточнения интерпретаций терминов
в формулах вида

A ∈ B, если оба A и B содержат одни и те же термины, например, {1, 2} ∈ 2. Вот что это такое

предполагается, что Конвенции о неразглашении должны заботиться.

Типичная Двусмысленность

139

3. Устранение двусмысленности утверждений о членстве
в теории типов

Неоднозначные выражения, такие как Cls,

,

V, 0, 1,... может быть присвоено много типов в STT;
они являются примерами выражений, которые стратифицированы в смысле Куайна, т. е. являются результатом
стирания индексов типов из всех переменных выражения STT (сохраняя переменные
различных типов непересекающимися друг от друга). Дано выражение

S из STT, пусть e(S)

быть результатом стирания всех индексов типа из переменных типа:

S. Для a стратифицированный

выражение пусть тип

(A) быть наименьшим n, для которого существует S типа n с A = e(S);

это то, что мы называем prima facie типом

A. Мы будем путать стратифицированное выражение
с самым низким выражением STT, из которого оно получается путем стирания различий типов.
Расплывчатость выражений формы

A ∈ B, где Тип A больше

чем или равны к тому из

B сначала делается здесь для особого случая, что они имеют то же самое

тип и

B-выражение вида {x|ϕ (x)}, где ϕ-стратифицированная формула. Позволь

ϕ

+

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

ϕ по соответствующей переменной next

более высокий тип, и после этого препятствуйте

Б

+

быть

{X / ϕ

+

(Икс)}. Тогда Конвенция о неразглашении является

просто:

A ∈ B означает A ∈ B

+

когда тип

А) = тип (B).

(Dis 1)

Таким образом, для

B вида {x|ϕ (x)}, A ∈ B эквивалентно ϕ

+

(Ля). Например,
приведенные выше утверждения (1) могут быть истолкованы как применение (Дис 1). Аналогично, если
A имеет prima facie тип один выше, чем B = {x / ϕ (x)}, Мы согласны со следующим
соглашением о снятии неопределенности:

A ∈ B означает A ∈ B

++

когда тип

(A) = тип(B) + 1.

(Dis 2)

Тогда, например, приведенные выше утверждения (2) могут быть выведены как применение
(Dis 2).

Неоднозначность в видах формул

A ∈ B, рассмотренный здесь, является типичным, поскольку
неоднозначность систематична с использованием принципов (Dis 1) и (Dis 2) в зависимости от
типа

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

А измеряется по сравнению с тем, что из B, до тех пор, пока все

типы сдвигаются на ту же величину. Это происходит из-за простой:

Теорема 1. Если предложение есть

θ доказуемо в STT, то так же, как и θ

+

.

Отсюда следует, что если

A ∈ B доказуемо в STT, где A, B задаются замкнутыми членами,

тогда так и есть

Один

+

∈ Б

+

. Что еще более важно, если

A ∈ B доказуемо, то каждое свойство

из элементов которых:

B также держит A. это сформулировано как:

Теорема 2 (правило переноса). На закрытые сроки

A, B, C с B = {x|ϕ (x)} и C =
{x|ψ (x)} и типом (A) = типом (B), если A ∈ B и B ⊆ C доказуемы в STT, то так
же верно

A ∈ C.

140

С. Феферман

Доказательство. Это потому, что

A ∈ B означает ϕ

+

(Ля). Поскольку ∀x[ϕ (x) → ψ (x)] является Тео-

Рем, так и есть

∀Х[ϕ

+

(X) → ψ

+

(X)], так ψ

+

А) имеет силу, т. е. А ∈ С имеет силу в
соответствии с Конвенцией о запрещении двусмысленностей.