Re: Empty algebras

[Steve Vickers <s.j.vickers@cs.bham.ac.uk>]

Dear Vaughan -

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.

To count the bound variables in the context is a crudeness that loses
information. For example, it implies there are problem with (all) a.
TRUE(a) and (exists) a. FALSE(a). Both are in fact theorems in the empty
context.

>
> "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).
>
> 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.

To avoid any misunderstanding, it's not my approach to handling the
empty universe - it has been around for a long time, I believe it
originated with Mostowski, and it is present well in the Elephant D.

It relies on conducting each logical deductions within a specified
context that describes which free variables are available for use. A
theorem phi proved in context (a1, ..., an) is implicitly

   (all) a1...an. phi

To put it another way, when you quantify out to get a theorem in the
empty context, that is what it is.

The theorems

   TRUE(a)
   TRUE(a) --> (exists) x. TRUE(x)

can only be in a context that has at least a, and applying modus ponens
leaves us with

   (exists) x. TRUE(x)

as a theorem _in that same context_. It is wrong to say (exists) x.
TRUE(x) is a theorem without specifying the context. In the empty
context it becomes the theorem

   (all) a. (exists) x. TRUE(x)

All the best,

Steve.


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]