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.
Can we take Mike’s suggested definition as accepted:
Let’s say that an -topos is Boolean if for every object , the lattice of subobjects (i.e. -truncated morphisms into ) is a Boolean algebra. I think this is equivalent to asking that the subobject classifier be an internal Boolean algebra, and hence to asking that the underlying 1-topos of 0-truncated objects is Boolean in the classical sense.
We’d need something along this line for Prop. 3 at Aufhebung which claims to work for the case as well as the 1-case, but relies only on the properties of
But the subtopos of sharp-modal types is which is clearly a 2-valued Boolean topos.
Do we want something along the lines of as Boolean -topos?
Concerning the -case, though this isn’t really my turf, I would think it conceptually more pleasing to have a definition that involves the full type theory and not only invoke (-1)-truncation though hopefully it would eventually boil down to something along the suggested propositional line.
Concerning Prop. 3, note that already in the (0,1)-case, it can readily be improved by invoking Prop. 5 at double negation and is in fact valid for Boolean base in general not only . Moreover, I think it is by now also subsumed by the more general results in the Lawvere-Menni paper though at the time of its writing Prop. 3 was one of the first general results on Aufhebung out in the open (due to Urs).
Looking at the Sierpinski topos suggests that what one should go after for the Aufhebung in is to look at the Aufhebung of that in and the way is imported into (e.g. in the Sierpinski topos preservation of 0 by the ’fringe functor’ seems to be crucial).
The thing about excluded middle is that it really only makes sense for (-1)-types. You can write down a “law of excluded middle” without the truncation hypotheses in type theory, but it’s inconsistent with univalence (3.2.7 in the HoTT Book). I take this as an argument for the unnaturalness of excluded middle. (-:
An alternative would be to settle for a less logical definition of Booleanness along some other characterization e.g. as a topos that has precisely one dense subtopos etc.
Me personally, though this is even less my turf, I wouldn’t dump a good definition of LEM for univalence, after all LEM is also incompatible with sufficient cohesion in the (0,1)-case and this does not mean that the definition is unnatural, merely that you have to let go LEM when working with sufficiently cohesive toposes !? It is surely interesting though that things like LEM or the De Morgan laws appear to have their natural habitat in the lower depth of type theory!
I wouldn’t dump a good definition of LEM for univalence
You realize that univalence is part of the definition of -topos? So strong-LEM contradicting univalence means that it is false in all -toposes, including .
Yes, the object classifier characterization is probably the version that looks most like the type-theoretic version of univalence.
Is it known how far this incompatibility goes into the intermediate logics between Boolean and intuitionistic logic?
That’s a good question; I don’t know the answer offhand. Are you thinking of things like de Morgan’s law?
At De Morgan topos are a couple of references concerning the type of intermediate logics that I have on my mind.
In particular the Lee identites in the Bagchi papers and the intermediate logics in Olivia Caramello’s (2012) provide systems of logics with diminishing strength of ’LEM’.
The results of Mielke there stating that De Morgan toposes lack non-trivial interval objects also somewhat suggest that the De Morgan does not fare better than the ordinary LEM when it comes to -toposes.
Offhand the result of Mielke doesn’t seem to have anything to do with -toposes; I see that it uses words like “homotopically”, but the mathematics is actually only talking about 1-toposes.
In fact, I think now that probably the naive “strong” form of de Morgan’s law (analogous to the “strong” LEM that’s inconsistent with univalence) is actually consistent, and follows from the (-1)-type version of LEM. Because it’s a statement like , and and are both (-1)-types, so no impossible “naturality” happens.
Back to what I quoted in #1, the ’two-valued’ there wasn’t linked, so I’ve sent that to two-valued logic.
Generally speaking, two-valuedness is an external property, and booleanness is an internal property.
Does that throw up any issues in the case?
I would probably define two-valuedness for an -topos to also be just about its underlying 1-topos; I’m not sure what else to do.
@#10: there is also some information on two-valued toposes at dense subtopos which might suit the reader in the context of Prop.3 at Aufhebung.
@#9: As I understand you, the definition of an De Morgan -topos would amount to say that the underlying 1-topos is De Morgan!? How different then is the -DML ultimately from -LEM since both seem to live exclusively at the truncated level ? It would be helpful to have some information on the -case at the De Morgan topos entry eventually.
What I’m saying is that there are two ways of formulating LEM — one of which is only about the underlying 1-topos, and the other of which is inconsistent — but only one way of formulating DML, which is only about the underlying 1-topos.
1 to 13 of 13