In classical mathematics, the distinction between linear orders and total orders is merely a terminological technicality, which is not always observed; more precisely, there is a natural bijection between the set of total orders on a given set and the set of linear orders on , and one distinguishes them by the notation (for the linear order) and (for the total order). In constructive mathematics, however, they are irreducibly different.
A linear order on a set is a (binary) relation with the following properties:
In classical mathematics, one may see these versions of asymmetry and connectedness:
Using excluded middle, these are equivalent to asymmetry and connectedness as given above, but they need not hold for all linear orders in constructive mathematics.
Actually, these axioms are overkill; to begin with, irreflexivity is simply a special case of asymmetry and so can be dropped. Additionally, one can either drop transitivity or drop asymmetry (which then requires keeping irreflexivity); they will still follow from the other axioms. Dropping transitivity shows manifestly the duality (see below) between linear orders and total orders (even in constructive mathematics), while keeping transitivity and dropping asymmetry shows manifestly that a linear order is a special kind of quasiorder.
In classical mathematics, there are even more options. Now comparison can be dropped, as it follows from transitivity and connectedness. Also, one often combines irreflexivity, asymmetry, and connectedness into a single axiom using exclusive disjunction:
Thus the most common definition uses only trichotomy and transitivity.
One can also interpret connectedness not as an axiom but as a definition of equality, getting a linear order on a quotient set of . In other words, if is an asymmetric comparison relation on , and we define to mean that neither nor , then is an equivalence relation and induces a linear order on .
Classically, any total order defines an example of a linear order (as explained below), and this also holds constructively in discrete mathematics. Since most linear orders in these cases are usually described in terms of their total orders, the focus here is on constructive analysis. (The first item, however, is an exception.)
Using excluded middle, one can move between linear orders and total orders using negation; that is, the negation of a linear order is a total order and vice versa. Actually one usually swaps the order too, as follows:
To prove this, it's enough to see that the properties of a linear order are dual to the properties of a total order, as follows:
|linear order||total order|
Constructively, these are still the default definitions to use; that is, if one is given a linear order or a total order and wants to interpret the other symbol, then one does so using these definitions. However, the result will not necessarily be a total order or a linear order. To be specific, if one starts with a linear order and defines as above, then totality does not follow; and if one starts with a total order and defines as above, then comparison does not follow. Nevertheless, at least will be a partial order, and least will be a quasiorder. Furthermore, the duality between the axioms is still there, even though negation no longer mediates between them; although comparison need not hold for a total order constructively, the duality is preserved if one defines linear orders without using transitivity.
One often sees defined as but ; this is equivalent, but doesn't show the de Morgan duality explicitly. Similarly, one often sees defined as or ; this is not even equivalent constructively, although it is classically.
Keep in mind, however, that the only use of excluded middle in the classical theory is the assumption that , , and are always either true or false. There is therefore a perfect correspondence between decidable linear orders and decidable total orders on sets with decidable equality.