# 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

• In general, for any statement $P$ which is true in classical mathematics, the statement that “the law of excluded middle implies $P$” is true in neutral constructive mathematics.

• Furthermore, for any statement $P$ which is true in classical mathematics with the axiom of choice, the statement that “the axiom of choice implies $P$” is true in neutral constructive mathematics.

### 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.