ТЕОРИЯ ТИПОВ В СЕМАНТИКЕ ПРОПОЗИЦИОНАЛЬНЫХ УСТАНОВОК
Аннотация
В статье описывается подход к анализу пропозициональных установок, опирающийся на теоретико-типовую семантику, предложенную А. Ранта и основанную на теории типов П. Мартин-Лёфа. Теоретико-типовая семантика в явном виде содержит контексты и способы извлечения информации из них. Это позволяет корректно формализовать зависимость от контекста, характерную для пропозициональных установок. В статье контекст представляется в виде типа зависимой суммы (тип Record в системе работы с доказательствами Coq), при этом подход А. Ранта уточняется и применяется к анализу фразы Куайна «Ральф верит, что кто-то шпион». Описано три варианта формализации этой фразы, которые различаются содержанием контекстуального знания и способом вывода из него истинностных значений фразы. Связь между контекстами устанавливается функцией преобразования, позволяющей соотносить значения истинности. В результате, средства для работы с контекстами, предоставляемые теоретико-типовой семантикой, позволяют избежать проблем непрозрачности, описанных Куайном. Формализация вместе с доказательствами кодирована в Coq и свободно доступна.
Скачивания
Литература
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.
