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.


Constructive taboos

These taboos are unprovable in constructive mathematics.

Homotopical taboos

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

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.

Created on November 28, 2015 17:23:58 by Mike Shulman (