Shulman (forthcoming) agrees, describing it as a ‘synthetic theory of structures’, in the sense that nothing can be said about mathematical entities defined within it except structurally. Awodey ( 2014) claims that, through its so-called ‘Univalence Axiom’, HoTT captures what is essentially right about the structuralist position. In the second half of the paper, I shall apply this account of definite description to the phrase ‘the structure of A’, for a general type A. We will find that a reasonable way to approach this topic casts light on mathematicians’ usage of ‘the’ in a generalized sense, as when they say ‘the product of two groups’, apparently without there being a unique way to construct such a product. It seems fitting then to see what the latest ‘new logic’ can bring to this question. One of the first applications by Russell of his ‘new logic’ (Russell 1905) was the analysis of definite descriptions. Whether we take it as an extended logic, or consider it to entail that logic is to be subsumed within mathematics, an early consideration as to how to engage philosophically with HoTT will be to revisit what thinkers took to be promising applications of previous forms of logic. Were its ‘modal’ and ‘linear’ variants to become accepted too, this extended logic would also have the resources to speak about Noether’s theorem, relating symmetries to conservation laws, and also about geometric quantization (Schreiber 2014, 2016). HoTT possesses the resources to derive, as matters simply arising from its conception of identity, results about homotopy groups of spheres and about group representations, topics normally seen as pieces of advanced mathematics. Were HoTT ever to take the place of the formal languages currently employed by analytic philosophers, it would involve a significant change of outlook. Logic, in the shape of a form of propositional and predicate logic, comes built into the type theory, arising from the application of its rules to a certain class of types. Homotopy type theory (henceforth HoTT), on the other hand, is given largely by type formation rules, and rules for the introduction and elimination of terms. Set theory is standardly formulated as a first-order axiomatic theory whose domain ranges over sets and which is equipped with a binary membership relation. This system possesses many novel features compared to the traditional set theoretic foundations, not least the way it integrates logic within itself. Homotopy type theory has recently been proposed as a new foundational language for mathematics (UFP 2014).
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |