[FOM] A New Ordinal Notation

[Dmytro Taranovsky]

Lew Gordeew wrote:
> Would you please explicitly expose primitive recursive definitions of your
> basic relations < and = in the system of notations built up from 0 and
> C(-,-,-) ?

The description under the heading "Comparison Relation" in my paper

http://web.mit.edu/dmytro/www/other/OrdinalNotation.htm

leads naturally to a recursive algorithm that checks whether the
ordinals are given in the standard form, and if so, compares them.


To compare d and e check whether d<e and whether e<d.
To check whether d<e, verify that 'd' is in the standard form and then
use (1) (see the paper).

Let d be given as C(a, b, c).  To verify that d is in the standard form,
verify that b and c are in the standard form, and then verify that b is
maximal and c is minimal. To verify that c is minimal, apply (3).  To
verify that b is maximal,  apply (4) and (5).  

Note that being in  the standard form guarantees the maximality and the
minimality in (1), (3), and (5).  To avoid infinite regress, when asked
to check for a strict inequality, check only for the strict inequality
as opposed to doing the full comparison.


The algorithm terminates since the expressions will simplify at each
stage of the recursion.

I should note that the self-referential definition of the notation  is
easier to understand than the comparison algorithm.

Dmytro Taranovsky