Hi Eldad, John has replied to a few queries in other lectures about how to properly deal with the empty set as a special case (I don't have links to his comments at the moment). I would like a formal symbolic way of expressing the issue, but I haven't had the chance to give that a try.

The quantifiers \\(\forall\\) and \\(\exists\\) seem to take two opposite (dual?) approaches. I suspect that John's discussion in Chapter 1 relating the quantifiers to adjunctions are relevant, but I don't have specifics for you. When dealing with the empty set, \\(\forall\\) seems to be "vacuously" true, as they say, and \\(\exists\\) is always false.

I kind of think that what's going on is that there is an implicit set union happening inside the definitions of many of the operations we care about, and the empty set is the identity element for the union operator. The \\(\forall\\) quantifier seems to involve the logical operator "and", so any empty list of logical tests becomes true, the identity for "and". Similarly, the \\(\exists\\) quantifier is somehow related to the logical operator "or", and so applying an empty list of tests in that context yields false, the identity for "or".

I had hoped to try to formalize these guesses and ask John about it back when he was answering people's questions about the empty set, but the class moves too quickly for me to ask my questions while they're still relevant.

Anyway, even if my guesses aren't correct, I believe that it's correct that \\(\forall\\) applied to zero logical tests simply returns a value of true, and \\(\exists\\) applied to zero logical tests returns false.

The definition of a meet or join involves \\(\forall\\), so when applied to the empty set, the test just drops out. "The largest element \\(q\\) in \\(Q\\) such that \\(\forall q' \in S, q \leq q'\\)." The second clause is vacuously true for \\(S = \emptyset\\), so it becomes \\(\forall(\textrm{nothing to test}) = \textrm{true}\\). Thus the meet of the empty set reduces to just "The largest element \\(q\\) in \\(Q\\)".

I believe your proposed example fails to be a problem because to demonstrate transitivity, there is an implied \\(\exists\\). To apply the transitivity rule, you must produce an actual intermediate element \\(q'\\) and show that \\(q \cong q'\\) and \\(q' \cong q''\\). But in your example, \\(q'\\) is just a formal symbol used to sweep through all elements of the empty set; it never takes on any actual values, so there is no transitivity argument to be made.

*****

Now finally getting to your poset example, I'm going to assume that I had things correct in my previous post, that the meet of the empty set is the top element. That means \\(\bigwedge_Q \emptyset = 3\\) and \\(\bigwedge_P \emptyset = e\\). The proposed function \\(g\\) doesn't send 3 to e, so it's not meet preserving, and can't be a right adjoint.

However, your \\(g\\) does seem to preserve *joins* (and \\(Q\\) has all joins), so I think it can be a left adjoint. For the empty set, the joins are \\(1\\) and \\(a\\), which checks out. The right adjoint would send \\((a,c \mapsto 1), (b \mapsto 2), (d,e \mapsto 3)\\), if I calculated it correctly.

The quantifiers \\(\forall\\) and \\(\exists\\) seem to take two opposite (dual?) approaches. I suspect that John's discussion in Chapter 1 relating the quantifiers to adjunctions are relevant, but I don't have specifics for you. When dealing with the empty set, \\(\forall\\) seems to be "vacuously" true, as they say, and \\(\exists\\) is always false.

I kind of think that what's going on is that there is an implicit set union happening inside the definitions of many of the operations we care about, and the empty set is the identity element for the union operator. The \\(\forall\\) quantifier seems to involve the logical operator "and", so any empty list of logical tests becomes true, the identity for "and". Similarly, the \\(\exists\\) quantifier is somehow related to the logical operator "or", and so applying an empty list of tests in that context yields false, the identity for "or".

I had hoped to try to formalize these guesses and ask John about it back when he was answering people's questions about the empty set, but the class moves too quickly for me to ask my questions while they're still relevant.

Anyway, even if my guesses aren't correct, I believe that it's correct that \\(\forall\\) applied to zero logical tests simply returns a value of true, and \\(\exists\\) applied to zero logical tests returns false.

The definition of a meet or join involves \\(\forall\\), so when applied to the empty set, the test just drops out. "The largest element \\(q\\) in \\(Q\\) such that \\(\forall q' \in S, q \leq q'\\)." The second clause is vacuously true for \\(S = \emptyset\\), so it becomes \\(\forall(\textrm{nothing to test}) = \textrm{true}\\). Thus the meet of the empty set reduces to just "The largest element \\(q\\) in \\(Q\\)".

I believe your proposed example fails to be a problem because to demonstrate transitivity, there is an implied \\(\exists\\). To apply the transitivity rule, you must produce an actual intermediate element \\(q'\\) and show that \\(q \cong q'\\) and \\(q' \cong q''\\). But in your example, \\(q'\\) is just a formal symbol used to sweep through all elements of the empty set; it never takes on any actual values, so there is no transitivity argument to be made.

*****

Now finally getting to your poset example, I'm going to assume that I had things correct in my previous post, that the meet of the empty set is the top element. That means \\(\bigwedge_Q \emptyset = 3\\) and \\(\bigwedge_P \emptyset = e\\). The proposed function \\(g\\) doesn't send 3 to e, so it's not meet preserving, and can't be a right adjoint.

However, your \\(g\\) does seem to preserve *joins* (and \\(Q\\) has all joins), so I think it can be a left adjoint. For the empty set, the joins are \\(1\\) and \\(a\\), which checks out. The right adjoint would send \\((a,c \mapsto 1), (b \mapsto 2), (d,e \mapsto 3)\\), if I calculated it correctly.