Recursive language

A formal language is decidable if a Turing machine halts on every input and correctly determines membership. Equivalently its encoded words form a recursive set. A computably enumerable language requires only a machine that eventually accepts every member; it may run forever on nonmembers.

For a fixed natural number $a$ and a standard encoding of natural numbers, validate the input and compare its encoded value with $a$. This decides $L_a$. A well-ordering argument can prove that an upward-closed set of natural numbers has this form without calculating its least element. A decider may contain that fixed least element in its finite description; its existence does not give a uniform method to discover the least element from another program.