nLab neutral constructive mathematics

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Mathematics

Constructivism, Realizability, Computability

Contents

Idea

Neutral constructive mathematics is a branch of constructive mathematics which simply removes the axiom of choice and excluded middle from the axioms of the foundations, and does not replace it either with weaker versions of the axiom of choice or with axioms which contradict the axiom of choice. Thus, neutral constructive mathematics is agnostic about the status of the axiom of choice and excluded middle.

As a result, impredicative neutral constructive mathematics is the internal logic of an elementary topos with natural numbers object.

 Examples

Examples of mathematical foundations which one could do impredicative neutral constructive mathematics include:

Examples of mathematical foundations which one could do predicative neutral constructive mathematics include:

 Consequences

Set theory

Real analysis

Algebra

  • Not every subset has an injection into the superset. Thus, subsets with an injection are usually better behaved than general subsets.

  • Not every vector space has a basis. Thus, free vector spaces are usually better behaved than vector spaces in general.

 See also

  • Jason Rute?, What is neutral constructive mathematics, (MathOverflow)

  • Fred Richman, Constructive Mathematics without Choice,

    in: Reuniting the Antipodes – Constructive and Nonstandard Views of the Continuum, Synthese Library 306, Springer (2001) 199-206 [doi:10.1007/978-94-015-9757-9_17]

There was a seminar on neutral constructive mathematics:

  • Mathematical Logic and Constructivity: The Scope and Limits of Neutral Constructivism, Stockholm, Sweden, August 20-23, 2019 (website)

Last revised on August 20, 2024 at 19:24:17. See the history of this page for a list of all contributions to it.