?
Models of HoTT and the Constructive View of Theories
Ch. 9. P. 191–219.
Rodin A.
Homotopy Type theory and its Model theory provide a novel formal
semantic framework for representing scientific theories. This framework
supports a constructive view of theories according to which a theory
is essentially characterised by its methods. The constructive view of
theories was earlier defended by Ernest Nagel and a number of other
philosophers of the past but available logical means did not allow these
people to build formal representational frameworks that implement this
view.
., 2025.
The 17th International Summer School-Conference “Problems Allied to Model Theory and Universal Algebra” was held on 19–26 of June 2025 at Sobolev Institute of Mathematics, Novosibirsk State Technical University NETI and at the Camping Center “Erlagol” in Altai mauntains. The School was organized by Algebra and Mathematical Logic Department of Novosibirsk State Technical University (NSTU ...
Added: November 24, 2025
Novosibirsk: ., 2023.
The 15th International Summer School-Conference “Problems Allied to
Model Theory and Universal Algebra” was held on 21–29 of June 2023 at
Novosibirsk State Technical University NETI and at the camping center
“Erlagol” in Altai mountains. The School was organized by Algebra and
Mathematical Logic Department of Novosibirsk State Technical University
(NSTU NETI) and Sobolev Institute of Mathematics of Siberian Branch ...
Added: November 23, 2023
Gavrilovich M., Communications in Algebra 2020 Vol. 48 No. 4 P. 1548–1566
We formulate two conjectures about étale cohomology and fundamental groups motivated by categoricity conjectures in model theory. One conjecture says that there is a unique ZZ-form of the étale cohomology of complex algebraic varieties, up to Aut(C)Aut(C)-action on the source category; put differently, each comparison isomorphism between Betti and étale cohomology comes from a choice of a ...
Added: October 29, 2020
Rodin A., , in: Одиннадцатые Смирновские чтения по логике: материалы Международной научной конференции, 19 – 21 июня 2019, г. Москва.: М.: Современные тетради, 2019. P. 42–43.
Kant famously argued that elementary geometrical statements such as
Euclid's Triangle Angle Sum theorem cannot be deduced from the rst principles
by purely logical means because their proofs require extra-logical geometrical
constructions [1, A719/B747]. The discovery of non-Euclidean geometries
in the 19-th century made Kant's analysis of geometrical reasoning untenable
in its original form, and throughout the following 20-th century ...
Added: June 30, 2019
Valery Isaev, Mathematical Structures in Computer Science 2018 Vol. 28 No. 10 P. 1695–1722
Models of dependent type theories are contextual categories with some additional structure. We prove that if a theory T has enough structure, then the category T-Mod of its models carries the structure of a model category. We also show that if T has Σ-types, then weak equivalences can be characterized in terms of homotopy categories ...
Added: November 6, 2018
Sustretov D., Zilber B., Solanki V., Annals of Pure and Applied Logic 2014 Vol. 165 No. 6 P. 1149–1168
We carry out a model-theoretic analysis of the Heisenberg algebra. To this end, a geometric structure is associated to the Heisenberg algebra and is shown to be a Zariski geometry. Furthermore, this Zariski geometry is shown to be non-classical, in the sense that it is not interpretable in an algebraically closed field. On assuming self-adjointness ...
Added: October 18, 2018
Sustretov D., Journal of Symbolic Logic 2016 Vol. 81 No. 3 P. 917–935
The objective of this article is to characterise elimination of finite generalised imaginaries (as defined by Hrushovski) in terms of group cohomology. As an application, I consider series of Zariski geometries constructed by Hrushovski and Zilber, and indicate how their non-definability in algebraically closed fields and other theories is connected to eliminability of certain generalised ...
Added: October 18, 2018
Zolin E., Logic Journal of the IGPL 2015 Vol. 23 No. 6 P. 861–880
The celebrated theorem proved by Goldblatt and Thomason in 1974 gives necessary and sufficient conditions for an elementary class of Kripke frames to be modally definable. Here we obtain a local analogue of this result, which deals with modal definability of classes of pointed frames. Furthermore, we generalize it to the case of n-frames, which ...
Added: June 14, 2018
Rodin A., , in: Philosophy, Mathematics, Linguistics: Aspects of Interaction (PhML 2012).: St. Petersburg: ВВМ, 2012. P. 170–174.
The non-standard identity concept developed in the Homotopy Type theory allows for an alternative analysis of
Frege’s famous Venus example, which explains how empirical evidences justify judgements about identities and accounts for
the constructive aspect of such judgements. ...
Added: June 6, 2018
Rodin A., , in: Frontiers of Fundamental Physics 14Vol. 224: EPISTEMOLOGY AND PHILOSOPHY.: [б.и.], 2014.
Homotopy Type theory instantiates a new form of axiomatic approach, which is more friendly to
physics than the standard axiomatic approach stemming from Hilbert. This new axiomatic approach
combines logical and geometrical methods in a new way and brings about a non-trivial
constructive concept of identity applicable in various physical contexts including Quantum Mechanics
and General Relativity. ...
Added: June 6, 2018
Springer, 2019.
Homotopy Type theory and its Model theory provide a novel formal semantic
framework for representing scienti c theories. This framework supports a constructive
view of theories according to which a theory is essentially characterised by its methods.
The constructive view of theories was earlier defended by Ernest Nagel and a number of
other philosophers of the past but available logical ...
Added: June 5, 2018
Rodin A., IfCoLoG Journal of Logics and their Applications 2017 Vol. 4 No. 4 P. 1427–1446
The identity concept developed in the Homotopy Type theory (HoTT) supports an analysis of Frege's famous Venus example, which explains how empirical evidences justify judgements about identities. In the context of this analysis we consider the traditional distinction between the extension and the intension of concepts as it appears in HoTT, discuss an ontological signi cance ...
Added: June 5, 2018
Rodin A., Logique et Analyse 2018 Vol. 242 No. 2 P. 201–231
The received notion of axiomatic method stemming from Hilbert is not fully adequate to the recent successful practice of axiomatizing mathematical theories. The axiomatic architecture of Homotopy type theory (HoTT) does not ft the pattern of formal axiomatic theory in the standard sense of the word. However this theory falls under a more general and ...
Added: May 26, 2018
Улан-Удэ: Издательство Бурятского госуниверситета, 2017.
The collection represents proceedings of the 5th school-seminar "Syntax and Semantics of Logic Systems" (Ulan-Ude, 08.08.2017 - 12.08.2017). The conference subject area includes: theory of models and universal algebra; theory of boolean and finite-valued functions; formal languages and logic calculus; mathematical logic in education. ...
Added: September 22, 2017
Fomichov V. A., Informatica. An International Journal of Computing and Informatics 2017 Vol. 41 No. 2 P. 221–232
The first starting point of this paper is the broadly accepted idea of employing, as a promising methodology, an artificial semantic language-intermediary for the realization of automatic cross-lingual intelligent information access to natural language (NL) texts on the Web. The second one is the emergence in computational semantics during 2013-2016 of great interest in the ...
Added: September 4, 2017
Gavrilovich M., Bays M., Hils M., International Mathematics Research Notices 2014 Vol. 14 P. 3927–4000
Let S be a semiabelian variety over an algebraically closed field, and let X be an irreducible subvariety not contained in a translate of a proper algebraic subgroup of S. We show that the number of irreducible components of [n]^−1 (X) is bounded uniformly in n, and moreover that the bound is uniform in families ...
Added: October 23, 2015
Gavrilovich M., Hasson A., Israel Journal of Mathematics 2015 Vol. 209
We construct a model category (in the sense of Quillen) for set
theory, starting from two arbitrary, but natural, conventions. It is the simplest
category satisfying our conventions and modelling the notions of niteness,
countability and in nite equi-cardinality. We argue that from the homotopy
theoretic point of view our construction is essentially automatic following basic
existing methods, and so is ...
Added: October 20, 2015