# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorTodd_Trimble
• CommentTimeMar 12th 2012

I’ve inserted some proofs of statements made at Heyting algebra, particular on the “regular element” left adjoint to the full inclusion $Bool \to Heyt$.

The proof that $L \to L_{\neg\neg}$ preserves implication seemed harder than I was expecting it to be. Or maybe my proof is a clumsy one? If anyone knows a shorter route to this result, I’d be interested.

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeMar 12th 2012

That’s intriguing! I would have expected there to be an abstract reason for that, but I can’t think of one right now. Abstract nonsense implies that $Bool \to Heyt$ has a left adjoint, whose unit is then necessarily a Heyting algebra map, but then how can we identify the Boolean reflection with $L_{\neg\neg}$?

• CommentRowNumber3.
• CommentAuthorTodd_Trimble
• CommentTimeMar 12th 2012

Actually, your comment made me realize how all this is connected with the double negation translation (a page I have just started), which I would imagine requires machinations of the sort worked out at Heyting algebra.

Here’s something that actually took me by surprise: double negation on a Heyting algebra $\neg\neg: L \to L$ preserves not only finite meets, but the implication operation as well! It follows from this that the inclusion $L_{\neg\neg} \to L$ also preserves implication (contrary to what was stated before at Heyting algebra, so I guess this will take someone else besides me by surprise (-: ).

• CommentRowNumber4.
• CommentAuthorMike Shulman
• CommentTimeMar 12th 2012

That does at first seem a little surprising; but then when I think about it in terms of logic, it’s obvious. (-:

• CommentRowNumber5.
• CommentAuthorTodd_Trimble
• CommentTimeMar 12th 2012

Sorry, could you explain what you mean? Is there an easier way to see this than what I put down in Heyting algebra: Proofs?

• CommentRowNumber6.
• CommentAuthorTobyBartels
• CommentTimeMar 12th 2012

Todd, I just broke your last link by making it permanent: Heyting algebra: Proofs.

• CommentRowNumber7.
• CommentAuthorMike Shulman
• CommentTimeMar 12th 2012

No, I think I was jumping to unjustified conclusions and being confused, sorry.

• CommentRowNumber8.
• CommentAuthorTodd_Trimble
• CommentTimeMar 13th 2012

Toby, I see you made edits at Heyting algebra, in particular putting the remark in an environment. But it renders funny, and I can’t see what’s wrong with the syntax. Does it look funny to you, and if so can you fix it?

• CommentRowNumber9.
• CommentAuthorTobyBartels
• CommentTimeMar 13th 2012

It’s an subtle typo; I had

+-- {: un_remark}


when it should be

+-- {: .un_remark}


It’s fixed now.

• CommentRowNumber10.
• CommentAuthorTodd_Trimble
• CommentTimeMar 13th 2012

Oops! Yes, I see it now – thanks.

• CommentRowNumber11.
• CommentAuthorUrs
• CommentTimeMar 13th 2012
• (edited Mar 13th 2012)

when it should be

     +-- {: .un_remark}


I have a general suggestion: let’s use

      +-- {: .num_remark}


and similar by default. That’s more useful when an entry grows. (And all entries will grow eventually…)

• CommentRowNumber12.
• CommentAuthorTodd_Trimble
• CommentTimeMar 13th 2012

I think that’s a good suggestion, Urs (and I’ve begun doing that, but not consistently).

I’d like to propose another suggestion: when including redirects, make a point of including plural forms. That way a link can be made directly from the plural, without extra fuss.

• CommentRowNumber13.
• CommentAuthorMike Shulman
• CommentTimeMar 13th 2012

If we do use numbered theorem environements, I think we should always also include an anchor name:

+-- {: .num_remark #MyRemark}


IIRC there is an instiki bug that rears its head when some, but not all, of the numbered theorems on a given page have anchor names assigned.

• CommentRowNumber14.
• CommentAuthorUrs
• CommentTimeMar 13th 2012

Yes, very true.

On the other hand, maybe there is hope that this bug will disappear some day? I keep liking the idea that the software helps me save time, instead of me having to invest time to work around it…

• CommentRowNumber15.
• CommentAuthorMike Shulman
• CommentTimeMar 13th 2012
• CommentRowNumber16.
• CommentAuthorTobyBartels
• CommentTimeMar 14th 2012

Bug or no bug, there’s not much point to numbering the theorems/remarks/etc if you can’t refer to them later by number. And the only safe way to do that is with the anchors.

• CommentRowNumber17.
• CommentAuthorUrs
• CommentTimeMar 14th 2012
• (edited Mar 14th 2012)

Bug or no bug, there’s not much point to numbering the theorems/remarks/etc if you can’t refer to them later by number. And the only safe way to do that is with the anchors.

That’s what we currently do anyway, being forced by the bug: if I want to refer to something by number, I need to anchor everything in between in order for the numbers to come out right.

But what I am hesitant (no: unwilling) to do is to preemptively think up anchor names for everything in sight even before I refer to a single one. It would be good, I agree, but there is some limit being reached here.

• CommentRowNumber18.
• CommentAuthorTobyBartels
• CommentTimeMar 14th 2012

But what I am hesitant (no: unwilling) to do is to preemptively think up anchor names for everything in sight even before I refer to a single one.

Me too. But in that case, I just leave them unnumbered until I decide that I wish to refer to them.

I agree, the bug should be fixed; and when it is, then you can just make everything numbered to start with, without thinking of names. However, so long as you cannot think of a name, then numbering it gives you no additional benefit (and leaving it unnumbered works around the bug, while we have it).

• CommentRowNumber19.
• CommentAuthorTobyBartels
• CommentTimeMar 14th 2012

I’ve moved the comments on theorem numbering to their own thread: Theorem numbering.

• CommentRowNumber20.
• CommentAuthoreparejatobes
• CommentTimeMar 16th 2012
• (edited Mar 16th 2012)

I don’t know if what follows is shorter, but I think is clearer:

First, factor the ${\neg\neg}$ monad as

$L \to L_{\neg\neg} \to L$

and call the reflection $L \to L_{\neg\neg}$ also ${\neg\neg}$; the inclusion $L_{\neg\neg} \to L$ will be implicit. We obviously have

1. ${\neg\neg} \dashv i$
2. $i$ fully faithful
3. $i$ preserves and $L_{\neg\neg}$ has finite meets

From 3 we have that for $a,b \colon L_{\neg\neg}$

$a \wedge_{\neg\neg} b = a \wedge b = {\neg\neg}(a \wedge b)$

Now, everything is easy once we note that

$L_{\neg\neg}$ is an exponential ideal in $L$

This is almost immediate from the definition of $\neg(x) = x \Rightarrow 0$; for arbitrary $x,y \colon L$:

${\neg\neg}(x \Rightarrow y) = ((x \Rightarrow y) \Rightarrow 0) \Rightarrow 0 = x \Rightarrow ((a \Rightarrow 0) \Rightarrow 0) = x \Rightarrow ({\neg\neg}(y))$

that is,

• ${\neg\neg}(x \Rightarrow y) = x \Rightarrow ({\neg\neg} y)$

Now, from this if $x \colon L, a \colon L_{\neg\neg}$, then

${\neg\neg}(x \Rightarrow a) = x \Rightarrow ({\neg\neg} a) = x \Rightarrow a$

so that $x \Rightarrow a \colon L_{\neg\neg}$ and we get $L_{\neg\neg}$ exponential ideal.

#### $L_{\neg\neg}$ closed

We have, for $x,y,c \colon L_{\neg\neg}$:

$\begin{matrix} L_{\neg\neg}(x\wedge_{\neg\neg} y, c) \simeq \\ L(x \wedge y, c) \simeq \\ L(x, y \Rightarrow c) \simeq \\ L_{\neg\neg}(x, y \Rightarrow c) \end{matrix}$

Note that for $a,b \colon L_{\neg\neg}$ trivially

$a \Rightarrow_{\neg\neg} b = {\neg\neg}(a \Rightarrow b) = a \Rightarrow b$

and from this both

• the reflection $L \to L_{\neg\neg}$
• the inclusion $L_{\neg\neg} \to L$

are closed. We get then ${\neg\neg}$ closed.

The only thing left is

#### reflection preserves finite meets

Every functor between cartesian categories is colax monoidal, which here amounts to

${\neg\neg}(x \wedge y) \leq {\neg\neg}(x)\wedge_{\neg\neg} {\neg\neg}(y)$

(this is the easy one, of course). For the reverse, first note that Kleisli extension yields

$x \leq {\neg\neg} y \iff {\neg\neg} x \leq {\neg\neg} y$

Now, for $x,y \colon L, a = {\neg\neg} a \colon L_{{\neg\neg}}$

$\begin{matrix} & L(x\wedge y, a) \simeq \\ closed: & L(x, y \Rightarrow a) \simeq \\ a = {\neg\neg}a : & L(x, y \Rightarrow {\neg\neg} a) \simeq \\ props of {\neg\neg}: & L(x, {\neg\neg}(y \Rightarrow a)) \simeq \\kleisli + exp ideal: & L({\neg\neg}x, y \Rightarrow a) \simeq \\ closed: & L({\neg\neg}x \wedge y, a) \end{matrix}$

Applying the same steps to $y$, we get a bijection

$L(x\wedge y, a) \simeq L({\neg\neg}x \wedge {\neg\neg} y, c)$

Taking the map given by the unit at $x\wedge y$,

$x \wedge y \to {\neg\neg}(x \wedge y)$

we get what we were looking for:

${\neg\neg}x \wedge_{\neg\neg} {\neg\neg} y = {\neg\neg}x \wedge {\neg\neg} y \leq {\neg\neg}(x \wedge y)$

This is just Proposition A.4.3.1 of the Elephant adapted to this context.

As for $L_{\neg\neg}$ being a Boolean algebra, it follows at once from double negation in $L_{\neg\neg}$ being just the double negation of $L$ resctricted to $L_{\neg\neg}$. Then, for $a \colon L_{\neg\neg}$:

${\neg\neg}_{\neg\neg} a = {\neg\neg} a = a$

Summing up,

• the inclusion $L_{\neg\neg} \to L$ is

• fully faithful,
• closed, and
• preserves any (in particular finite) meets that exist in $L$
• the reflection $L \to L_{\neg\neg}$ is

• eso,
• closed, and
• preserves finite meets
• it also preserves joins, of course

From this we get that

• double negation ${\neg\neg} \colon L \to L$ is

• closed,
• and preserves finite meets

#### De Morgan?

By symmetry of $\wedge$, we get

$\neg \dashv \neg^{op}$

and ${\neg\neg} = \neg^{op}\neg$. It’d be nice if being De Morgan would be equivalent to this adjunction being an ambijunction

$\neg \dashv \neg^{op} \dashv \neg$

one such Heyting algebra is automatically De Morgan; guess there should be examples of De Morgan Heyting algebras for which $\neg^{op}$ is not left adjoint to $\neg$.

• CommentRowNumber21.
• CommentAuthorTodd_Trimble
• CommentTimeMar 16th 2012

Sorry, eparejatobes (I don’t know your given name) – how is the second equation in the second line after

$L_{\neg\neg}$ is an exponeital ideal in $L$

(where there is a typo – you mean $y$ instead of $a$) supposed to be obvious? I mean, I can prove it, but it’s not totally obvious to me without some calculation.

• CommentRowNumber22.
• CommentAuthoreparejatobes
• CommentTimeMar 17th 2012
• (edited Mar 17th 2012)

Hi Todd,

it’s Eduardo :)

Sorry, eparejatobes (I don’t know your given name) – how is the second equation in the second line after

L¬¬ is an exponeital ideal in L (where there is a typo – you mean y instead of a) supposed to be obvious? I mean, I can prove it, but it’s not totally obvious to me without some calculation.

Whoah! that’s wrong in many ways! don’t know what I was thinking when I wrote that. I mean, it may be true, but not obvious at all, and in fact I don’t know how to prove it :) Thanks for spotting it. I’ve been looking for a way to fix this, and found a nice proof of $\neg\neg$ perserving finite products in this lecture notes:

So, here follows what I have:

### negation

First of all, let’s state some properties of negation which will be of great use later on; most of them are direct consequences of the definition $\neg x = x \Rightarrow 0$; note that this means that

$x \wedge y = 0 \iff x \leq \neg y$
1. $\neg \dashv \neg^{op}$ from the symmetry of meets
2. $\neg \neg \neg = \neg$ because every poset adjunction is idempotent
3. $a \wedge b = 0 \iff a \wedge (\neg\neg b) = 0$ For this, take $a \wedge b = 0 \iff a \leq \neg b$, and from the previous one $a \leq \neg b \iff a \leq \neg\neg\neg b = \neg(\neg\neg b)$ and then this equivales to $a \wedge (\neg\neg b) = 0$.

We can factor the monad $\neg\neg$ coming from the $\neg \dashv \neg^{op}$ adjunction as:

$L \to L_{\neg\neg} \to L$

#### reflection preserves finite meets

Let’s see first that the reflection $\neg\neg$ preserves meets; as a reflective subcategory, we have that finite meets in $L_{\neg\neg}$ are just finite meets in $L$; so that $\neg\neg \colon L \to L_{\neg\neg}$ presrving finite meets is equivalent to

$\neg\neg(a\wedge b) = \neg\neg a \wedge \neg\neg b$

One inclusion is always true for a functor between posets with finite meets

$\neg\neg(a\wedge b) \leq \neg\neg a \wedge \neg\neg b$

(every functor between cartesian cats is colax monoidal). Now, for the other one:

$\neg\neg a \wedge \neg\neg b \leq \neg\neg(a\wedge b)$

$(\neg\neg a \wedge \neg\neg b) \wedge \neg(a\wedge b) = 0$

reorganizing this to

$(\neg\neg a \wedge (\neg\neg b \wedge \neg(a\wedge b)) = 0$

we can apply 3 to get

$a \wedge (\neg\neg b \wedge \neg(a\wedge b)) = 0$

doing the same with $b$ we arrive at

$(a \wedge b) \wedge \neg(a\wedge b) = 0$

which is always the case, via adjunction and the unit of $\neg\neg$:

$(a \wedge b) \leq \neg\neg(a\wedge b)$

From this we get that double negation also preserves finite meets.

#### $L_{\neg\neg}$ closed

This is in the Elephant, A.4.3.1. The key is noting that

$\neg\neg(x\wedge y) = \neg\neg x \wedge \neg\neg y = \neg\neg(\neg\neg x \wedge y)$

because of $\neg\neg$ idempotent. Now, taking $a \in L_{\neg\neg}$, $x,y \in L$ we have

$\begin{matrix} & L(x, y \Rightarrow a) \simeq \\ closed: & L(x\wedge y, a) \simeq \\ adjunction: & L(\neg\neg(x\wedge y), a) \simeq \\ property above: & L(\neg\neg(\neg\neg x\wedge y), a) \simeq \\ adjunction: & L(\neg\neg x \wedge y, a) \simeq \\ closed: & L({\neg\neg}x, y \Rightarrow a) \simeq \\ \end{matrix}$

So we have

$x \leq y \Rightarrow a \iff \neg\neg x \leq y \Rightarrow a$

So taking $y = \in L, x = y \Rightarrow a$ we get

$\neg\neg (y \Rightarrow a) = y \Rightarrow a$

that is, $L_{\neg\neg}$ is an exponential ideal. From this, it is immediate that

1. $L_{\neg\neg}$ is closed, with $\Rightarrow_{\neg\neg} = \Rightarrow$
2. $i$ closed

From this is easy to get that $L_{\neg\neg}$ is a Boolean algebra etc.

What I don’t know how to get is that also the reflection is closed. I mean, in a different way than what you have. Really nice the expression:

$\neg(a \Rightarrow b) = \neg\neg a \wedge \neg b$

haven’t seen that before.

So, sorry for the noise :)

Apart from that, does anyone knows something about Heyting algebras for which $\neg \dashv \neg^{op} \dashv \neg$? thanks!