Lets take (classical) first-order logic for granted, including an equality symbol and its associated axioms.
Given all this, a rigorous work of mathematics will typically begin with a signature - that is, a collection of symbols. For example, the symbols $\in$ for set theory, or the symbols $0,1,+,\times,<$ for arithmetic.
Lets just stick with set theory as our motivating example, so our starting symbol is $\in$.
The next thing is to list axioms which will be assumed true for the remainder of the work. For example, in set theory a common axiom is:
Axiom of Extensionality. For all $X$ and all $Y$, it holds that
- (if) for all $o$ it holds that $o \in X$ precisely when $o \in Y,$
- (then) $X=Y.$
The writer then proceeds from these axioms to prove theorems.
For instance, using the axioms of ZFC we can prove the existence of a unique empty set. This might be Theorem 1.
Theorem 1. There exists unique $X$ such that for all $o$ it holds that not $o \in X$.
What I'm looking for is a slightly different approach to rigor. Rather than asserting some axioms at the get-go, I'd like a work that merely defines axioms.
Definition 1. Extensionality means that for all $X$ and $Y$, it holds that
- (if) for all $o$ it holds that $o \in X$ precisely when $o \in Y,$
- (then) $X=Y.$
Where we would normally state a theorem, we instead define another axiom, and then write the theorem after.
Definition 5. Unique empty set means there exists unique $X$ such that for all $o$ it holds that not $o \in X$.
Theorem 1. If Extensionality and Empty set, then Unique empty set.
Is there a work of mathematics structured in this fashion?