 is provably false within recursive function theory, even with classical logic (see Bridges &amp; Richman [1987], Chapter 3); so if we want to allow a recursive interpretation of all our mathematics, then we cannot use LPO. Secondly, there is a model theory (Kripke models) in which it can be shown that LPO is not constructively derivable (Bridges &amp; Richman [1987], Chapter 7).