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 implies LEM, then one can be sure that is also not provable in constructive mathematics; this is known as a Brouwerian counterexample.
These taboos are unprovable in neutral constructive mathematics.
These taboos are unprovable in (constructive) weakly predicative mathematics.
These taboos are unprovable in strongly predicative mathematics.
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):
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.
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, 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.