Login
You're viewing the discuss.systems public feed.
  • Nov 13, 2023, 8:29 PM

    There are a variety of models validating one taboo but not others.

    For example, the toposes that validate EM are precisely those which are boolean. And given any topos, we can construct (constructively!) a derived topos which is boolean and satisfies a certain universal property with respect to the original topos. This is similar, and explains mathematically, rather than logically, the so-called double-negation translation.

    All the above "taboos" hold in boolean toposes. But some of them hold in non-boolean toposes. One example is Johnstone's Topological Topos, which makes all the above taboos, except LLPO and WSAC, to fail. All of the above "taboos", except LLPO and WSAC, allow one to define non-continuous functions, which don't exist in the topological topos.

    Why are they called taboos? Perhaps for philosophical reasons.

    But they are rather useful in mathematical practice when one is "agnostic" regarding the constructive/non-constructive dichotomy.

    E.g. Trying to prove a mathematical statement A without classical assumptions? Failed for a long time? Perhaps it is time to find a counter-model. Or, instead, and more easily, and more mathematically, show that A implies a "taboo". Even more ambitiously, try to prove that it is equivalent to some "taboo". Sometimes people call this "reverse constructive mathematics": which non-constructive assumptions are needed to prove a given mathematical statement A?

    2/

    💬 3🔄 0⭐ 0

Replies