 Before mathematicians assert something (other than an axiom) they are supposed to have proved it true. What, then, do mathematicians mean when they assert a disjunction \(P \vee Q\), where \(P\) and \(Q\) are syntactically correct statements in some (formal or informal) mathematical language? A natural — although, as we shall see, not the unique — interpretation of this disjunction is that not only does (at least) one of the statements \(P, Q\) hold, but also we can decide which one holds. Thus just as mathematicians will assert \(P\) only when they have decided that \(P\) holds by proving it, they may assert \(P \vee Q\) only when they either can produce a proof of \(P\) or else produce one of \(Q\).