Теория типа ST

Мендельсона (1997, 289–293) ST Следующая система представляет собой теорию типа . ST эквивалентен разветвленной теории Рассела плюс аксиоме сводимости . Область количественной оценки разделена на восходящую иерархию типов, в которой всем людям присвоен тип. Количественные переменные варьируются только в пределах одного типа; следовательно, лежащая в основе логика является логикой первого порядка . ST является «простым» (относительно теории типов Principia Mathematica ) прежде всего потому, что все члены домена и кодомена любого отношения должны быть одного и того же типа.Существует низший тип, особи которого не имеют членов и являются членами второго низшего типа. Индивиды низшего типа соответствуют элементам некоторых теорий множеств. Каждый тип имеет следующий более высокий тип, аналогичный понятию преемника в арифметике Пеано . Хотя ST умалчивает о том, существует ли максимальный тип, трансфинитное число типов не представляет трудности. Эти факты, напоминающие аксиомы Пеано, делают удобным и условным назначение натуральное число для каждого типа, начиная с 0 для самого низкого типа. Но теория типов не требует предварительного определения натуральных чисел.

Символами, характерными для ST, являются переменные со штрихом и инфиксный оператор. $\in$. В любой формуле все переменные без штриха имеют один и тот же тип, а переменные со штрихом ( $x'$) варьируются в пределах следующего более высокого типа. Атомные формулы ST : имеют две формы $x=y$ ( личность ) и $y\in x'$. Символ инфиксного оператора $\in$ предлагает предполагаемую интерпретацию , устанавливает членство.

Все переменные, встречающиеся в определении идентичности и в аксиомах «Расширенность» и «Понимание» , охватывают индивидов одного из двух последовательных типов. Слева от ' могут отображаться только переменные без штриха (начиная с «нижнего» типа). $\in$', тогда как справа от него могут появляться только штрихованные переменные (начиная с «высшего» типа). первого порядка Формулировка ST исключает количественную оценку типов. Следовательно, каждая пара последовательных типов требует своей собственной аксиомы Экстенсиональности и Понимания, что возможно, если Экстенсиональность и Понимание рассматривать ниже как схемы аксиом, «охватывающие» типы.

• Идентичность , определяемая $x=y\leftrightarrow \forall z'[x\in z'\leftrightarrow y\in z']$.
• Экстенсиональность . аксиом Схема . $\forall x[x\in y'\leftrightarrow x\in z']\rightarrow [y'=z']$.

Позволять $\Phi (x)$ обозначают любую формулу первого порядка, содержащую свободную переменную $x$.

• Понимание . аксиом Схема . $\exists z'\forall x[x\in z'\leftrightarrow \Phi (x)]$.

Замечание . Любая коллекция элементов одного типа может образовывать объект следующего более высокого типа. Понимание носит схематический характер по отношению к $\Phi (x)$ а также по типам.

• Бесконечность . Существует непустое бинарное отношение $R$ над индивидами низшего типа, то есть иррефлексивными , транзитивными и сильно связными: $\forall x,y[x\neq y\rightarrow [xRy\vee yRx]]$ и с кодоменом, содержащимся в домене.

Замечание . Бесконечность — единственная истинная аксиома ST , имеющая полностью математическую природу. Он утверждает, что $R$ является строгим полным порядком , кодомен содержится в котором . Если 0 присвоен самому низкому типу, тип $R$ равно 3. Бесконечность может быть удовлетворена только в том случае, если (ко) область $R$ бесконечно , что приводит к существованию бесконечного множества. Если отношения определяются в терминах упорядоченных пар , эта аксиома требует предварительного определения упорядоченной пары; определение Куратовского, адаптированное к ST подойдет . В литературе не объясняется, почему обычная аксиома бесконечности (существует индуктивное множество ) ZFC других теорий множеств не может сочетаться с ST .

ST показывает, как можно сделать теорию типов очень похожей на аксиоматическую теорию множеств . Более того, более сложная онтология ST ZFC , основанная на том, что сейчас называется «итеративной концепцией множества», обеспечивает аксиомы (схемы), которые намного проще, чем аксиомы традиционных теорий множеств, таких как , с более простыми онтологиями. Теории множеств, отправной точкой которых является теория типов, но чьи аксиомы, онтология и терминология отличаются от приведенных выше, включают «Новые основы» и теорию множеств Скотта-Поттера .

основанные на

Теория типов Чёрча тщательно изучалась двумя учениками Чёрча, Леоном Хенкиным и Питером Б. Эндрюсом . Поскольку ST является логикой более высокого порядка , а в логиках высшего порядка можно определять пропозициональные связки в терминах логической эквивалентности и кванторов, в 1963 году Хенкин разработал формулировку ST , основанную на равенстве, но в которой он ограничил внимание пропозициональными типами. Позже в том же году это было упрощено Эндрюсом в его теория Q ₀ . В этом отношении ST можно рассматривать как особый вид логики высшего порядка, классифицированный П.Т. Джонстоном в «Очерках слона» как имеющий лямбда-сигнатуру высшего порядка, , то есть сигнатуру которая не содержит никаких отношений и использует только продукты и стрелки (типы функций) в качестве конструкторов типов . Более того, как выразился Джонстон, ST «безлогичен» в том смысле, что в его формулах нет логических связок или кванторов.

См. также

• Теория типов

Ссылки

• Мендельсон, Эллиот, 1997. Введение в математическую логику , 4-е изд. Чепмен и Холл.
• У. Фармер, Семь достоинств простой теории типов , Journal of Applied Logic, Vol. 6, № 3. (сентябрь 2008 г.), стр. 267–286.