 Roughly speaking, there are two main motivations for these restrictions. The traditional intuitionists L. E. J. Brouwer (e.g., [1964a], [1964b]) and Arend Heyting (e.g. [1956]) held that the essence of mathematics is idealized mental construction. Consider, for example, the proposition that for every natural number \(n\), there is a prime number \(m \gt n\) such that \(m \lt n!+2\). For Brouwer, this proposition invokes a procedure that, given any natural number \(n\), produces a prime number \(m\) that is greater than \(n\) but less than \(n!+2\). The proposition expresses the existence of such a procedure. Given this orientation, we have no reason to hold that for any mathematical proposition \(\Phi\), we can establish either the procedure associated with \(\Phi\) or the procedure associated with \(\neg \Phi\).