|
ИСТИНА |
Войти в систему Регистрация |
ИПМех РАН |
||
Univalent Foundations of Mathematics and Paraconsistencyстатья
Информация о цитировании статьи получена из
Web of Science,
Scopus
Дата последнего поиска статьи во внешних источниках: 30 августа 2016 г.
- Автор: Васюков В.Л.
- Сборник: New Directions in Paraconsistent Logic
- Серия: Springer Proceedings in Mathematics & Statistics
- Том: 152
- Год издания: 2016
- Издательство: Springer (India)
- Местоположение издательства: New Delhi, India
- Первая страница: 285
- Последняя страница: 294
- DOI: 10.1007/978-81-322-2719-9_13
- Аннотация: Vladimir Voevodsky in his Univalent Foundations Project writes that univalent foundations can be used both for constructive and for non-constructive mathematics. The last is of extreme interest since this project would be understood in a sense that this means an opportunity to extend univalent approach on non-classical mathematics. In general, Univalent Foundations Project allows the exploitation of the structures on homotopy types instead of structures on sets or structures on categories as in case of set-level mathematics or category-level mathematics. Non-classical mathematics should be respectively considered either as non-classical set-level mathematics or as non-classical category-level (toposes-level) mathematics. Since it is possible to directly formalize the world of homotopy types using in particular Martin-Lof type systems then the task is to pass to non-classical type systems e.g. da Costa paraconsistent type systems in order to formalize the world of non-classical homotopy types. Taking into account that the univalent model takes values in the homotopy category associated with a given set theory and to construct this model one usually first chooses a locally cartesian closed model category (in the sense of homotopy theory) then trying to extend this scheme for a case of non-classical set theories (e.g. paraconsistent ones) we need to evaluate respective non-classical homotopy types not in cartesian closed categories but in more suitable ones. In any case it seems that such Non-Classical Univalent Foundations Project should be directly developed according to Logical Pluralism paradigma and and it seems that it is difficult to find counter-argument of logical or mathematical character against such an opportunity except the globality and complexity of a such enterprise.
- Добавил в систему: Маркин Владимир Ильич