Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

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

Он был привязан к формальной математике со времен Principia Mathematica до сегодняшних помощников по доказательству .

1900–1927 [ править ]

Происхождение теории типов Рассела [ править ]

В письме к Готтлобу Фреге (1902 г.) Бертран Рассел объявил о своем открытии парадокса в « Begriffsschrift» Фреге . [1] Фреге незамедлительно ответил, признав проблему и предложив решение в техническом обсуждении «уровней». Цитируя Фреге:

Между прочим, мне кажется, что выражение « предикат предикатирован сам по себе» неточно. Предикат, как правило, является функцией первого уровня, и эта функция требует объект в качестве аргумента и не может иметь себя в качестве аргумента (субъекта). Поэтому я бы предпочел сказать «понятие основывается на собственном расширении». [2]

Он пытается показать, как это может работать, но, кажется, отказывается от этого. В результате того, что стало известно как парадокс Рассела, и Фреге, и Рассел были вынуждены быстро вносить поправки в работы, которые у них были в типографии. В приложении B, которое Рассел привязал к своим «Основам математики» (1903), можно найти его «предварительную» теорию типов. Этот вопрос мучил Рассела около пяти лет. [3]

Уиллард Куайн [4] представляет исторический синопсис происхождения теории типов и «разветвленной» теории типов: рассмотрев отказ от теории типов (1905), Рассел, в свою очередь, предложил три теории:

  1. теория зигзага
  2. теория ограничения размера,
  3. теория бесклассов (1905–1906), а затем,
  4. повторное принятие теории типов (1908ff)

Куайн отмечает, что введение Расселом понятия «кажущаяся переменная» привело к следующему результату:

различие между 'all' и 'any': 'all' выражается связанной ('кажущейся') переменной универсальной квантификации, которая колеблется в зависимости от типа, а 'any' выражается свободной ('реальной') переменной что схематично относится к любой неопределенной вещи независимо от типа.

Куайн отвергает это понятие «связанной переменной» как « бессмысленное вне определенного аспекта теории типов ». [5]

«Разветвленная» теория типов 1908 года [ править ]

Куайн объясняет разветвленную теорию следующим образом: «Она была названа так потому, что тип функции зависит как от типов ее аргументов, так и от типов кажущихся переменных, содержащихся в ней (или в ее выражении), если они превышают типы аргументов ". [5] Стивен Клини в своем « Введении в метаматематику» 1952 года описывает разветвленную теорию типов следующим образом:

Первичные объекты или индивиды (т. Е. Данные вещи, не подлежащие логическому анализу) назначаются одному типу (скажем, типу 0 ), свойства индивидов - типу 1 , свойства свойств индивидов - типу 2 и т. Д .; и не допускаются никакие свойства, которые не попадают ни в один из этих логических типов (например, это выводит свойства «предсказуемость» и «непредсказуемость» ... за пределы логики). Более подробный отчет описал бы допустимые типы для других объектов как отношения и классы. Затем, чтобы исключить непредикативные определения внутри типа, типы выше типа 0 далее разделяются на порядки. Таким образом, для типа 1 свойства, определенные без упоминания какой-либо совокупности, принадлежат к порядку 0., а свойства, определенные с использованием совокупности свойств данного порядка, относятся к следующему более высокому порядку. ... Но такое разделение на порядки делает невозможным построение привычного анализа, который, как мы видели выше, содержит непредикативные определения. Чтобы избежать этого исхода, Рассел постулировал свою аксиому сводимости , которая утверждает, что для любого свойства, принадлежащего к порядку выше низшего, существует коэкстенсивное свойство (то есть свойство, которым обладают точно такие же объекты) порядка 0. Если бы только определяемые свойства были считается существующим, тогда аксиома означает, что каждому импредикативному определению в пределах данного типа существует эквивалентное предикативное определение (Kleene 1952: 44–45).

Аксиома сводимости и понятие «матрица» [ править ]

Но поскольку положения разветвленной теории оказались бы (цитируя Куайна) «обременительными», Рассел в своей « Математической логике 1908 года», основанной на теории типов [6], также предложил свою аксиому сводимости . К 1910 году Уайтхед и Рассел в своих Principia Mathematica дополнили эту аксиому понятием матрицы.- полностью расширенная спецификация функции. Из его матрицы функция может быть получена процессом «обобщения» и наоборот, то есть два процесса обратимы - (i) обобщение от матрицы к функции (с использованием кажущихся переменных) и (ii) обратный процесс сокращение типа путем подстановки значений аргументов для кажущейся переменной. С помощью этого метода можно было избежать непредсказуемости. [7]

Таблицы истинности [ править ]

В 1921 году Эмиль Пост разработал теорию «функций истинности» и их таблиц истинности, которые заменяют понятие очевидных и реальных переменных. Из его «Введения» (1921 г.): «Поскольку полная теория [Уайтхеда и Рассела (1910, 1912, 1913)] требует для формулировки своих предложений реальных и кажущихся переменных, которые представляют как индивидов, так и пропозициональные функции различных видов, и, как результат, требует громоздкой теории типов, эта подтеория использует только действительные переменные, и эти реальные переменные представляют собой лишь один вид сущностей, которые авторы решили назвать элементарными предложениями ». [8]

Примерно в то же время Людвиг Витгенштейн развил аналогичные идеи в своей работе 1922 года Tractatus Logico-Philosophicus :

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

3.332. Никакое предложение не может ничего сказать о себе, потому что пропозициональный знак не может содержаться в себе (это вся «теория типов»).

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

Витгенштейн также предложил метод таблицы истинности. В своих статьях с 4.3 по 5.101 Витгенштейн принимает неограниченный штрих Шеффера в качестве своей фундаментальной логической сущности, а затем перечисляет все 16 функций двух переменных (5.101).

Понятие «матрица как таблица истинности» появляется еще в 1940–1950-х годах в работах Тарского, например, в его указателях 1946 года «Матрица, см .: Таблица истинности» [9].

Сомнения Рассела [ править ]

Рассел в своем « Введении в математическую философию» 1920 года посвящает целую главу «Аксиоме бесконечности и логических типов», в которой он выражает свои опасения: «Теория типов категорически не принадлежит законченной и определенной части нашего предмета: большая часть из эта теория все еще находится в зачаточном состоянии, запутана и неясна. Но необходимость в некоторой доктрине типов менее сомнительна, чем точная форма, которую эта доктрина должна принять; и в связи с аксиомой бесконечности особенно легко увидеть необходимость некоторых таких доктрина ". [10]

Рассел отказывается от аксиомы сводимости : во втором издании Principia Mathematica (1927) он признает аргумент Витгенштейна. [11] В начале своего введения он заявляет, что «не может быть никаких сомнений ... что нет необходимости проводить различие между действительными и кажущимися переменными ...». [12] Теперь он полностью принимает понятие матрицы и заявляет, что « функция может появляться в матрице только через ее значения » (но возражает в сноске: «Она занимает место (не совсем адекватно) аксиомы сводимости» [13] ] ). Кроме того, он вводит новое (сокращенное, обобщенное) понятие «матрицы», то есть «логической матрицы ... такой, которая не содержит констант.Таким образом, p |q является логической матрицей ». [14] Таким образом, Рассел фактически отказался от аксиомы сводимости, [15] но в своих последних абзацах он заявляет, что из« наших нынешних примитивных суждений »он не может вывести« дедекиндовы отношения и хорошо упорядоченные отношения ». и отмечает, что если есть новая аксиома, которая заменяет аксиому сводимости, «ее еще предстоит открыть» [16].

Теория простых типов [ править ]

В 1920-х годах Леон Чвистек [17] и Франк П. Рэмси [18] заметили, что, если кто-то готов отказаться от принципа порочного круга , иерархия уровней типов в «разветвленной теории типов» может рухнуть.

Результирующая ограниченная логика называется теорией простых типов [19] или, возможно, более широко, теорией простых типов. [20] Подробные формулировки теории простых типов были опубликованы в конце 1920-х - начале 1930-х годов Р. Карнапом, Ф. Рэмси, В. В. О. Куайном и А. Тарски. В 1940 году Алонсо Чёрч (заново) сформулировал его как просто типизированное лямбда-исчисление . [21] и исследован Геделем в 1944 году. Обзор этих достижений можно найти в Collins (2012). [22]

1940-е годы по настоящее время [ править ]

Гёдель 1944 [ править ]

Курт Гёдель в своей математической логике Рассела 1944 года дал следующее определение «теории простых типов» в сноске:

Под теорией простых типов я подразумеваю доктрину, которая гласит, что объекты мысли (или, в другой интерпретации, символические выражения) делятся на типы, а именно: индивиды, свойства индивидов, отношения между индивидами, свойства таких отношений, и т. д. (с аналогичной иерархией для расширений), и что предложения формы: « a имеет свойство φ », « b имеет отношение R к c » и т. д. бессмысленны, если a, b, c, R, φне подходят друг к другу. Смешанные типы (например, классы, содержащие индивидов и классы в качестве элементов) и, следовательно, также трансфинитные типы (например, класс всех классов конечных типов) исключаются. То, что теории простых типов достаточно, чтобы избежать эпистемологических парадоксов, показывает их более тщательный анализ. (См. Ramsey 1926 и Tarski 1935 , стр. 399) ". [23]

Он пришел к выводу, что (1) теория простых типов и (2) аксиоматическая теория множеств «допускают вывод современной математики и в то же время избегают всех известных парадоксов» (Gödel 1944: 126); более того, теория простых типов «является системой первых начал [ Principia Mathematica ] в соответствующей интерпретации ... [M] любые симптомы, однако, слишком ясно показывают, что примитивные концепции нуждаются в дальнейшем разъяснении» (Gödel 1944). : 126).

Переписка Карри – Ховарда, 1934–1969 [ править ]

Соответствие Карри – Ховарда - это интерпретация доказательств как программ и формул как типов. Идея началась в 1934 году с Хаскелла Карри и завершилась в 1969 году с Уильямом Элвином Ховардом . Он соединил «вычислительную составляющую» многих теорий типов с выводами в логике.

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

АВТОМАТ де Брейна, 1967–2003 [ править ]

Николаас Говерт де Брюйн создал теорию типов Automath как математическую основу для системы Automath, которая могла проверять правильность доказательств. Система развивалась и добавляла функции с течением времени по мере развития теории типов.

Интуиционистская теория типов Мартина-Лёфа, 1971–1984 [ править ]

Пер Мартин-Лёф открыл теорию типов, соответствующую логике предикатов , введя зависимые типы , которая стала известна как интуиционистская теория типов или теория типов Мартина-Лёфа.

Теория Мартина-Лёфа использует индуктивные типы для представления неограниченных структур данных, таких как натуральные числа.

Лямбда-куб Барендрегта, 1991 [ править ]

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

Ссылки [ править ]

  1. ↑ Письмо Рассела (1902) к Фреге появляется с комментариями в van Heijenoort 1967: 124–125.
  2. ^ Frege (1902) Письмо к Расселу появляется с комментариями в van Heijenoort 1967: 126–128.
  3. ^ ср. Комментарий Куайна перед Расселом (1908) Математическая логика, основанная на теории типов у ван Хейенурта 1967: 150
  4. ^ ср. комментарий В.В.О. Куайна до работы Рассела (1908). Математическая логика, основанная на теории типов у ван Хейенурта 1967: 150–153
  5. ^ a b Комментарий Куайна до Рассела (1908) Математическая логика, основанная на теории типов у ван Хейенурта 1967: 151
  6. ^ Рассел (1908) Математическая логика, основанная на теории типов в van Heijenoort 1967: 153–182
  7. ^ ср. в частности п. 51 в главе II Теория логических типов и * 12 Иерархия типов и аксиома сводимости стр. 162–167. Уайтхед и Рассел (1910–1913, 2-е издание 1927 г.) Principia Mathematica
  8. ↑ Post (1921) Введение в общую теорию элементарных предложений в van Heijenoort 1967: 264–283
  9. ^ Тарский 1946, Введение в логику и методологию дедуктивных наук , Дуврское переиздание, 1995
  10. ^ Рассел 1920: 135
  11. ^ ср. «Введение» ко 2-му изданию, Russell 1927: xiv и Приложение C
  12. ^ ср. «Введение» ко 2-му изданию, Russell 1927: i
  13. ^ ср. «Введение» ко 2-му изданию, Russell 1927: xxix
  14. ^ Вертикальная черта «|» - штрих Шеффера; ср. «Введение» ко 2-му изданию, Russell 1927: xxxi
  15. ^ «Теория классов одновременно упрощается в одном направлении и усложняется в другом из-за предположения, что функции возникают только через свои значения, и из-за отказа от аксиомы сводимости»; ср. «Введение» ко 2-му изданию, Russell 1927: xxxix
  16. ^ Эти цитаты из «Введения» ко 2-му изданию, Russell 1927: xliv – xlv.
  17. ^ L. Chwistek, Antynomje logikiformalnej, Przeglad Filozoficzny 24 (1921) 164–171
  18. ↑ FP Ramsey, Основы математики, Труды Лондонского математического общества , серия 2 25 (1926) 338–384.
  19. ↑ Gödel 1944, страницы 126 и 136–138, сноска 17: «Математическая логика Рассела», появляющаяся в Kurt Gödel: Collected Works: Volume II Publications 1938–1974 , Oxford University Press, New York NY, ISBN  978-0-19-514721 -6 (v.2.pbk).
  20. ^ Это не означает, что теория «проста», это означает, что теория ограничена : типы разных порядков не должны смешиваться: «Смешанные типы (например, классы, содержащие индивидов и классы в качестве элементов) и, следовательно, также трансфинитные типы ( такие как класс всех классов конечных типов) исключены ". Gödel 1944, страницы 127, сноска 17: «Математическая логика Рассела», появляющаяся в Kurt Gödel: Collected Works: Volume II Publications 1938–1974 , Oxford University Press, New York NY, ISBN 978-0-19-514721-6 (v. 2.pbk). 
  21. ^ А. Чёрч, Формулировка простой теории типов, Журнал символической логики 5 (1940) 56–68.
  22. ^ Дж. Коллинз, История теории типов: развитие после второго издания «Principia Mathematica». LAP Lambert Academic Publishing (2012). ISBN 978-3-8473-2963-3 , особенно. гл. 4–6. 
  23. ↑ Gödel 1944: 126 сноска 17: «Математическая логика Рассела», появляющаяся в Kurt Gödel: Collected Works: Volume II Publications 1938–1974 , Oxford University Press, New York NY, ISBN 978-0-19-514721-6 (v.2 .pbk). 

Источники [ править ]

  • Бертран Рассел (1903), Принципы математики: Vol. 1 , Cambridge at the University Press, Кембридж, Великобритания.
  • Бертран Рассел (1920), Введение в математическую философию (второе издание), Dover Publishing Inc., Нью-Йорк, штат Нью-Йорк, ISBN 0-486-27724-0 (в частности, главы XIII и XVII). 
  • Альфред Тарский (1946), Введение в логику и методологию дедуктивных наук , переизданный в 1995 году Dover Publications, Inc., Нью-Йорк, NY ISBN 0-486-28462-X 
  • Жан ван Хейенорт (1967, 3-е издание 1976 г.), От Фреге до Гёделя: Справочник по математической логике, 1879–1931 , Издательство Гарвардского университета, Кембридж, Массачусетс, ISBN 0-674-32449-8 (pbk) 
    • Бертран Рассел (1902), Письмо Фреге с комментарием ван Хейеноорта, страницы 124–125. При этом Рассел объявляет о своем открытии «парадокса» в творчестве Фреге.
    • Готтлоб Фреге (1902), Письмо Расселу с комментарием ван Хейеноорта, страницы 126–128.
    • Бертран Рассел (1908), Математическая логика, основанная на теории типов , с комментарием Уилларда Куайна , страницы 150–182.
    • Эмиль Пост (1921), Введение в общую теорию элементарных предложений , с комментарием ван Хейеноорта, страницы 264–283.
  • Альфред Норт Уайтхед и Бертран Рассел (1910–1913, 1927, 2-е издание, переиздано в 1962 году), Principia Mathematica до * 56 , Cambridge at the University Press, Лондон, Великобритания, без ISBN или номера в каталоге США.
  • Людвиг Витгенштейн (переиздано в 2009 г.), Основные работы: Избранные философские сочинения , HarperCollins, Нью-Йорк. ISBN 978-0-06-155024-9 . Витгенштейна (1921 на английском языке), Tractatus Logico-Philosophicus , страницы 1–82. 

Дальнейшее чтение [ править ]

  • W. Farmer, "Семь достоинств теории простых типов", Journal of Applied Logic , Vol. 6, № 3. (сентябрь 2008 г.), стр. 267–286.