Intuitionistic choice and classical logic (Q1976877)

Many mathematical results are proven by using non-constructive methods. Sometimes, however, it is possible to re-prove the same result in a more constructive manner. This re-proof is often more complex than the original proof, but it has its advantages: first, if the result stated the existence of an object, the more constructive the proof, the closer we are to actually constructing this object; second, in general, the more constructive the proof, the more reliable the statement. The authors show that a large part of analysis can be formulated and proven within a theory which combines the classical logic's law of excluded middle for ``arithmetic'' statements \(\forall n An\) with decidable \(A\) (\(\forall n(An\vee\neg An)\) implies \(\forall n An\vee \exists n \neg An\)) with an appropriate axiom of choice for sequences (e.g., \(\forall m\exists n A(m,n)\to \exists f\forall m A(m,f(m))\)). The authors provide a constructive model for this theory -- sheaves over (appropriately constructive) Boolean algebras.