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.
New to topics? Read the docs here!