mixing theorem with definition (definition with proof)

Question

I often find myself writing a definition which requires a proof. You are defining a term and, contextually, need to prove that the definition makes sense.

How can you express that? What about a definition with a proof?

Sometime one can write the definition and then the theorem. But often happens that many definition which should stay together need to be split because a theorem is required in between.

A tentative example:

Definition (rational numbers) Let $\sim$ be the equivalence relation on $\mathbb Z^*\times \mathbb Z$ given by $$ (q,p) \sim (q',p') \iff pq' = p'q. $$ We define $\mathbb Q= (\mathbb Z^*\times \mathbb Z)/\sim$. On $\mathbb Q$ we define addition and multiplication as follows $$ [(q,p)] + [(q',p')] = [(qq',pq'+p'q)] \\ [(q,p)] \cdot[(q',p')] = [(qq',pp')] $$ With these operations and choosing $0_\mathbb Q=[(1,0)]$, and $1_\mathbb Q=[(1,1)]$ turns out that $\mathbb Q$ is a field.

Proof. We are going to prove that $\sim$ is indeed an equivalence relation, that addition and multiplication are well defined and that the resulting set is a field. [...]

Answer 1

Dixmier always solves this as follows, e.g. in C*-algebras — surely one possible example of good exposition (E. C. Lance’s translator‘s preface: “With is clear and straightforward style, this remains the best book from which to learn about C*-algebras”):

16.1. The compact group associated with a topological group

16.1.1. Theorem. Let $G$ be a topological group. There exists a compact group $\Sigma$ and a continuous morphism $\alpha:G\to\Sigma$ possessing the following property: (...). Furthermore, the pair $(\Sigma,\alpha)$ is determined up to isomorphism by this property.

(... Long proof goes here ...)

16.1.2. Definition. The group $\Sigma$ is called the compact group associated with $G$, and $\alpha$ is called the canonical morphism of $G$ into $\Sigma$.

The book has about two dozen “X.Y.2” definitions like this — e.g. no less than six over pp. 116–123 (disjoint representations, factor representation, quasi-equivalent representations, type I, multiplicity-free, multiplicity), and the almost last statement in the book is a definition (Plancherel measure).

---

Added: I took the above example as perhaps the closest to yours (constructed object). In fact Dixmier’s relative Bourbaki does yours exactly, just the same down to the use of a subtitle (Algebra I.2.4 “Monoid of fractions”, I.8.12 “Rings of fractions”, I.9.4 “The field of rational numbers”):

12. Rings of fractions

Theorem 4. (...)

Definition 8. The ring defined in Theorem 4 is called the ring of fractions (...)

Of course, this “classic” way is not the only one: I also agree with Nik Weaver’s answer, and with this contrasting epigraph in Reed & Simon, Functional Analysis (my emphasis): “A good definition should be the hypothesis of a theorem. (J. Glimm)”

Answer 2

$\newcommand{\Z}{\mathbb{Z}} \newcommand{\Q}{\mathbb{Q}}$ I think the notion of "well-defined" may not always be well defined and should perhaps be avoided. In your example, it may be unclear what exactly is being proved.

I also think it is all right to introduce notions within a statement; this can be done without ambiguity by using terms such as "define" and "introduce" and/or the symbol "$:=$" meaning "[is] defined as". I have done it many times in my papers and never had a reviewer complain about that. In particular, your example could be rewritten as follows.

---

\subsection{Rational numbers}

The following proposition introduces, in a justified manner, the field of rational numbers.

Proposition

(I) The binary relation $\sim$ on $P:=\Z\times\Z^*$ defined by the condition \begin{equation} (p_1,q_1)\sim(p_2,q_2)\iff p_1q_2=p_2q_1 \end{equation} for $(p_1,q_1)$ and $(p_2,q_2)$ in $P$ is an equivalence. Let then \begin{equation} \Q:=P/\sim. \end{equation}

(II) Consider the binary operations $\oplus$ and $\odot$ on $P$ defined by the formulas \begin{align} (p_1,q_1)\oplus(p_2,q_2)&:=(p_1q_2+p_2q_1,q_1q_2), \\ (p_1,q_1)\odot(p_2,q_2)&:=(p_1p_2,q_1q_2) \end{align} for $(p_1,q_1)$ and $(p_2,q_2)$ in $P$. Then for any $r_1,\tilde r_1,r_2,\tilde r_2$ in $P$ such that $r_1\sim\tilde r_1$ and $r_2\sim\tilde r_2$ we have \begin{equation} r_1\oplus r_2\sim\tilde r_1\oplus\tilde r_2\quad\text{and}\quad r_1\odot r_2\sim\tilde r_1\odot\tilde r_2. \end{equation}

(III) Define now the binary operations $+$ and $\cdot$ on $\Q$ by the formulas
\begin{equation} [r_1]+[r_2]:=[r_1\oplus r_2]\quad\text{and}\quad [r_1]\cdot[r_2]:=[r_1\odot r_2] \end{equation} for all $r_1,r_2$ in $P$. Let also $0_\Q:=[(0,1)]$ and $1_\Q:=[(1,1)]$. Then $(\Q,+,\cdot,0_\Q,1_\Q)$ is a field.

Proof. $\ldots$

---

Answer 3

One approach always available is to decompose your problem into a series of definitions and theorems each of which is formally correct and relies only on the previous ones. It may require defining and naming sub-objects. For example: (1) Definition of ~. (2) Theorem: ~ is an equivalence relation. Proof. (3) Definition of the set Q. (4) Definition of the + operation. (5) Definition of the x operation. (6) Theorem: (Q,+,x) is a field. Proof.[0]

This decomposition must be possible, otherwise what you are trying to do is not formally correct. But I admit, it feels inelegant. We are taking up more space and time than we "need". We are introducing apparently "global" definitions ~,+,x but we know these are really "local" to the definition of the field Q.

So I think one just has to decide stylistically whether it sacrifices clarity to compress this into a single more concise definition. This is harder if you are introducing a new definition nobody has seen before. In this case you can consider wrapping the whole construction into a subsection of the paper with a summary/overview. ("The goal of this part is to define Q, but to do so we need some intermediate objects...").

---

[0] A similar common example is to define a function $f: A \to B$ in some way and prove it is well-defined. Formally this can be broken into two steps, e.g. (1) define the relation $f$, (2) Theorem: $f$ is a function. In both cases you want to define a _____, but really you are first defining an object then proving it is a _____.

Answer 4

I disagree with the implication that it's always necessary, when trying to write something to be understood, that every sentence has to be a logical consequence of previous sentences or assumed background knowledge.

If you're careful about it, and you say this is what you're doing, I think it can be pedagogical to state a definition first and then show that it makes sense. Especially if the verification is routine and you don't want the definition to be buried among a mass of trivialities. I can give examples of this from my own writing.