"The whole is greater than the sum of its parts" (Aristotle).
Semantics and syntax
A real number r1 is greater than another real number r2 (and is written r1>r2 if and only if r1−r2 belongs to R/+, the positive real ray or, in other words, if r2−r1 belongs to R/−, the negative real ray.
A real number r1 is less than another real number r2 (and is written r1<r2)if and only if r1−r2 belongs to R/−, the negative real ray or, in other words, if r2−r1 belongs to R/+. the positive real ray.
Definitions
⟨( r1>r2 =: (r1−r2 ∈ R/+) )⟩
⟨( r1<r2 =: (r2−r1 ∈ R/+) )⟩
Justification
It is the formal definition of comparison operators in terms of membership of real semiring.
Examples
(3<4)? // ev. α
(4<3)? // ev. θ
(3>4)? // ev. θ
(4>3)? // ev. α
(n = 7)
(v ← (n>5) // ev. v
(n1 = 7)
(n2 = 4)
(u ← ((n1>5) ← (n2<3)) →' v) // ev. v
Remarks
Operations can be used as conditions or as declarative expressions.
Properties
⟨( r1>r2 ↔ r2<r1 )⟩
⟨( r1=r2 ↔ (r1−r2)=0 )⟩
⟨( r1>r2 ↔ (1.÷r1 < 1.÷r2) )⟩
⟨( (r1>r2 ∧ r>0) → (r1*r> r2*r) )⟩
⟨( r1>r2 ∧ r<0 → (r1*r< r2*r) )⟩
Contrary operators
Syntax
Not greater than (or less than or equal to): >' eq. ≤
Not less than (or greater than or equal to): <' eq. ≥
