Changes

In this setting the <math>^{\backprime\backprime}\!\!<\!^{\prime\prime}</math> on the left is a logical ordering on syntactic terms while the <math>^{\backprime\backprime}\!\!<\!^{\prime\prime}</math> on the right is an arithmetic ordering on real numbers.

In this setting the <math>^{\backprime\backprime}\!\!<\!^{\prime\prime}</math> on the left is a logical ordering on syntactic terms while the <math>^{\backprime\backprime}\!\!<\!^{\prime\prime}</math> on the right is an arithmetic ordering on real numbers.

The type of principle that comes up here is usually discussed under the question of whether a map between two ordered sets is ''order-preserving'' or not.  The general type of question may be formalized in the following way.

The question that arises in this case is whether a map between two ordered sets is ''order-preserving''.  In order to formulate the question in more general terms, we may begin with the following set-up:

: Let ''X''₁ be a set with an ordering denoted by "&lt;₁".

| Let <math>X_1\!</math> be a set with the ordering <math><_1\!.</math>

| Let <math>X_2\!</math> be a set with the ordering <math><_2\!.</math>

: Let ''X''₂ be a set with an ordering denoted by "&lt;₂".

An order relation is typically defined by a set of axioms that determines its properties.  Since we have frequent occasion to view the same set in the light of several different order relations, we often resort to explicit specifications like <math>(X, <_1),\!</math> <math>(X, <_2),\!</math> and so on, to indicate a set with a given ordering.

 

What makes an ordering what it is will commonly be a set of axioms that defines the properties of the order relation in question.  Since one frequently has occasion to view the same set in the light of several different order relations, one will often resort to explicit forms like (''X'',&nbsp;&lt;₁), (''X'',&nbsp;&lt;₂), and so on, to invoke a set with a given ordering.

A map ''F'' : (''X''₁,&nbsp;&lt;₁) &rarr; (''X''₂,&nbsp;&lt;₂) is ''order-preserving'' if and only if a statement of a particular form holds for all ''x'' and ''y'' in (''X''₁,&nbsp;&lt;₁), specifically, this:

A map ''F'' : (''X''₁,&nbsp;&lt;₁) &rarr; (''X''₂,&nbsp;&lt;₂) is ''order-preserving'' if and only if a statement of a particular form holds for all ''x'' and ''y'' in (''X''₁,&nbsp;&lt;₁), specifically, this: