The synthetic method constructs a mathematical structure from more primitive ingredients, then derives its properties as theorems rather than postulating them as axioms. Where the axiomatic method says “assume H is a Heyting algebra,” the synthetic method says “here is a topos; Sub(Y) in any topos is a Heyting algebra; therefore H = Sub(Y) is a Heyting algebra.”
The term “synthetic” comes from synthetic geometry, which reasons about geometric objects directly (points, lines, circles) rather than encoding them as coordinate tuples. Lawvere and others extended this idea to algebra and topology: synthetic differential geometry reasons about smooth spaces without coordinates, synthetic homotopy theory (as in HoTT) reasons about paths without point-set topology. In each case, the structure is built rather than assumed.
In formalization, the synthetic method means defining the primitive constructions (categories, subobject classifiers, closure operators on Ω) and proving that they assemble into the desired algebraic structure. The Agda formalization of the semiotic universe takes this approach: it constructs the elementary topos, builds Sub(Y), and derives the Heyting algebra structure — so properties like meet-preservation of the modal closure operator j are theorems, not axioms.
The strength of the synthetic method is that it leaves no foundational gap: every property is justified by the construction, and the construction itself makes visible why the properties hold. The limitation is that it requires more infrastructure — you must build before you can prove.
Both methods are constructive in the logical sense (neither assumes excluded middle). The distinction is methodological: axiomatic = postulate properties, prove consequences; synthetic = build structure, derive properties.
Historical context
The axiomatic-synthetic distinction has a long history. Hilbert’s axiomatization of geometry (1899) was explicitly axiomatic — geometry as the study of things satisfying certain axioms, independent of construction. Lawvere’s categorical foundations (1960s onward) revived the synthetic tradition, treating mathematical structures as things you build from categorical primitives rather than things you axiomatize in first-order logic. The HoTT/Univalent Foundations program (Voevodsky et al., 2013) extends this to homotopy theory.
Related concepts
- Axiomatic method — the complementary approach that postulates rather than constructs
- Proof — what both methods produce
- Grothendieck universe — the ambient universe within which synthetic constructions take place
- Curry-Howard correspondence — the bridge that makes synthetic proofs computational