Less-Than Predicate (Primitive Recursion)

Definition

Less-Than Predicate ( Primitive Recursion)

The less-than predicate on natural numbers has the primitive-recursive indicator function

The result is when and otherwise. Truncated subtraction computes the non-negative difference ; signum tests whether it is positive. Thus

The projections swap the inputs so that the difference is , not . In particular, the less-than predicate is decidable.

Construction

The truncated difference is positive exactly when the second input exceeds the first:

If or , truncated subtraction returns , so the strict comparison is false.

Example

Less than, equal to, or greater than