The axiomatic method begins with a list of properties that a structure is assumed to satisfy, then deduces consequences from those properties alone. You do not build the structure — you postulate its existence and its laws, then prove theorems within that framework.
Euclid’s Elements is the classical example: five postulates about points and lines, then hundreds of propositions derived from them. Modern algebra works the same way: a group is any set with an operation satisfying three axioms (associativity, identity, inverses), and group theory is the study of what follows from those axioms, independent of any particular group.
In formalization, the axiomatic method means defining a typeclass or record with fields for the operations and properties, then proving lemmas about any instance of that typeclass. The Lean formalization of the semiotic universe takes this approach: HeytingDomain postulates that H is a Heyting algebra, ModalClosure postulates that j is extensive, monotone, idempotent, join-preserving, and meet-preserving, and theorems are proved from these axioms.
The strength of the axiomatic method is speed and generality: you can begin proving things immediately, and your results apply to every structure satisfying the axioms. The limitation is that the axioms themselves are unjustified within the formalization — they must be justified externally (by construction, by example, or by appeal to a metatheorem). An axiomatic formalization verifies that the consequences of the axioms are correct, but does not verify that the axioms are achievable.
The synthetic method addresses this limitation by constructing the structure from primitives and deriving the axiomatic properties as theorems.
Related concepts
- Synthetic method — the complementary approach that constructs rather than postulates
- Proof — what both methods produce
- Heyting algebra — an example of an axiomatically defined structure