Classical Mathematics for a Constructive World

TL;DR

This paper demonstrates how classical reasoning can be integrated into dependent type theory without extra axioms, enabling classical mathematics within a constructive framework using a weak value monad.

Contribution

It introduces a practical approach to support classical reasoning in dependent type theory without additional axioms, bridging classical and constructive mathematics.

Findings

Classical results can be applied within constructive mathematics.

Classical reasoning is supported without non-constructive axioms.

Representation of classical function spaces using a weak value monad.

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.