Intuitionistic choice and classical logic
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.
- Wellfounded trees in categories
- Arithmetical conservation results
- To be or not to be constructive, that is not the question
- Statistics of intuitionistic versus classical logics
- Determinate logic and the axiom of choice
- Heyting-valued interpretations for constructive set theory
- 2000 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium 2000. La Sorbonne, Paris, France, July 23-31, 2000
- A Constructive Proof of Dependent Choice, Compatible with Classical Logic
- Classical mathematics for a constructive world
- Intuitionistic Decision Procedures Since Gentzen
- scientific article; zbMATH DE number 2051381 (Why is no real title available?)
- Choice Principles and Constructive Logics†
- Does choice really imply excluded middle? II: Historical, philosophical, and foundational reflections on the Goodman-Myhill result
- Does choice really imply excluded middle? I: Regimentation of the Goodman-Myhill result, and its immediate reception
- scientific article; zbMATH DE number 6607423 (Why is no real title available?)
- Type theories, toposes and constructive set theory: Predicative aspects of AST
- The iteration of the mathematical process
This page was built for publication: Intuitionistic choice and classical logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1976877)
