ТЕОРИЯ ТИПОВ В СЕМАНТИКЕ ПРОПОЗИЦИОНАЛЬНЫХ УСТАНОВОК

  • Олег Анатольевич Доманов Институт философии и права СО РАН
Ключевые слова: теория типов, теоретико-типовая семантика, пропозициональные установки, А.Ранта

Аннотация

В статье описывается подход к анализу пропозициональных установок, опирающийся на теоретико-типовую семантику, предложенную А. Ранта и основанную на теории типов П. Мартин-Лёфа. Теоретико-типовая семантика в явном виде содержит контексты и способы извлечения информации из них. Это позволяет корректно формализовать зависимость от контекста, характерную для пропозициональных установок. В статье контекст представляется в виде типа зависимой суммы (тип Record в системе работы с доказательствами Coq), при этом подход А. Ранта уточняется и применяется к анализу фразы Куайна «Ральф верит, что кто-то шпион». Описано три варианта формализации этой фразы, которые различаются содержанием контекстуального знания и способом вывода из него истинностных значений фразы. Связь между контекстами устанавливается функцией преобразования, позволяющей соотносить значения истинности. В результате, средства для работы с контекстами, предоставляемые теоретико-типовой семантикой, позволяют избежать проблем непрозрачности, описанных Куайном. Формализация вместе с доказательствами кодирована в Coq и свободно доступна.

Скачивания

Данные скачивания пока не доступны.

Литература

Martin-Löf, P. An intuitionistic type theory: Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980. Napoli: Bibliopolis, 1984. 91 pp.
Martin-Löf, P. "On the Meanings of the Logical Constants and the Justifications of the Logical Laws", Nordic Journal of Philosophical Logic, 1996, vol. 1, no. 1, pp. 11-60.
Martin-Löf, P. "An intuitionistic theory of types", in: Twenty-five years of constructive type theory. New York: Oxford Univ. Press, 1998, pp. 127-172.
Quine, W. "Quantifiers and propositional attitudes", Journal of Philosophy, 1956, vol. 53, iss. 5, pp. 177-187.
Ranta, A. Type-theoretical grammar. Oxford: Clarendon Press, 1994. 226 pp.
Salmon, N. U. Frege’s Puzzle. Cambridge, Mass.: Bradford Books/The MIT Press, 1986. 195 pp.
The Coq Proof Assistant. URL: https://coq.inria.fr/
Univalent Foundations Program T. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study: http://homotopytypetheory.org/book, 2013. 589 pp.
Опубликован
2019-03-21
Как цитировать
Доманов О. А. ТЕОРИЯ ТИПОВ В СЕМАНТИКЕ ПРОПОЗИЦИОНАЛЬНЫХ УСТАНОВОК // Эпистемология и философия науки. 2019. Т. 55. № 4. С. 26-37.