Decidable well-order
= Decidable well-order
{title2=$\prec\ \subseteq\mathbb N^2$}
= Computable well-order
{synonym}
A <decidable well-order> on the <natural numbers> is a <well-order> whose comparison relation is computable. Comparing two codes is an effective finite task; the proof that the relation has no infinite descending chain is a separate mathematical assertion. <Computable Cantor normal form notation> gives such an order of type <epsilon zero>.