Classical mathematics for a constructive world

DOI10.1017/S0960129511000132MaRDI QIDQ3094179zbMATH OpenOpenAlexFDO

Authors Russell O'Connor

Publication date 21 October 2011

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1008.1213

zbMATH Keywords

classical function spacesclassical reasoningconstructive logic as an extension of classical logicconstructive reasoningdependent type theoryinteractive theorem provingweak value monad

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Other constructive mathematics (03F65)

Abstract: Interactive theorem provers based on dependent type theory have the flexibility to support both constructive and classical reasoning. Constructive reasoning is supported natively by dependent type theory and classical reasoning is typically supported by adding additional non-constructive axioms. However, there is another perspective that views constructive logic as an extension of classical logic. This paper will illustrate how classical reasoning can be supported in a practical manner inside dependent type theory without additional axioms. We will see several examples of how classical results can be applied to constructive mathematics. Finally, we will see how to extend this perspective from logic to mathematics by representing classical function spaces using a weak value monad.

Recommendations

• A Constructive Proof of Dependent Choice, Compatible with Classical Logic
• Intuitionistic choice and classical logic
• Proof-theoretic semantics for classical mathematics
• On the constructive and computational content of abstract mathematics
• Automated constructivization of proofs

Cites work

• A course in constructive algebra
• A Modular Formalisation of Finite Group Theory
• Automated Machine-Checked Hybrid System Safety Proofs
• Certified Exact Transcendental Real Number Computation in Coq
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 1226875 (Why is no real title available?)
• scientific article; zbMATH DE number 949290 (Why is no real title available?)
• Strong functors and monoidal monads
• The Dedekind reals in abstract Stone duality

Cited in

(2)

• Starting the Dismantling of Classical Mathematics
• Dynamic separation logic

This page was built for publication: Classical mathematics for a constructive world

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3094179)