Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Inspired by a discussion with Martin Escardo, I created taboo.
Well, I suppose if you redefine “taboo” to mean “Brouwerian counter-example”, then that changes its meaning. But I would prefer to keep the two separate.
Is there anywhere in writing where Aczel said what he intended it to mean? Or anyone who’s in a position to ask him?
Under the homotopical taboos can we include Whitehead theorem?
Mike said once:
we shouldn’t expect to prove in homotopy type theory that every weak equivalence, in this sense, is an actual equivalence. In other words, “Whitehead’s theorem” should not be provable.
For what it’s worth, I find that the Aczel quote that I had dug out here vindicates exactly this kind of suggestion (#7) and the attitude of the entry in general.
My feeling is that the complaint in #2 is about the would-be claim that the unprovability of taboos is itself provable, which the entry doesn’t actually claim, or doesn’t mean to claim (maybe the wording can be enhanced to clarify this). But, of course, what do I know.
Perhaps along the same lines as Urs, I wonder if the word ’known’ in the first sentence could be improved upon.
Otherwise I think this page is worth having; whether one uses the word ’taboo’ or something else is not something I have an opinion on!
Thanks Urs! It looks like Aczel did intend to include Brouwerian counterexamples. So as Urs and Richard said, we should definitely modify the paragraph not to claim that a taboo is known to be unprovable. What about something like
A taboo, for a particular flavor of mathematics or formal system, is a simple statement that is known, or intended, to be not provable therein. Therefore, if some other statement can be shown to imply the taboo, it follows that that statement also is not, or should not be, provable. When discussing a formal system, a taboo can 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) — although of course metamathematics had to be used to establish the unprovability of the taboo itself. When discussing an imprecisely specified flavor of mathematics, a taboo can be used to decide on statements that are “off-limits” without descending into philosophy, although similarly the philosophy was invoked to argue for the inadmissibility of the taboo in the first place.
(Or we could have separate paragraphs about taboos in formal systems and taboos in informal flavors of mathematics.)
Whitehead’s principle is what I call a “constructive-homotopical taboo”. It’s not a pure taboo for homotopy theory, since it holds in the classical model; nor is it a pure taboo for constructive mathematics, since it presumably holds in any model defined out of sets, even constructively. But it is a taboo if we want to include arbitrary -topos models that are both constructive and homotopical.
I’ve added in Whitehead’s principle.
I think of this as an informal terminology which is also not restricted to constructive mathematics. If you set up your classical logic with negation, you may write False (the constant \bot) for, say, “there exists an x with x unequal x”. Then to prove any proposition P to be false (i.e. to prove not P) is to prove
P -> False
We might phrase this as saying that P is “classically false”, we could also say P is “False-implying”.
People, under the implicit assumption that False is not provable in our system, casually say “P is unprovable” (e.g. 3^2=10 is supposedly unprovable in Peano arithmetic, because we assume False is unprovable). So for most theories in general, False is a taboo quite as described in the sense of the article. If the article wants to use the word taboo for formalized systems, it should probably not say “known”, since to e.g. “False is known to be unprovable” is a strong consistency claim. The claim that some formal theory (with explosion, constructive or not) is known not to prove certain statements (say whether constructive arithmetic proves all LEM instances or its other taboos) formally depends on whether we want to go as far and claim the theory is certainly consistent.
Now we can play this game with any proposition Q. We have a notion of being “Q-implying” or “Q-false.” And then “Constructively false” means Q-implying where Q is a theorem as listed in the article (omniscience principle, etc.). But again, I think we can use this language for all theories.
added impredicative polymorphism to weakly predicative constructive taboos section
Anonymouse
1 to 25 of 25