From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7004 Path: news.gmane.org!not-for-mail From: Paul Levy Newsgroups: gmane.science.mathematics.categories Subject: Re: Empty algebras Date: Wed, 26 Oct 2011 12:31:45 +0100 Message-ID: References: <4EA1807A.1060802@cs.bham.ac.uk> <5E279F28-70B7-4393-A564-B95E3768C561@cs.bham.ac.uk> <36141083-FB05-4179-8C98-81D5D6EBB6B1@kestrel.edu> Reply-To: Paul Levy NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 (Apple Message framework v936) Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit X-Trace: dough.gmane.org 1319635145 16660 80.91.229.12 (26 Oct 2011 13:19:05 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Wed, 26 Oct 2011 13:19:05 +0000 (UTC) To: categories list Original-X-From: majordomo@mlist.mta.ca Wed Oct 26 15:19:01 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 1RJ3Nh-0005dF-LO for gsmc-categories@m.gmane.org; Wed, 26 Oct 2011 15:18:57 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:47771) by smtpx.mta.ca with esmtp (Exim 4.76) (envelope-from ) id 1RJ3MU-00006H-4y; Wed, 26 Oct 2011 10:17:42 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1RJ3MS-0005yw-Fo for categories-list@mlist.mta.ca; Wed, 26 Oct 2011 10:17:40 -0300 Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7004 Archived-At: On 25 Oct 2011, at 19:02, Vaughan Pratt wrote: > The rationale I gave on Monday for sticking to the standard > axiomatization of first order logic, which proves Dusko's formula, > Steve's objection to it notwithstanding, was as follows. > >> But it is just as reasonable to say there are variables even when >> they >> don't occur free in the formula, e.g. when they occur bound, and the >> opposite result then obtains. The wffs of propositional calculus, >> L_0, >> don't even contain bound variables. Since this convention seems to >> create fewer problems I'm inclined to prefer it. > > "Seems to create fewer problems" being the sort of sentence any > Wikipedia editor would these days tag as "weasel words", I should be > more explicit about the sorts of problems it can create. > > If I've understood Steve's reasoning, he accepts > > TRUE(a) --> (exists) x. TRUE(x) > > as a theorem of FOL that holds even in the empty universe, on the > ground > that it is "vacuously true" (where I would have said vacuously valid). I think a source of confusion in this debate is the idea that there is a single FOL. Surely we should speak of FOL(Sigma), where Sigma is a signature i.e. a collection of function symbols and predicate symbols, each with an arity. If P is a unary predicate in Sigma, then (for all x. P(x)) => (exists x. P(x)) is a theorem of FOL(Sigma) iff Sigma contains at least one constant (nullary function symbol). That is for single-sorted predicate logic. More generally, given a set S of "sorts", we can take Sigma to be an S-sorted signature (meaning that each function symbol has a sort, and each position within each arity has a sort). If P is a predicate in Sigma with one argument of sort A, then (for all x:A. P(x)) => (exists x:A. P(x)) is a theorem of FOL(Sigma) iff there is at least one closed term of sort A built from the function symbols of Sigma. For example, if Sigma contains a constant of sort A. I think the multi-sorted setting makes the whole issue clearer, because it's perfectly natural and indeed useful to have a variety of sorts of which some are empty and some are not. regards, Paul > > The same reasoning would also appear to justify > > TRUE(a) > > as a theorem of FOL. (Note that both formulas are standard FOL > theorems, with both holding in every nonempty universe.) > > But by Modus Ponens, which I can't imagine Steve rejecting, we obtain > > (exists) x. TRUE(x) > > which Steve has judged as false. > > Since falsehood is the criterion by which Steve has been judging > theoremhood, unless I've misinterpreted Steve it seems to me that his > approach to handling the empty universe is unsound. > > For ease of reference I've put online my proof that cylindric algebra > semantics handles all this in stride by making the pertinent Boolean > algebra the one-element inconsistent one whenever Steve and Dusko > disagree on this point. Currently it's at > http://boole.stanford.edu/Empty/ but I'm open to suggestions for a > suitable more permanent resting place. > > Vaughan -- Paul Blain Levy School of Computer Science, University of Birmingham +44 (0)121 414 4792 http://www.cs.bham.ac.uk/~pbl [For admin and other information see: http://www.mta.ca/~cat-dist/ ]