 where, for reasons that we divulge shortly, \(x \ne 0\) means that we can find a rational number \(r\) with \(0 \lt r \lt \abs{x}\). A natural computational interpretation of (*) is that we have a procedure which, applied to any real number \(x\), either tells us that \(x = 0\) or else tells us that \(x \ne 0\). (For example, such a procedure might output 0 if \(x = 0\), and 1 if \(x \ne 0\).) However, because the computer can handle real numbers only by means of finite rational approximations, we have the problem of underflow, in which a sufficiently small positive number can be misread as 0 by the computer; so there cannot be a decision procedure that justifies the statement (*). In other words, we cannot expect (*) to hold under our natural computational interpretation of the quantifier \(\forall\) and the connective \(\vee\).