Algorithm Implementation/Sorting/Some proofs

This section rigorously and in standard mathematical language describes the logical system which rationalizes sorting in computer programs. Many of these results are obvious, and some of the notation might be found in assorted computer-science textbooks. Anyone who finds any flaw with the following is invited to improve it.

The mathematics the first author applies here is sophisticated, but hardly complicated.

NOTE: The conventional approach to these proofs rests on slightly shakier assumptions. It employs a device called a "loop invariant," which is defined in terms of underlying program structure. Proofs constructed this way can be found in most good algorithmics textbooks.

Basic notions

It is impossible to order an unordered set; but sorting usually concerns itself not with sets, but with sequences. Let us define, then, precisely what sequences we may sort, and what the results may entail. Let S be any set with a total ordering ($\mathbb {Z}$, $Q$, $\mathbb {R}$...) Let A be a finite subset of that set. Let J be a finite subset of $\mathbb {N}$, the natural numbers. Now draw up a function $\phi :J\rightarrow S$. The set J induces a so-called permutation group, Sym(J), the set of all bijections from J back onto J. Now let $\Phi \equiv \{\mu \in Sym)J):\phi \circ \mu$. A little consideration will convince the reader that the set hereupon described is exactly the set of possible arrangements of the elements of a sequence. Of course, $\phi _{\mu }=\phi _{\lambda }$ is possible if it happens that a permutation exchanges indices so that the value of the function doesn't change at the indices; but this will not be a great concern to us. As we will see, exactly one of the functions in $\Phi$ is increasing. (A function is increasing whenever x ≥ y implies f(x) ≥ f(y)).