Доклад Арнольда Григоряна «Justifying Homotopical Logic Two Ways» на Международной конференции «Logic, Algebra and Truth Degrees» в Сиене (Италия)
Стажер-исследователь МЛ ЛогЛинФФ Арнольд Григорян выступил с докладом «Justifying Homotopical Logic Two Ways» на Международной конференции «Logic, Algebra and Truth Degrees» (LATD 2025), которая прошла с 21 по 25 июля 2025 года в Сиене (Италия), объединив исследователей в области математической логики, алгебры и их приложений.
Аннотация
The talk will be divided into three parts. The first one will be dedicated to the notion of internal language in category theory and its foundational significance. The second part will use the model-theoretic viewpoint to justify the logical status of the Univalence Axiom. Finally, the rest of the talk will be dedicated to connecting both of the approaches together in order to justify the idea behind homotopical logic. Certain categories with rich enough structure (like various kinds of topoi) can be used as a model of a “mathematical universe”. One can differentiate the use of the internal language of the category in question, i.e. 'reasoning within the universe’, with ’meta-theoretical’ or external reasoning (which is more similar to the ordinary style of mathematical reasoning), that is,’reasoning about the universe.’ This opens a possibility for various conceptually interesting interactions. Proving state- ments internally allows for the generalization of obtained results to a certain extent. However, I will give a few examples where external and internal presentations of the same concept do not coincide and why this distinction is important for modern practice regarding foundations of mathematics, such as univalent foundations.
As one can use set-theoretic constructions to encode all mathematics inside the hierarchy of sets, the same can supposedly be done with certain categories (e.g., (inf,1)- topoi). More importantly, if one uses intuitionistic principles internally, but the meta-theoretical is classical, the proof as a whole can’t be considered constructive. As noted by T. Coquand [7], initial work on the simplicial model of univalent foundations used classical meta- theory, which resulted in non-constructive proofs. Thus, internal reasoning can prevent making unwarranted statements. Furthermore, it allows us to use an appropriately defined internal language as a tool to internalize principles of meta-theoretical nature, such as homotopy-invariance, shaping the idea behind homotopical logic (borrowing the name from A. Joyal’s talk [2]). The Univalence Axiom states that =U (A, B) ∼= (A ∼= B). The axiom was first introduced by Voevodsky and was motivated by the idea of homotopy theory, i.e., everything is considered under "homotopy equivalence". Another way to read the axiom is captured in S. Awodey’s slogan for mathematical structuralism that "isomorphic structures can be identified". In the homotopical interpretation of Martin-Löf’s type theory, types are interpreted as spaces, i.e., they are essentially homotopy types of spaces. The introduction of the Axiom of Univalence into type theory allows to give a formal status to the intuition that any object is invariant under the homotopy equivalence, i.e. it internalizes the aforementioned external meta-theoretical principle.
The general idea goes as follows. Given a first-order language, one can formulate a list of axioms in a given fragment of logic T. T, then, is modeled by some mathematical objects. For example, having ZFC as a theory, it is modeled by the von Neumann universe V, which is constructed using the meta-theory. In particular, V is constructed using set theory as a semi-informal meta-language and, consequently, ZFC will be the object language. From the foundational point of view, models (or in this case, V) live in some set-theoretic universe, which is the case in the set-theoretical model theory.
From the perspective of category-theoretic semantics, this just means that "traditional" set-theoretical models "live" in the category Sets, i.e., semantics is a functor from some category that represents syntax of a given theory to the universe Sets. Instead of Sets, we can consider something with more structure, obtaining other kinds of models.
The addition of homotopical interpretation to type theory is essentially about interpreting identity as a homotopy equivalence. If two types are homotopy equivalent, they are identical, i.e., there exists an identity type between them. Homotopy theory is a study of objects invariant under continuous deformation, which presupposes a weaker notion of identity.
Finally, one can see that it makes perfect sense that the universe corresponding to the ho- motopical meta-theory above is not Sets and set-theory. In particular, for the intensional dependent type theory with the Univalence Axiom, correct models can be categorically described as infinity topoi. HoTT, as a theory, is the presupposed internal language of these categories. The fact that the Univalence Axiom holds only in "homotopical" mod- els, makes the shift from set-theoretical foundations to category theory foundationally justified. On the one hand, the example above gives a definitive positive answer to the question why one needs internal language in order to distinguish between different meta-theoretical principles since the presupposed internal language of the univalent universes is not set- theoretic. On the other hand, the categories for which HoTT are supposed to be the internal language are characterized by weaker invariance criteria. This poses an interesting question about the logical status of the Univalence Axiom and the justification for homotopical logic.
References
[1] Kapulkin, K., Lumsdaine, P. L. (2021). The simplicial model of Univalent Foundations (after Voevodsky). Journal of the European Mathematical Society, 23(6), 2071–2126.
[2] André Joyal. "Remarks on homotopical logic" In Awodey, S., Garner, R., Martin- Löf, P., Voevodsky, V. (2011). Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory. Oberwolfach Reports, 8(1), 609–638.
[3] Blechschmidt, I. (2021). Using the internal language of toposes in algebraic geome- try. arXiv (Cornell University). https://doi.org/10.48550/
[4] Awodey, S. (1996). Structure in Mathematics and Logic: A Categorical perspective.
Philosophia Mathematica, 4(3), 209–237. https://doi.org/10.1093/
[5] Rodin, A. Axiomatic Method and Category Theory. en. Vol. 364. Synthese Library. Cham: Springer International Publishing, 2014. ISBN: 978-3-319-00403-7 978-3-
319-00404-4.
[6] Osius, G. “The internal and external aspect of logic and set theory in elementary topoi”. In: Cahiers de topologie et geometrie differentielle 15.2 (1974), pp. 157–180
[7] Thierry Coquand, Fabian Ruch, and Christian Sattler. Constructive sheaf models of type theory. arXiv:1912.10407 [math]. July 2021
Страница конференции.