Статья: ТЕОРИЯ ТИПОВ МАРТИН-ЛЁФА: МЕЖДУ ФЕНОМЕНОЛОГИЕЙИ АНАЛИТИЧЕСКОЙ ФИЛОСОФИЕЙ

Теория типов Мартин-Лёфа опирается одновременно на логико-онтологические идеи Фреге и Рассела и на феноменологию Гуссерля. В статье исследуется этот промежуточный характер теории типов на примере синтактико-семантического метода Мартин-Лёфа и роли очевидности и канонических объектов в его теории. Синтактико-семантический метод заимствуется Мартин-Лёфом у Фреге и расширяется с опорой на теорию значения Гуссерля. Этот метод приводит в теории типов к совпадению (изоморфизму) синтаксиса и семантики (формальной логики и формальной онтологии). В отличие от традиционной формальной логики, теория типов является изначально интерпретированной системой. Будучи интуиционистской, теория Мартин-Лёфа построена на понятии доказательства, а не истинности. С точки зрения теории значения, она представляет собой вариант теоретико-доказательной семантики (Генцен, Правиц, Даммит), в которой смысл понимается как объект, построенный по определённым правилам. Так понятое доказательство опирается на очевидность, что позволяет связать его с теорией интенциональности Гуссерля. В статье проводится сопоставление теории типов и теории интенциональности Гуссерля, особенно её ноэматической стороны. Правила конструирования объектов и оперирования с ними в теории типов можно рассматривать как конкретизацию и формализацию феноменологического понятия ноэмы. То и другое является экспликацией более общего понятия смысла или значения. В статье рассмотрено соотношение понятий смысла и значения (Sinn, Bedeutung) у Фреге, Гуссерля и Мартин-Лёфа. Показана неопределённость позиции Мартин-Лёфа по отношению к теориям значения Фреге и Гуссерля.