Re: Empty algebras

[Paul Levy <P.B.Levy@cs.bham.ac.uk>]

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/ ]