 We turn now to intuitionistic logic in practice. What sort of things are we looking for if we are serious about developing mathematics in such a way that when a theorem asserts the existence of an object \(x\) with a property \(P(x)\), then the proof of the theorem embodies algorithms for constructing \(x\) and for demonstrating, by whatever calculations are necessary, that \(x\) has the property \(P(x)\). Here are some examples of theorems, each followed by an informal description of the requirements for its constructive proof.