**constructive mathematics**, **realizability**, **computability**

propositions as types, proofs as programs, computational trinitarianism

A **taboo**, for a particular flavor of mathematics or formal system, is a simple statement that is known to be not provable therein, and that can therefore be used to establish the unprovability of other statements without the need to descend into metamathematical considerations (such as syntactic analysis or construction of countermodels) or, in some cases, even to decide on a particular formal system to be working in.

For example, the law of excluded middle (LEM) is a taboo for constructive mathematics. Therefore, if some statement $P$ implies LEM, then one can be sure that $P$ is also not provable in constructive mathematics; this is known as a **Brouwerian counterexample**.

These taboos are unprovable in constructive mathematics.

- law of excluded middle
- principle of omniscience
- axiom of choice
- supports split
- fan theorem
- choice operator
- presentation axiom
- dependent choice

These taboos are unprovable in (constructive) weakly predicative mathematics.

These taboos are unprovable in strongly predicative mathematics.

- subset collection
- function sets
- axiom of replacement
- axiom of collection
- function types
- dependent function types

These taboos are unprovable in homotopy type theory, even if we assume constructive taboos such as LEM and AC.

A taboo found in cubical type theory:

These taboos are unprovable in constructive homotopy type theory, but they may be provable if we assume a constructive taboo *or* a homotopical taboo.

These taboos are unprovable in discrete cohesive homotopy type theory (i.e. the setting for plain homotopy type theory):

- Peter Aczel, slide 8 of:
*Constructive Set Theory*, 2008 (pdf)

A mathematical taboo is a statement that we may not want to assume false, but we definitely do not want to be able to prove.

- Peter Aczel, Michael Rathjen, Section 2.3 of:
*Notes on Constructive Set theory*, 2001 (pdf, pdf)

Certain basic principles of classical mathematics are taboo for the constructive mathematician. Bishop called them

principles of omniscience.

- Mark Mandelkern?,
*Brouwerian Counterexamples*, Mathematics Magazine, vol. 62 no. 1, 1989 (doi:10.2307/2689939)

See also:

- Michael J. Beeson, Footnote 3, p. 6 (27 of 484) in:
*Foundations of Constructive Mathematics*, Ergebnisse der Mathematik und ihrer Grenzgebiete**3**6, Springer 1985 (doi:10.1007/978-3-642-68952-9, pdf)

Peter Aczel has introduced the word

tabooin this context. The decidability of equality on the reals is taboo in the sense that any proposition which has been shown to imply it will be regarded as essentially non-constructive. When we refute a proposition, we show that it implies a contradiction, an absurdity. If instead we show that it implies the decidability of equality on the reals, we have shown its essential non-constructivity, but in a weaker way than by actually refuting it. In other words, $0 = 1$ is the most taboo of all taboos. There are several other common taboos besides the decidability of equality, which we shall soon encounter.

- Hannes Diener, Section 0.3 and 0.4 of:
*Constructive Reverse Mathematics*, 2018 (arXiv:1804.05495, dspace:ubsi/1306)

the full axiom of choice is a definite constructive taboo

Last revised on November 27, 2022 at 23:35:50. See the history of this page for a list of all contributions to it.