🐱: Существуют чистые системы типов (pure type systems, PTS), которые

Question

🐱: Существуют чистые системы типов (pure type systems, PTS), которые

можно увидеть, в частности, в так называемом лямбда-кубе (lambda cube). От обычных теорий типов отличаются особыми ограничениями: запрещены индуктивные типы (в том числе типы натуральных чисел, например) и запрещены же вселенные типов. Это неудобно, но больше похоже на математическую логику, чем обычные теории типов. По этой причине неудобности, можно ввести всё это хитрыми способами через Church encodings. Так, интерактивный доказыватель теорем / пруф-ассистент Cedille делает всё это (но пишут, что он отходит от PTS в контексте identity types). В контексте схожести с математической логикой такой вопрос: можно ли при помощи чистых систем типов (PTS) — и только них — возродить логицизм [условно] в стиле Рассела?

🕸: Чистые системы типов (PTS) действительно представляют собой мощный инструмент для формализации различных аспектов логики и математики. В лямбда-кубе, предложенном Хенком Барендрегтом, PTS классифицируются по различным зависимостям между типами и термами¹. Эти системы позволяют выразить многие логические конструкции, но имеют ограничения, такие как отсутствие индуктивных типов и вселенных типов.

Возрождение логицизма в стиле Рассела с использованием только PTS представляет собой интересную задачу. Логицизм, как направление в философии математики, стремится свести все математические понятия к логическим. Основная проблема, с которой столкнулись Рассел и Уайтхед, заключалась в парадоксах, таких как парадокс Рассела, и в необходимости введения аксиом, которые не являются чисто логическими⁵.

Использование PTS для возрождения логицизма потребует обхода этих ограничений. Одним из возможных подходов является использование кодировок Чёрча для представления индуктивных типов и других конструкций, которые отсутствуют в PTS. Это позволяет выразить многие математические структуры в рамках PTS, но не решает всех проблем, связанных с логицизмом. Например, аксиома бесконечности и другие экзистенциальные аксиомы остаются вызовом⁴.

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

Если у вас есть конкретные аспекты или примеры, которые вы хотели бы обсудить подробнее, дайте знать!

0

11.07.2024

1 ответов

44 просмотра

Brenoritvrezorkre · Answer 1

Brenoritvrezorkre Автор вопроса

Стикер

0

3 месяца назад

Похожие чаты

🐱: Существуют чистые системы типов (pure type systems, PTS), которые

1 ответов

Похожие вопросы