5
$\begingroup$

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. [...]

$\endgroup$
  • 4
    $\begingroup$ These are often introduced with the label "Theorem-Definition" or "Lemma-Definition". $\endgroup$ – S. Carnahan Oct 17 '18 at 9:08
  • 1
    $\begingroup$ Although the rational-number example is clearly not the heart of your question, I'd like to agitate against $\mathbb Z^*$ for $\mathbb Z \setminus \{0\}$. In this context, it is clearly meant to be (identical to, or at least) reminiscent of the symbol $\times$, as in $\mathbb R^\times = \mathbb R \setminus \{0\}$; but $\times$ in this context should refer to the unit group, according to which $\mathbb Z^\times = \{\pm1\}$. The notation $\mathbb Z_{\ne0}$ is one, albeit ugly, alternative. $\endgroup$ – LSpice Oct 17 '18 at 15:54
  • 2
    $\begingroup$ A Google Books search mostly turns up the word "theorem" incidentally followed by the word "definition" (like "we'll prove the theorem. Definition 10.2 says …"), but here's an example from another source: (16.38) of Souriau - Structure of dynamical systems: A symplectic view of physics. $\endgroup$ – LSpice Oct 18 '18 at 16:17
  • 2
    $\begingroup$ @LSpice And yet the notation $(-)^*$ to exclude zero is widely understood. The IOS didn't invent a standard out of thin air... $\endgroup$ – Najib Idrissi Oct 19 '18 at 7:53
  • 3
    $\begingroup$ My impression is that the notation $(-)^\times$ was invented by purpose to differentiate from $(-)^*$. This makes sense because $*$ has nothing to do with multiplication (outside programming languages). $\endgroup$ – Emanuele Paolini Oct 19 '18 at 9:10
4
$\begingroup$

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)”

$\endgroup$
  • $\begingroup$ on a slight tangent, I always found Dixmier's vn alg book much more readable than the Cstar alg book (both in the French original and in the English translations). I don't think there was any difference between the two books in how he introduced definitions, though $\endgroup$ – Yemon Choi Nov 11 '18 at 21:36
3
$\begingroup$

$\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$


$\endgroup$
  • $\begingroup$ Yes, this is what I'm also currently doing. However I think that in cases like this the statement is more a definition than a proposition. If the reader wants to know how rational numbers are defined he will look for a definition. The fact that a proof is contextually required is incidental, in my opinion. $\endgroup$ – Emanuele Paolini Oct 18 '18 at 10:48
  • $\begingroup$ @EmanuelePaolini : I think what we are discussing here is a matter of values and, to an extent, taste. To me, clarity at every step is of high value. If you want to make sure your readers know that rational numbers (say) are being introduced here, you can alert them by a sentence or two introducing the statement and/or maybe give such a piece a subsection or subsubsection title, which is what I have now done. It is also possible to use labels such as "Theorem-Definition", as suggested by S. Carnahan, but I have never seen that in publications. $\endgroup$ – Iosif Pinelis Oct 18 '18 at 14:32
2
$\begingroup$

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 _____.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.