nLab taboo

Taboos

Taboos

Idea

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 PP implies LEM, then one can be sure that PP is also not provable in constructive mathematics; this is known as a Brouwerian counterexample.

Examples

Neutral constructive taboos

These taboos are unprovable in neutral constructive mathematics.

Weakly predicative-constructive taboos

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

Strongly predicative taboos

These taboos are unprovable in strongly predicative mathematics.

Homotopical taboos

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:

Constructive-homotopical taboos

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

 Discrete cohesion taboos

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

References

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.

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:

Peter Aczel has introduced the word taboo in 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=10 = 1 is the most taboo of all taboos. There are several other common taboos besides the decidability of equality, which we shall soon encounter.

the full axiom of choice is a definite constructive taboo

Last revised on September 19, 2024 at 17:03:33. See the history of this page for a list of all contributions to it.