Writing proofs that are more or less formal

[Terrell]

How do I know if a proof I am writing or reading is informal or formal enough? Of course there are obvious distinctions like a formal proofs cannot constitute a drawing (e.g. venn diagrams, triangles for the triangle inequality), but sometimes I read proofs that uses phrases like "Continue in this manner". Are there clear rules we can follow?

For instance, I am trying to prove

"Let $X$ be a totally ordered set and $\forall U\subseteq X$ s.t. $U\neq\emptyset$ has both a max. and min., then $X$ is finite."

The idea of the proof is very intuitive and recursive, but formalizing it is a bit tricky since there's multiple ways of doing it. After writing a quite complicated and incorrect proof. Then someone wrote the following proof

"Assume X is infinite and let $x_1$ be the bottom element of $X$. Let $X_1$ = $X$ - {$x_1$} and $x_2$ the bottom element of $X_1$. Continue in this manner creating the set { $x_j$ : j in N }. which has no maximum."

Which made me a bit irritated because I think using the phrase "Continue in this manner" is like "cheating". So how can I take advantage of this style of writing if I am not aware of the boundaries of what I can and cannot do when writing formal proofs in math?

 

[andrewkirk]

The proof is using the principle of recursive definition to define the set, without acknowledging it. It is poor practice to use a principle without acknowledging it, unless that principle is being used so often in the text leading up to the proof that it need not be mentioned.

In the famous Topology text by Munkres, the author makes a specific point of the defects in proofs that assume this principle without stating it. He presents an example of a proof that does this and then calls out the transgression immediately afterwards in order to introduce the principle. See section 1-7 'Countable and Uncountable Sets'.

The above proof can be written more rigorously without increasing the length, as follows:

Assume X is infinite. Then the principle of recursive definition tells us that there exists a unique function $h:\mathbb N\to X$ such that $h(1)=\min(X)$ and for $k>1,\ h(k)=\min \left (X - \bigcup_{j=1}^{k-1}\{h(j)\}\right)$. Then the image of $h$ is a subset of X that has no maximum.

The last sentence is not blindingly obvious and could do with some expansion, but that criticism applies both to this version and the one in the OP.

 

[mfb]

"Continue in this manner" means "replace 1 by 2 and 2 by 3 for the next step, then replace them by 3 and 4, and so on." There are nicer ways to write it, but there is nothing informal about it - it is a unique description of the set.

 

[Terrell]

"Continue in this manner" means "replace 1 by 2 and 2 by 3 for the next step, then replace them by 3 and 4, and so on." There are nicer ways to write it, but there is nothing informal about it - it is a unique description of the set.

So the principle of recursive definition is the way of mathematicians of "formalizing" this?

 

[andrewkirk]

So the principle of recursive definition is the way of mathematicians of "formalizing" this?

The principle of recursive definition is actually a theorem, which has to be proven rigorously. The claim of the theorem is set out in the above link. Essentially it says that there exists a unique function that has the properties given in a recursive definition. The proof of the theorem typically uses the induction axiom of Peano arithmetic.

There are two long proofs of the theorem given here, as well as a short, fallacious one. I had a quick look at the first proof and it looks sound, except that in the last line of the theorem statement $g(f(m))$ should be $g(f(n))$. But I did not check it step by step.

On reflection I realize that a more precise way of invoking the theorem in my above post is to say "the principle of recursive definition tells us that there exists a unique function" rather than "use the principle of recursive definition to define a function". I will make the change above.

 

[Terrell]

The principle of recursive definition is actually a theorem, which has to be proven rigorously.

Wow, this is cool! However, my university profs might not approve of me using this though lol.