Кросс-мировая предикация: теоретико-типовая и теоретико-множественная формализация

Oleg Domanov

Аннотация


В статье описываются некоторые потенциальные проблемы теории кросс-мировой предикации Е. Борисова и предлагаются альтернативные формализации в терминах теории типов с зависимыми типами и теории множеств. Преимущество теоретико-типовой формализации состоит в её простоте, связанной с наличием в теории типов функций в зависимые типы. Преимущество предлагаемой теоретико-множественной формализации состоит в большей близости к традиционным подходам и отсутствии некоторых неинтуитивных следствий, таких как предикация по несуществующим объектам.

Полный текст:

PDF

Литература


Hofmann 1997 — Hofmann M. Syntax and semantics of dependent types // Extensional Constructs in Intensional Type Theory. London: Springer London, 1997. P. 13–54.

Kocurek 2016 — Kocurek A. W. The Problem of Cross-world Predication // Journal of Philosophical Logic. 2016. Vol. 45, no. 6. P. 697–742.

Martin-Löf 1984 — 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 p. (Studies in Proof Theory).




DOI: https://doi.org/10.52119/LPHS.2021.13.88.006

Ссылки

  • На текущий момент ссылки отсутствуют.


Bookmark and Share


(c) 2021 Oleg Domanov

Лицензия Creative Commons
Это произведение доступно по лицензии Creative Commons «Attribution-NonCommercial» («Атрибуция — Некоммерческое использование») 4.0 Всемирная.