Dear Michael, Yes, that's what I've been saying: the meet is not always less than the join. Steve. Michael Barr wrote:
Maybe I'm naive, but I don't see why meet is always below join. Certainly that's usually the case but the empty meet is top and empty join is bottom and I think that is what this is all about.
Michael
On Mon, 24 Oct 2011, Steve Vickers wrote:
Dear Dusko,
First of all, what your "tautology" says is semantically incorrect in the case where A is empty: for then the meet of P is true and the join is false, so we don't have that the meet is lower than the join. Constructively, the product is an empty product and hence 1, while the coproduct is 0 and there is no morphism from the product to the coproduct. The composite morphism
(all) x.P(x) --> P(a) --> (exists) x.P(x)
exists only when we have a in A.
Second, in your proof with contexts, you use "the equivalence true |-() ((all) b. ((all) a. P(a) --> (exists) x. P(x))) <-> (((all) a. P(a) --> (exists) x. P(x)))"
You didn't give a proof of this equivalence, but anyway we have a counterexample. When A is empty, (all) a. P(a) and (exists) x. P(x) are true and false respectively, so (all) a. P(a) --> (exists) x. P (x) is false. But
(all) b. ((all) a. P(a) --> (exists) x. P(x))
is true, so the biequivalence is false.
Regards,
Steve.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]