basic constructions:
strong axioms
further
In “synthetic” approaches to the formulation of theories in mathematics the emphasis is on axioms that directly capture the core aspects of the intended structures, in contrast to more traditional “analytic” approaches where axioms are used to encode some basic substrate out of which everything else is then built analytically.
| analytic | synthetic |
|---|---|
| structures built out of “point-set”-substrate | axioms imposed on the available types |
Often the “synthetic approach” is just referred to as “axiomatic”. For instance model categories were introduced as “axiomatic homotopy theory” and indeed they may be regarded as providing a synthetic axiomatization of homotopy theory, which is not based on (but does subsume) the traditional “point-set model” provided by topological spaces.
The terminology “analytic/synthetic” has ancient roots (cf. analytic versus synthetic). Its use in modern mathematics may go back to Lie 1876, who wrote about his development of what is now called Lie theory the following (translated to English, as quoted in Kock 1981, Preface) with reference to what is now called analysis and synthetic differential geometry:
“The reason why I have postponed for so long these investigations, which are basic to my other work in this field, is essentially the following. I found these theories originally by synthetic considerations. But I soon realized that, as expedient the synthetic method is for discovery, as difficult it is to give a clear exposition on synthetic investigations, which deal with objects that till now have almost exclusively been considered analytically. After long vacillations, I have decided to use a half synthetic, half analytic form. I hope my work will serve to bring justification to the synthetic method besides the analytical one.”
synthetic geometry axiomatizes the nature of objects in a plane or hyperplane without speaking of the plane or hyperplane itself as a collection of points and without speaking of these figures as being subsets of points.
synthetic differential geometry is refinement of this to contemporary research-level mathematics.
Here instead of defining the concept of smooth manifold analytically by “point-set methodology” as is traditional (a set of points equipped with a topology and a smooth structure, etc.) one imposes one single axiom scheme in the ambient topos (the “Kock-Lawvere axiom” in this case) which essentially ensures that for all objects/types there exists also an object/type which behaves as the tangent bundle of should. These axioms then turn out to have models in smooth spaces (which include smooth manifolds) but also in other, such as algebraic geometry and supergeometry.
Alternatively one may set up synthetic differential geometry via axioms for differential cohesion.
synthetic homotopy theory – With the advent of homotopy type theory, which may be regarded to some extent as a further abstraction of axioms similar to those of model categories, it became more common to speak of this as “synthetic homotopy theory”, as, for example, in the HoTT book. For a list of work carried out in homotopy type theory, see at mathematics presented in homotopy type theory
synthetic topology – There are many different approaches for doing topology synthetically. Some of them include:
synthetic Stone duality, which sets up the topos of light condensed sets via axioms
abstract Stone duality, which sets up the category of locally compact locales via axioms
real-cohesive homotopy type theory, which sets up the (infinity,1)-topos of Euclidean topological infinity-groupoids via axioms
formal category theory, a synthetic approach to category theory
Synthetic approaches are naturally compatible with constructive mathematics/intuitionistic mathematics, but synthetic mathematics is about a different issue than constructivism. For instance even most constructive proof assistants in existence have in their libraries defined basic mathematics concepts, such as topological spaces, in the traditional analytic way.
There is at least some similarity between synthetic mathematics and domain specific embedded programming languages, see for instance (Hudak 98, section 3.2). In (Hudak 98, figure 2) this shows aspects of a real-world DSL for “geometric region analysis” embedded in Haskell which under the relation between type theory and category theory/computational trinitarianism one immediately recognizes as a fragment of synthetic geometry.
Proving an arithmetic result in Peano arithmetic, or more generally a statement in an appropriate axiomatic theory, ensures axiomatic purity (a notion of purity of methods) , cf. Lehet 2021).
Moreover, such proofs are certain to be valid because of the nature of the fundamental objects considered, as captured by the axioms of the theory, and not by accident because of their particular construction in such and such a system.
Andrej Bauer: Synthetic Mathematics with an Excursion Into Computability Theory, talk at University of Wisconsin Logic Seminar (Feb 2021) [blog, slides:pdf, pdf video:yt]
Wikipedia: Analytic-synthetic distinction
On the axiomatic method:
Discussion of synthetic homotopy theory (cf. synthetic homotopy theory, typically understood as homotopy type theory):
Ulrik Buchholtz, Sec. 3.1 of: Higher Structures in Homotopy Type Theory [arXiv:1807.02177]
Mike Shulman, slides 37 onwards in: Homotopical trinitarianism:A perspective on homotopy type theory, 2018 (pdf)
Egbert Rijke: Classifying Types [arXiv:1906.09435]
Via cubical type theory:
Last revised on June 27, 2026 at 14:23:22. See the history of this page for a list of all contributions to it.