теория типа ST

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

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

Все переменные, появляющиеся в определении идентичности и в аксиомах Экстенсиональности и Осмысления , ранжируются по индивидам одного из двух последовательных типов. Только нештрихованные переменные (ранжирующие по "низшему" типу) могут появляться слева от ' ', тогда как справа от него могут появляться только штрихованные переменные (ранжирующие по "высшему" типу). Формулировка ST первого порядка исключает квантификацию по типам. Следовательно, каждая пара последовательных типов требует своей собственной аксиомы Экстенсиональности и Осмысления, что возможно, если Экстенсиональность и Осмысление ниже рассматриваются как схемы аксиом "ранжирующие по" типам. ${\displaystyle \in }$

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

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

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

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

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

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

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

Формулировки, основанные на равенстве

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

Смотрите также

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

Ссылки

• Мендельсон, Эллиот, 1997. Введение в математическую логику , 4-е изд. Chapman & Hall.
• У. Фармер, Семь добродетелей теории простых типов , Журнал прикладной логики, т. 6, № 3. (сентябрь 2008 г.), стр. 267–286.

1. Стэнфордская энциклопедия философии : «Теория типов Чёрча» — Питер Эндрюс (адаптировано из его книги).
2. PT Johnstone, Эскизы слона , стр. 952