From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6992 Path: news.gmane.org!not-for-mail From: Steve Vickers Newsgroups: gmane.science.mathematics.categories Subject: Re: Empty algebras Date: Mon, 24 Oct 2011 10:53:14 +0100 Message-ID: References: <4EA1807A.1060802@cs.bham.ac.uk> Reply-To: Steve Vickers NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 (Apple Message framework v753.1) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Content-Transfer-Encoding: 7bit X-Trace: dough.gmane.org 1319459789 10084 80.91.229.12 (24 Oct 2011 12:36:29 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Mon, 24 Oct 2011 12:36:29 +0000 (UTC) Cc: Categories list To: Dusko Pavlovic Original-X-From: majordomo@mlist.mta.ca Mon Oct 24 14:36:25 2011 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtpx.mta.ca ([138.73.1.4]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1RIJlP-0000aj-I9 for gsmc-categories@m.gmane.org; Mon, 24 Oct 2011 14:36:23 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:36879) by smtpx.mta.ca with esmtp (Exim 4.76) (envelope-from ) id 1RIJk7-0002R1-6p; Mon, 24 Oct 2011 09:35:03 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1RIJk3-0002Ln-Mu for categories-list@mlist.mta.ca; Mon, 24 Oct 2011 09:34:59 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6992 Archived-At: Dear Dusko, You've missed the point about the adjunctions: that the adjunction is between two different contexts. Constructively we have two Heyting algebras here: H() has formulae (modulo equivalence) with no free variables, H(b) has formulae with at most one free variable, namely b. The inclusion homomorphism H() - > H(b) has right and left adjoints given by universal and existential quantification. The adjunction, or your proof, show that (all) a. P(a) --> (exists) x. P(x) is equivalent to true, or that (all) a. P(a) <= (exists) x. P (x), _in H(b)_. That's because it works by cutting P(b), which is present only in H(b). We should not conclude that it is equivalent to true in H(). The notation "(all) a. P(a) --> (exists) x. P(x)" conceals the difference, but it comes out clearly with a sequent calculus that keeps track of the possible free variables - see e.g. part C of the Elephant. With this notation you distinguish between, on the one hand, true |-(b) ((all) a. P(a) --> (exists) x. P(x)) or (all) a. P(a) |-(b) (exists) x. P(x) (both valid) and, on the other, true |-() ((all) a. P(a) --> (exists) x. P(x)) or (all) a. P(a) |-() (exists) x. P(x) (both not valid). All the best, Steve. On 23 Oct 2011, at 22:11, Dusko Pavlovic wrote: >> variable a. To avoid the vacuity and get a falsehood you have to >> quantify out the free variable, as >> >> ((all) a. P(a)) --> ((exists) x. P(x)) > > here is a proof of this apparent falsehood: > > (all) a. P(a) --> (all) b. P(b) (exists) b. P(b) > --> (exists) x. P(x) > -------------------------------- > ------------------------------------- > (all) a. P(a) --> P(b) P(b) > --> (exists) x. P(x) > ---------------------------------------------------------------------- > ----------------- > (all) a. P(a) --> (exists) x. P(x) > > > (it's is just adjunctions in foundations again: we compose the > counit of the adjunction of one quantifier with the unit of the > other one. note that it is valid constructively. i am not sure, but > i think gentzen gave a different proof in an example.) > > -- dusko [For admin and other information see: http://www.mta.ca/~cat-dist/ ]