ru %D0%98%D0%BD%D1%82%D1%83%D0%B8%D1%86%D0%B8%D0%BE%D0%BD%D0%B8%D1%81%D1%82%D1%81%D0%BA%D0%B0%D1%8F %D1%82%D0%B5%D0%BE%D1%80%D0%B8%D1%8F %D1%82%D0%B8%D0%BF%D0%BE%D0%B2

Интуиционистская теория типов (теория типов Мартин-Лёфа, конструктивная теория типов) — теория типов, созданная Пером Мартин-Лёфом в 1972 году с целью формализации конструктивной математики, объекты которой, согласно Маркову-младшему, являются «некоторыми фигурами, составленными из элементарных конструктивных объектов»^[1]. В данном направлении логика математики может рассматриваться как часть философии математики, в составе которой и используется^[2].

Имеются несколько вариантов теории: Мартин-Лёфом предложены как интенсиональный^[англ.], так и экстенсиональный^[англ.] варианты, также были разработаны непредикативные версии, несовместимые с парадоксом Жирара. Тем не менее, все варианты сохраняют базовый стиль конструктивной логики с использованием зависимых типов.

Примечания

↑ Марков А. А. О конструктивной математике. Проблемы конструктивного направления в математике. 2.Конструктивный математический анализ, Сборник работ. Тр. МИАН СССР, 67, Изд-во АН СССР
↑ Д. Д. Рогозин; А. В. Родин. Теория типов в логике и основаниях математике. Москва, Институт философии РАН. 2016

[1] Марков А. А. О конструктивной математике. Проблемы конструктивного направления в математике. 2.Конструктивный математический анализ, Сборник работ. Тр. МИАН СССР, 67, Изд-во АН СССР

[2] Д. Д. Рогозин; А. В. Родин. Теория типов в логике и основаниях математике. Москва, Институт философии РАН. 2016

[1]

[2]