Synthetic mathematics
Synthetic mathematics is an approach to mathematics in which a mathematical theory is built around a set of postulates specific to the theory. This contrasts with the traditional analytic approach, in which the objects studied by the theory are first constructed and their basic properties are deduced.[1]
An early historical example of synthetic mathematics is Euclidean geometry as developed in Euclid's Elements, which starts from basic postulates on points, lines, circles and angles. This form of synthetic geometry is in contrast to analytic geometry, in which points are defined by their coordinates.
In modern terminology of mathematical logic, a synthetic approach consists in reasoning about a mathematical structure using an appropriate internal language. In other words, synthetic mathematics is developed in a given logical system, of which the structure is a model. Theorems proved inside the internal language can then be translated to external theorems about the model. This model is frequently an elementary topos or an ∞-topos, and hence the synthetic approach requires not only restricting to a set of postulates but also weakening the ambient logic to be intuitionistic. This makes constructive mathematics the common basis of much of synthetic mathematics.
An advantage of synthetic mathematics is that once proved synthetically, theorems can become applicable to multiple different models. For example, reasoning in univalent foundations yields theorems about arbitrary (∞, 1)-toposes.[2] Furthermore, synthetic approaches have been employed to ease the formalization of mathematics.[3][4][5]
Examples
[edit]- Homotopy type theory is a synthetic approach to homotopy theory using the language of univalent foundations to reason about simplicial sets and cubical sets.
- Synthetic computability theory[6][7][8] develops computability theory in constructive mathematics by postulating, among other principles, that there are countably many countable subsets of the natural numbers. The main model of the theory is the effective topos, where this axiom corresponds to the basic fact from classical computability theory that there exists an admissible numbering of partial computable functions.
- Synthetic algebraic geometry has been developed in the internal language of Zariski toposes.[9][10]
- Synthetic differential geometry
References
[edit]- ↑ Synthetic mathematics at the nLab
- ↑ Shulman, Mike (2019). "All (∞, 1)-toposes have strict univalent universes". arXiv:1904.07004 [math.AT].
- ↑ Ljungström, Axel; Mörtberg, Anders (2023). "Formalising and computing the fourth homotopy group of the 3-sphere in cubical Agda". arXiv:2302.00151 [math.AT].
- ↑ Barton, Reid; Ljungström, Axel; Milner, Owen; Mörtberg, Anders; Pujet, Loïc (23 October 2025). "A formalisation of the Serre finiteness theorem" (video). Homotopy type theory electronic seminar talks.
- ↑ Forster, Yannick; Kirst, Dominik; Kunze, Fabian; Lauermann, Nils; Mück, Niklas; Zeng, Haoyi. "Synthetic computability theory in Coq". GitHub.
- ↑ Richman, Fred (1983). "Church's thesis without tears". The Journal of Symbolic Logic. 48 (3): 797–803. doi:10.2307/2273473. JSTOR 2273473.
- ↑ Bauer, Andrej (2006). "First steps in synthetic computability theory" (PDF). Electronic Notes in Theoretical Computer Science. 155: 5–31. doi:10.1016/j.entcs.2005.11.049.
- ↑ Forster, Yannick; Kirst, Dominik; Mück, Niklas (2023). Oracle computability and Turing reducibility in the calculus of inductive constructions. Programming languages and systems.
- ↑ Blechschmidt, Ingo (2021). "Using the internal language of toposes in algebraic geometry". arXiv:2111.03685 [math.AG].
- ↑ Cherubini, Felix; Coquand, Thierry; Hutzler, Matthias (2024). "A foundation for synthetic algebraic geometry". Mathematical Structures in Computer Science. 34 (9). Cambridge University Press: 1008–1053. arXiv:2307.00073. doi:10.1017/S0960129524000239. ISSN 1469-8072.
