Теория разветвленного типа и ее семантика

Чтобы облегчить сравнение с логикой 1925 года, в этом разделе представлена версия
теории разветвленного типа ("irt" - издание I, R amified T ypes), обычно следующая
Церкви [9], но сформулированная с абстракциями (и правилами

β-преобразование) вместо
постижения аксиом. Во втором подразделе обсуждается статус принципов экстенсиональности
и мотивация для использования рефератов, а в третьем разделе представлена” замещающая "
интерпретация. Четвертый делает экскурс в теорию доказательств.

Логика irt:

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

я, конечно

urelements или индивиды, и для каждой конечной последовательности типов

т

1

,..., Т

н

тип

(t

1

,..., Т

н

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

типы

т

1

,..., Т

н

:

n-адические соотношения (свойства в случае n = 1) или, если мы предполагаем

объемность,

n-адические отношения-в-расширении (классы в случае n = 1). Мы включаем:

также случай последовательностей нулевой длины, дающих тип

() из предложений или, предполагая

экстенсиональность, истинностные ценности.

"Конструктивное" расширение теории разветвленных типов

455

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

() отдельно стоящий подсчет как Формулы;

все остальные атомарные формулы имеют вид

А[b

1

,..., б

н

], где b

1

,..., б

н

оставаться свободными

переменные (или константы) соответствующих типов

т

1

,..., Т

н

, и

a-свободная переменная (или

константа) типа

(t

1

,..., Т

н

). Неатомные формулы формируются обычными способами, путем
объединения формул со связями или путем прохождения через формулу, заменяя каждое
вхождение в ней некоторой одной свободной переменной вхождениями связанной переменной (еще не
встречающейся в Формуле) того же типа и предваряя Квантор этой
связанной переменной в качестве операторной переменной. (Другими словами: Я принимаю конвенцию Гильберта и Гентцена
, в соответствии с которой связанные и свободные переменные нотационно различны, связанные
переменные не встречаются свободно в хорошо сформированных формулах и кванторах с одинаковыми значениями
переменная оператора никогда не имеет перекрывающихся областей.) Предложения, как обычно, являются формулами, не
содержащими свободных переменных, квази-формулами, такими как Формулы, за исключением содержащих
несвязанные вхождения связанных переменных в местах, где они должны иметь свободные
переменные.

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

А-это квази-формула, содержащая

свободные вхождения не связанных переменных, кроме

икс

1

,..., икс

н

, из видов

т

1

,..., Т

н

ре-

спективно,

{икс

1

,..., икс

н

: A} является абстрактным типом (t

1

,..., Т

н

), и может происходить в любой
среде, в которой может иметь место свободная переменная или константа такого типа (а
также вхождения

икс

1

,..., икс

н

в случае возникновения

{икс

1

,..., икс

н

: A} в Формуле учитываются как

связанный в Формуле). Мы можем сделать нашу форму машинного оборудования путем говорить то, где

Один

есть такая формула,

{A} является абстрактным типом (). Как известно (ср. [41] для обсуждения),
абстракты исключаются контекстуальным определением, если предполагается экстенсиональность. Они
вообще не устраняются без этого предположения, а в некоторых приложениях дают
полезное увеличение выразительной силы. Обратите внимание, что каждое вхождение связанной переменной
в абстракте либо связано в Формуле, следующей за двоеточием, либо является вхождением
одной из переменных, предшествующих двоеточию. Повторное формирование рефератов или
количественное определение формул, содержащих рефераты, может привести к появлению квазиабстрактов,
выражения, подобные абстрактам, но содержащие свободные переменные, которые не являются ни операторными
переменными абстрактного, ни связанными операторами внутри абстрактного.

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

Тион с бесконечно большим числом сущностей типа

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

456

А. П. Хазен

правила естественной дедукции или последовательного исчисления для связок и кванторов (правила
кванторов для переменных и констант каждого типа), как в [14]. Эти правила сами по
себе, однако, не позволяют нам доказать, что существует пропозициональная функция
, выраженная какой-либо данной формулой. Как уже говорилось, правила квантификатора позволяют заменять свободные
переменные и константы (если таковые имеются) на связанные переменные более высоких типов:
необходим какой-то способ замены формул.

Здесь возможны два общих подхода. Один из них-постулировать аксиомы
понимания. Это удовлетворительно, если предположить экстенсиональность, но кажется
недостаточным без этого предположения: пропозициональная функция, содержащая все и только те
(последовательности) элементов, которые удовлетворяют формуле, которая является тем, что дает аксиома
понимания, не может быть пропозициональной функцией, выраженной этой формулой. В
неэкстенсиональном случае эту трудность можно обойти
, обогатив язык неистинной функциональной связкой пропозиционального тождества и формулирования
постижение аксиомы с этой Связной, а не материальной эквивалентностью, как
в [8] и [10] и (вслед за церковью) [1] и [2]. Более простой альтернативой, которая будет
следовать здесь, является дополнение утверждения правил кванторов для типов, отличных
от

i, с определением того, что значит подставлять формулу для переменной, как в
(первой части) [8]. Учитывая сложность этого понятия, более удобно
вводить абстракты в качестве вспомогательных обозначений.

Постулируйте, следовательно, правила игры

β-преобразование для обработки рефератов: формулы, полученные из

один другого мимо

β-преобразование (последовательности, полученные друг от друга путем замены a

формула по одному полученному из нее путем

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

λ-исчисление, β-конвертируемость разрешима. При значительных затратах-
деривации становятся намного длиннее-мы могли бы получить тот же самый эффект, постулируя простые
правила абстрагирования и конкретизации.) Затем, устанавливая правила квантификатора, позвольте связанным
переменным заменять абстракты (хотя, конечно, не квази-абстракты), а
также свободные переменные и константы их типа.

[В сторону: даже если гипотезы и вывод из вывод (поставить его в естественной
дедукции условия: в секвенции исчисления сроков, даже если формул в endsequent
доказательства) свободны рефератов, производной, используя эти правила могут содержать формулы
, по существу, содержащий рефераты: то есть формул, которые содержат рефераты, даже когда
сведено к

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

∃X∃ ([X] & X[a]) (с переменными типов

: (i)), X: (i) и a: i) из F [a]:

1.

F [a]

Гипотеза

2.

(F [a] & F [a])

1, & Введение

3.

({x: F [x]} [a] & F [a])

2,

β-абстракция

"Конструктивное" расширение теории разветвленных типов

457

4.

({X: X[a]} [{x: F [x]}] & F [a])

3,

β-абстракция

5.

∃ ([{x: F [x]}] & F [a])

4,

∃ вступление

6.

∃ ([{x: F [x]}] & {x: F [x]} [a])

5,

β-абстракция

7.

∃X∃ ([X] & X[a])

6,

∃ вступление.

Тезисы, представленные в 3, 4 и 6, являются частью механизма: те, которые были представлены в 3
и 6, не возникнут, если

rule правило введения было сформулировано в терминах правила
замены формул для переменных вместо того, чтобы делать обход через абстракты.
Формула 5, однако, находится в

β-нормальная форма и содержит неприводимый конспект. 7 можно,
конечно, вывести из 1 и другими способами, но это кажется наименее неуклюжим.
Мораль, по-видимому, заключается в том, что можно рассматривать абстракции как простую вспомогательную нотацию для упрощения
формулировки правил дедукции, но что более удобно предоставить им
полное гражданство, расширяя выразительные ресурсы языка, чтобы позволить такие предложения
, как 5. Конец в сторону.]

Экстенсиональная теория простых типов-это разумная формулировка теории множеств: не такая
сильная, как у Цермело, но систематическое использование прописных и строчных букв рабочими математиками
и различение таких выражений, как “семейство множеств”, предполагают
, что на практике математическое мышление является теоретико-типологическим. Неэкстенсиональный вариант, однако,
неадекватен как теория пропозиций и пропозициональных функций: он поддается
семантическим и эпистемическим парадоксам. Рассел перешел к теории, делающей более тонкие
различия типа. Церковь [9] относится к типам разветвленной теории типов как
r -типы.

Следуя учетной записи в [9], мы еще раз начнем с типа

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

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

(i), (i, i), (i, i, i), и

из предложений:,

(), то есть, соответствующее каждому такому простому типу серии типов
(я)/1, (я)/2, (я)/3,..., (я, я)/1, (я, я)/2, (я, я)/3,... и так далее. Это удобно, хотя
и не соответствует букве изложения Рассела, интерпретировать каждую из этих иерархий
кумулятивно, так что, например, сущность типа

(i, i)/3 считается также находящимся

типов

(i, i)/4, (i, i) / 5 и так далее. С перечисленными до сих пор типами мы имеем разветвленную
логику второго порядка, как описано в разделах 58 и 59 Церкви [7]. Цифра
после косой черты в обозначении типа, как говорят, дает уровень типа или объектов
этого типа.

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

((i)/1)/1, (i)/1) / 2,..., свойств, принимающих в качестве аргументов уровень-

458

А. П. Хазен

одни свойства особей, виды

(i, (i)/3)/1, (i, (i)/3)/2,..., отношений между
индивидами и свойств третьего уровня индивидов, и так далее. По кумулятивности
уровней для типов второго порядка, an

(i, (i) / 3) / 1 Может ли физическое лицо соотноситься с подпунктом (i) / 1

или Ан

(i)/2; уровни типов третьего порядка также являются кумулятивными, поэтому an (i, (i) / 3) / 1 будет

быть засчитан, чтобы быть an

(i, (i)/3)/2 также. В логике третьего порядка (и при более высоких типах)
полезно определить еще одно понятие- плохость (Черч [9] использует термин Рассела
order, но это противоречит современной терминологии “

логика n-го порядка")
типа. Индивидуумы определяются как имеющие плохость 0; для других типов плохость является суммой
” худшего " допустимого аргумента для сущности типа с уровнем типа.
Таким образом, тип

(i, (i) / 3) / 1 имеет плохость 4 (= 3, плохость тех (i)/3 сущностей, которые

не

(i) / 2, +1, уровень реляционного типа), и (i, (i)/3)/2 имеет плохость 5.

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

логика n-го порядка для некоторых

натуральное число

н.

Словарь irt будет содержать (свободные и связанные) переменные всех этих типов
и, возможно, константы некоторых из них; о константах и переменных будет сказано, что у них есть плохость
их типа. (Principia Mathematica, которая занималась чисто логическими и
математическими вопросами, не содержит в своем формальном языке никаких нелогических констант. Его
авторы рассматривали этот язык как своего рода скелетный язык, который был бы способен
выражать содержание произвольных мыслей, если бы он был дополнен соответствующими
нелогическими константами, стоящими за предметами непосредственного знакомства.) Атомарные формулы являются
форма

А[b

1

,..., б

н

], где б

я

являются ли термины (константы, переменные или абстракты)

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

тип a: обратите внимание, что плохость
предиката атомной формулы всегда будет больше, чем плохость любого из ее
аргументов. Набор хорошо сформированных формул задается обычным видом рекурсии.
Его дедуктивный аппарат будет включать, как и прежде, обычные правила квантификационной логики
для всех типов, а также правила логического вывода.

β-конверсия. Предполагается, что уровневый аспект r-типов
отражает конструктивную сложность пропозиций и пропозициональных функций, и
именно это мотивирует логическую спецификацию того, какие абстракты могут быть заменены
переменными данного (неиндивидуального) типа.
Прежде чем сформулировать эту спецификацию, будет полезно дать одно предварительное техническое определение. Мы можем заявить следующее::

Фундаментальная спецификация

: При применении Квантификата-

tion и

β-правила преобразования, абстрактный {x

1

,..., икс

н

: A} является заменяемым

для переменной типа

(t

1

,..., Т

н

) / j и плохость k (где k > j), если и

только если...

1. переменные абстракции

икс

1

,..., икс

н

находятся, по порядку, из типов

т

1

,..., Т

н

,

2. отсутствие свободная переменная или константа происходя внутри

А есть зло > k, и

3. каждая связанная переменная, происходящая в

А-это зло строго

Тезисы и расширительность

: Многие приложения irt (включая
предполагаемое применение Рассела для теории разветвленных типов) несовместимы с предположением ex-

"Конструктивное" расширение теории разветвленных типов

459

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

t, единственная аксиома экстенсиональности (с переменными из

типы

: ((t)), X: (t), Y: (t) и x: t):

∀Х∀У (∀Х(Х[х] ↔ Г [Х]) → ∀ ([Х] ↔

[Год ]))

В irt это невозможно, проблема лежит с кванторами двух более высоких типов.
Существует бесконечно много типов,

t) / 1, t)/2 и т.д., о принятии пропозициональных функций

элементы типа

t в качестве аргументов потребуется бесконечно много аксиом с кванторами ∀X∀Y
, переписанными в этих различных типах. Хуже того, каждая из этих аксиом должна
быть бесконечно много раз повторена, причем

∀

переписывается в разные типы

способный принимать аргументы типа

Quan X quan y кванторы. (Другими словами,
аксиома экстенсиональности, уже схематичная в контексте теории типов, становится трижды
таковой!)

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

также определите индивидуальность индивидов по формуле

∀X(X[a] ↔ X[b])

Однако, как указал Рассел, этого будет недостаточно в разветвленной логике: что бы там ни было

уровень выбирается для проведения

Quan Квантор X, соответствующая формула с более высоким уровнем X
не будет выведена из него (эта неразводимость строго установлена в Myhill
[32]). Так что придется добавить еще один бесконечный набор аксиом экстенсиональности:

∀X (X[a] ↔ X[b]) → ∀Y (Y [a] ↔ Y [b])

(с переменными типов

X: (i)/1, Y: (i)/n для n > 1 и x: i). Полученная в результате
экстенсиональная система, возможно, является лучшей версией теории разветвленных типов для использования в
исследовании математической силы разветвленных типов без аксиомы
Сводимости. Он интерпретируется в нашем базовом irt путем введения соответствующих ограничений на все
кванторы более высокого порядка.

Без экстенсиональности использование аксиом понимания не даст такой
гибкой системы, как использование абстрактов. Черч [9] представляет собой нечто вроде Тур-де-Форса,
демонстрирующего, что можно использовать разветвленную теорию типов, чтобы дать интересный
анализ (по крайней мере, некоторых) семантических парадоксов, используя вариант логики
только с аксиомами понимания, но для других целей выразительная сила абстрактов
желательна. Например, использование абстрактов позволяет, чего не делают аксиомы понимания
, естественным образом идентифицировать пропозициональную функцию, выраженную заданной формулой
формальной системы.

Семантика с заместительными кванторами

: Учитывая, что мотивирующая идея
пропозиций и пропозициональных функций структурирует их таким образом, что они параллельны
построению формул формального языка, идея интерпретации
квантификаций более высокого порядка теории разветвленных типов подстановочно была естественной
. Интерпретация такого рода была дана Fitch [13], а подстановочный Интер-

460

А. П. Хазен

с тех пор претации обсуждались рядом авторов. Самые яркие дискуссии
идут в Парсонсе’ [34, 35, 36, 37].

Существуют как концептуальные, так и технические трудности с такой семантикой, которые
мы можем либо игнорировать, либо обходить стороной. Одна концептуальная проблема, вызывающая сомнения в том, что
чисто субститутивная семантика должна рассматриваться как правильная или предполагаемая
интерпретация, была упомянута в первом разделе настоящей статьи: нет никакой
гарантии, что (эмпирические) открытия не приведут нас к дополнению нашего языка
новыми предикатами, выражающими универсалии, которые в настоящее время неизвестны. Также
неясно, как следует формулировать семантику предикатных констант более высокого порядка, таких как
как те, кто выражает интенсиональные понятия, такие как значение или вера. Эта проблема может быть
проигнорирована в контексте сравнения с логикой Рассела 1925 года, поскольку такие константы
были явно исключены из более поздней логики. Наконец, существует проблема
референциально интерпретируемой квантификации над индивидами: если есть безымянные индивиды в
области интерпретации переменных типа

i, как правило, невозможно будет
интерпретировать квантификации других типов в терминах закрытых экземпляров замещения. Эта последняя
формальность была отмечена Парсонсом; для простоты мы можем ограничить рассмотрение
интерпретаций irt над моделями с доменами именованных индивидов.

Модель замещения для irt (без предикатных констант типов, отличных от
(i,..., i)/1), то есть это просто структура в смысле модельной теории
логики первого порядка, интерпретирующей предикатные константы, в которых названы все индивиды. Как и следовало
ожидать, атомарное предложение (семантика имеет дело только с закрытыми формулами!)
истинен тогда и только тогда, когда кортеж объектов, названных его терминами, находится в расширении его
предиката. Это несколько упростит экспозицию (причем, так как существует

β-нормальный

формы разрешимы и т. д., это безвредно), чтобы предположить, что все предложения находятся в

β-нормальный

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

Тогда истинность предложений в целом может быть определена обычным видом рекурсии:

* отрицание истинно, если отрицаемое предложение не истинно;

* конъюнкция (дизъюнкция) является истинной, если оба ее конъюнкта (один или несколько из ее

дизъюнкты) - это правда;

* аналогично для любых других связей, которые вы хотите включить;

* универсальная количественная оценка является истинной, если все ее примеры истинны; и

* экзистенциальная квантификация истинна, если хотя бы один из ее экземпляров истинен, где

* экземпляр квантификации с квантифицированной переменной типа

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

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

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

"Конструктивное" расширение теории разветвленных типов

461

Интуитивно понятно, что эта семантика объясняет истинностное значение каждого сложного
предложения, сводя его к вопросу о истинностных значениях более простых предложений. Это понятие
редукции часто драматизируется с помощью метафоры семантической игры. Чтобы определить
истинностное значение предложения, мы даем его двум всеведущим игрокам: стороннику, который
выиграет, если игра закончится истинным атомарным предложением, и противнику, который выиграет, если
игра закончится ложным атомарным предложением. На каждом этапе игры, если предложение
в игре является конъюнкцией или универсальной квантификацией, противник получает возможность выбрать a
конъюнкт или экземпляр, пытаясь для ложного одного. Если предложение в игре является дизъюнкцией или
экзистенциальной квантификацией, сторонник получает возможность выбора, пытаясь выбрать истинный дизъюнкт
или экземпляр. Если это отрицание, они переходят на другую сторону и играют с отрицаемым предложением;
правила для других связок легко определяются. Начальное предложение истинно, если
сторонник может выиграть, ложно, если противник может.

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

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

его предикат равен 0

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

является

ω · k, где k-плохость переменной

* степень отрицания - это степень отрицаемого предложения или квазиформулы

+ 1

* степень соединения (etc.) на 1 больше, чем класс любого конъюнкта

(...) имеет более высокую оценку

* степень количественной оценки - это степень матрицы.

+ 1.

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

462

А. П. Хазен

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

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

Заметим, что” замещающая “семантика, определенная для irt, является” честной", в отличие
от той, которая утверждалась для теории простых типов в [28]. Как подчеркивалось ранее, когда мы начинаем с
определенного набора примитивных предикатов, в целом будут существовать экзистенциально квантифицированные
предложения, которые непротиворечивы (с дедуктивной системой для irt), но ложны в
субститутивной интерпретации, как определено: такие предложения можно рассматривать как утверждения
о том, что набор предикатов языка неадекватен. С другой стороны, каждая
теорема irt будет верна на семантике: обоснованность дедуктивного аппарата
может быть установлено с помощью обычных видов аргументации. (Полнота, конечно,другое
дело: как известно-ср. [12]—полнота на замещающей семантике не
следует надеяться без бесконечных правил вывода!) Другими словами, это согласуется с
признанием дедуктивного аппарата ИРТ полагать, что чей-то язык имеет
достаточно предикатов, чтобы выразить все способы, которыми индивиды похожи и отличаются друг от
друга. Заместительные интерпретации Леблана, напротив, связаны с не --
стандартные модели (в смысле Хенкина [24]) теории простых типов и могут потребовать
добавления бесконечного числа новых примитивных предикатов к заданному языку
для проверки теорем системы. Леблан, другими словами, получает замещающую
семантику только постулируя неизвестный язык, расширяя тот, с которого он начинает:
конечно, случай воровства, а не честного труда! С другой стороны, семантика
Leblanc & Weaver [29] (а также то, что представлено в Grover [19] в том же томе)
близка к тому, что представлено здесь.

Заметка о сокращении-устранение

: Мера сложности, используемая здесь, тесно связана
с понятием степени Гентцена в [14], которое было использовано для доказательства его Гауптзаца
для логики первого порядка, и почти верно, что после расширения нашего определения до
формул, содержащих свободные переменные, мы можем использовать его для доказательства теоремы о вырезании
для irt. Однако есть небольшое осложнение: поскольку абстракты, заменяемые
для связанной переменной предиката в приложениях правил кванторов, разрешают
содержать свободные переменные той же плохости, простое определение степени, используемое выше
для семантических целей позволяет открытым экземплярам превышать количественную оценку в классе.
Например (где

P и Q-чисто атомарные предложения класса 0, a-индивид

константа или переменная, а также переменные предиката

X и R имеют типы (i) / 1 и (i, i)/1

соответственно),

(P & (Q & ∀xRxa))

имеет ранг

ω + 3, но, после абстрагирования до

{y: (P & (Q & ∃R ∀xRxa))} [a],

"Конструктивное" расширение теории разветвленных типов

463

мы можем сделать вывод:

∃X (X[a]),

а это всего лишь класс

ω + 1, от него же. Для теоретико-доказательственных целей нам нужно немного
более утонченное понятие ранга. Мы можем снова позволить атомарным предложениям (и открытым
формулам также, на этот раз) с константами в качестве предикатов иметь ранг 0, а
функциональные связи и кванторы истинности над индивидуальными переменными могут увеличить ранг
на 1, как и раньше. Оставшиеся два пункта определения изменены на:

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

ω·(2k -1),

где

k-это плохость переменной предиката, и

* степень квантификации с неиндивидуальной переменной в исходном кванторе

является

ω · 2k, где k-плохость переменной, если ранг матрицы меньше

чем

ω · 2k, а в противном случае на 1 больше, чем ранг матрицы.

С этим измененным определением предел степеней хорошо сформированных формул irt

остатки

ω

2

, но теперь открытые, а также закрытые экземпляры количественных оценок будут иметь
более низкий уровень, чем сами количественные оценки. (Доказательство: случай 0:
удаленный Квантор имеет переменную, отличную от самой высокой плохой в Формуле. Тогда
квантификация переменных более высокой степени вредности определит ранг
матрицы, а удаление исходного квантора уменьшит ранг целого на 1.
Случай 1: удаленный Квантор имеет переменную более высокой плохости, чем любая связанная
переменная в матрице, поэтому квантификация имеет ранг вида

ω · 2n. поскольку
связанные переменные в абстрактной замене переменной также будут иметь меньшую плохость,
максимальная оценка для экземпляра будет равна

ω · (2n − 1) + некоторое натуральное число.
Случай 2: в матрице есть дополнительные связанные переменные той же самой плохости. Обратите
внимание, что, исходя из предположения, что формула находится в

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

ω · (2n − 1) + некоторое натуральное число, и поэтому, с точки зрения
вычисления ранга всего экземпляра, будут доминировать субформулы,
правда функционально связанные с ними, которые действительно содержат квантифицированные переменные высшей
плохости. Таким образом, в этом случае, как и в случае 0, ранг экземпляра будет на 1 меньше, чем
у количественной оценки. Конец доказательства.)

С этим пересмотренным определением ранга, следовательно, Hauptsatz для irt может быть доказано
путем повторного истолкования индукции Гентцена на grade как трансфинитной индукции, а в противном
случае принять его доказательство неизменным. (В результате Hauptsatz является для слегка абстрактного

464

А. П. Хазен

формулировка логики, выявление

β-эквивалентные формулы и игнорирование шагов
βабстрации и редукции.) Доказуемость cut-elimination для
теории разветвленных типов была известна по крайней мере со времен Лоренцена [31], но я не знаю легкодоступного
лечения на английском языке. Обсуждение теории разветвленного типа (и системы Акермана
typefree) в Schütte [52] было исключено из английского перевода, но есть
псевдотрансляция (замена идиосинкразического варианта последовательных исчислений Шютте с
таблицами Бет-Смульяна) в Толедо [55].

Логика 1925 Года

В этом разделе мы опишем логику 1925 года (bmt для “приложения B, M odified T Ype
Theory). В первом подразделе описываются мотивирующие идеи и расхождения с
irt

. Во втором (написанном для самостоятельного чтения) приводится формальное описание
БМТ. bmt, представленная во втором подразделе, хотя
и мотивирована экстенсиональной концепцией пропозициональной функции, не содержит принципов экстенсиональности:
в третьем подразделе обсуждается степень, в которой экстенсиональность может быть выражена
добавленными аксиомами или правилами. Четвертый подраздел доказывает существование заместительной
семантики.

Влияние Рамсея и Витгенштейна

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

(*) Сократ не верит этому положению

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