`Kronecker's density theorem and irrational numbers in constructive reverse mathematics'

To prove Kronecker’s density theorem in Bishop-style constructive analysis one needs to define an irrational number as a real number that is bounded away from each rational number. In fact, once one understands “irrational” merely as “not rational”, then the theorem becomes equivalent to Markov’s principle. To see this we undertake a systematic classification, in the vein of constructive reverse mathematics, of logical combinations of “rational” and “irrational” as predicates of real numbers.