Empty algebras

Empty algebras

[Michael Barr]

I just wanted to comment on the "empty algebra" business.  Every person
conversant in CT ought to know this.

I had never heard the "clean-shaven gods" argument, but another
substantive reason logicians give for avoiding empty models is that it
messes up ultraproducts.  Specifically, an ultraproduct will be empty if
even one factor is.  This can be totally avoided by using a better
definition of ultraproduct.  Simply define as the (directed) colimit,
taken over all the sets in the ultrafilter, of all the large products.
Now the ultraproduct will be empty iff the set of empty factors is large.

Incidentally, I like the idea of the -1 cell.  It means that the Euler
characteristic of any simplex (and any contractible space) is 0, which is
the number of holes.  But it also makes the whole detour into "reduced
homology" unnecessary.

Michael


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

Re: Empty algebras

[Steve Vickers]

Dear Michael,

What Vaughan called the "clean-shaven gods" argument is, I think, the
normal logicians' excuse for barring empty carriers.

The logical deduction

   (all) x. P(x)
   -------------
   P(a)
   -------------
   (exists) x. P(x)

is false for empty carriers, but many logicians persuade themselves that
the deduction is correct and the empty carriers are therefore monsters.

Vaughan I think is taking P(x) as "x is clean-shaven" in the theory of gods.

You can get a similar phenomenon with equational reasoning, especially
for many-sorted algebras. I expect this is what bothered Meinke and
Tucker when they wrote their monograph on universal algebra.

The fix was discovered by Mostowski (I believe). To use a free variable
such as a is to hypothesize a denotation for it in the carrier.
Therefore in each deduction one should be explicit about the context of
free variables that may be used. This deals cleanly with empty carriers.

All the best,

Steve.

Michael Barr wrote:
> I just wanted to comment on the "empty algebra" business.  Every person
> conversant in CT ought to know this.
>
> I had never heard the "clean-shaven gods" argument, but another
> substantive reason logicians give for avoiding empty models is that it
> messes up ultraproducts.  Specifically, an ultraproduct will be empty if
> even one factor is.  This can be totally avoided by using a better
> definition of ultraproduct.  Simply define as the (directed) colimit,
> taken over all the sets in the ultrafilter, of all the large products.
> Now the ultraproduct will be empty iff the set of empty factors is large.
>
> Incidentally, I like the idea of the -1 cell.  It means that the Euler
> characteristic of any simplex (and any contractible space) is 0, which is
> the number of holes.  But it also makes the whole detour into "reduced
> homology" unnecessary.
>
> Michael
>



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

Re: Empty algebras

[Vaughan Pratt]

On 10/21/2011 7:23 AM, Steve Vickers wrote:
> What Vaughan called the "clean-shaven gods" argument is, I think, the
> normal logicians' excuse for barring empty carriers.

That's my alternative to St. Augustine's proof of the existence of god,
with "clean-shaven" thrown in to draw attention away from the real
fallacy (one would no more portray God without a beard than Santa Claus).

What I don't understand is why the emphasis on existence to the
exclusion of uniqueness, given that monotheism is the intellectual
descendant not of atheism but polytheism.  The only explanation I've
been able to come up with is that uniqueness is an equational property
(g = g') and therefore admissible as an axiom, say as part of the
definition of god.  Postulating existence in a definition is an obvious
cheat since the definition might be inconsistent.  A minimal requirement
for an existence proof is a consistency proof, which are tough to begin
with and get increasingly tougher with increasing scientific understanding.

>
> The logical deduction
>
>    (all) x. P(x)
>    -------------
>    P(a)
>    -------------
>    (exists) x. P(x)

Even simpler: P(a) --> (exists) x. P(x) is a theorem of the pure
predicate calculus, which is "clearly" false in the empty universe when
P is taken to be the identically true predicate.

> The fix was discovered by Mostowski (I believe). To use a free variable
> such as a is to hypothesize a denotation for it in the carrier.
> Therefore in each deduction one should be explicit about the context of
> free variables that may be used. This deals cleanly with empty carriers.

If you use cylindric algebras B as the subalgebras of the Boolean
algebra 2^D^V of all V-ary relations on a domain D, there is nothing to
fix.   Given a first order language L of wffs over a set X of variables,
for each subset V of X, let L_V denote those wffs of L using variables
from V, and for each D and each B as above let I_B: L_V --> B interpret
the wffs of L_V in B subject only to requirement T0 below.  Define the
theory T(L) to consist of those wffs P of L such that every I_B having P
in its domain map P to the top element of B.  Requirement T0 is that the
intersection of T(L) and L_0 consist of the propositional tautologies.

(Every reasonable notion of classical pure predicate calculus must
surely satisfy these extremely mild conditions, which shouldn't be too
hard to phrase appropriately for intuitionist logic as well.)

Claim.  T(L) is independent of whether D = 0 is forbidden.

Proof.  Allowing D = 0 can only decrease T(L).  There are two cases.

1.  V > 0.  In this case D^V = 0 whence B has only one element and so
I_B maps *every* wff to the top element of B.  This cannot decrease T(L).

2.  V = 0.  This is propositional calculus, for which requirement T0
makes the choice of D irrelevant.  QED

I noticed this property of cylindric algebras when I first ran across
them in mid-1979 and assumed it must be well-known since Tarski and
Henkin had been playing around with them since the 1950s and could
hardly have overlooked such an elementary fact.  A month later I
attended the sixth International Congress of Logic, Methodology, and
Philosophy of Science in Hannover where I met a number of algebraic
logicians for the first time: Routley, Dunn, Nemeti, Andreka, Maksimova,
etc.  When Nemeti and Andreka told me they were working with Henkin,
Monk and Tarski on Vol. 2 of Cylindric Algebras, I asked them if they
were aware that cylindric algebra semantics solved the
logic-of-the-empty-universe problem.  They said no so I showed them the
argument.  Since they were much better connected to the cylindric
community than I, I figured they'd pass it on, relieving me of any
obligation to write up what seemed to me little more than a passing
remark.  I was hoping it might appear in Vol. 2 but I don't see it there.

Vaughan


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

Re: Empty algebras

[Steve Vickers]

Dear Vaughan, -

On 21 Oct 2011, at 23:06, Vaughan Pratt wrote:

>>
>> The logical deduction
>>
>>    (all) x. P(x)
>>    -------------
>>    P(a)
>>    -------------
>>    (exists) x. P(x)
>
> Even simpler: P(a) --> (exists) x. P(x) is a theorem of the pure
> predicate calculus, which is "clearly" false in the empty universe
> when
> P is taken to be the identically true predicate.

No, that's wrong.

Your formula P(a) --> (exists) x. P(x) is valid in the empty carrier,
because it is (vacuously) true under every interpretation of the free
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))

Steve.



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

Re: Empty algebras

[Vaughan Pratt]

On 10/22/2011 6:03 AM, Steve Vickers wrote:

>> Even simpler: P(a) --> (exists) x. P(x) is a theorem of the pure
>> predicate calculus, which is "clearly" false in the empty universe
>> when P is taken to be the identically true predicate.
>
> No, that's wrong.

You may have overlooked the scare quotes.

> Your formula P(a) --> (exists) x. P(x) is valid in the empty carrier,

I agree, but I said "false," not "invalid."

> because it is (vacuously) true under every interpretation of the free
> variable a.

This would only make sense if you identify truth and validity.
The formula is vacuously *valid* under every interpretation.

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

Your "have to" here brings to mind Dan Dennett's chapter "Qualia
Disqualified" in his 1991 book "Consciousness Explained."  Concerning
"if a tree falls in the forest and there is no one to hear it, does it
make a sound?", Dennett says "The answer is left as an exercise for the
reader."  Dennett appears to reject the possibility of two answers
depending on whether "sound" is considered a physioacoustic or
psychoacoustic phenomenon on the ground that it can't be the latter
since (if I understand his argument on pages 370-411) there is no
coherent notion of the latter.  (How could anyone doubt this after 40
pages?)  Dennett's argument in turn brings to mind the argument that,
since we can't pin down climate sensitivity to better than a range of
1.5 to 5 degrees per doubling of CO2, global warming can't be real.

What we have here is the logical counterpart of "no one to hear the
sound" as "no interpretation to witness the truth."  The distinction
between physioacoustic and psychoacoustic becomes that between
physio-logical and psycho-logical, truth vs. validity.

But did the tree actually fall?  Is "P(a) --> (exists) x. P(x)" (context
should make clear that those are not intended as scare quotes) actually
false as I claim?

Enter the scare quotes on "clearly," and enter Tarski pointing out that
truth can't be defined.

For this sentence it's not impossible to define truth, it's just that
there's no canonical definition, since in the empty universe the truth
of P(a) becomes an incoherent notion, leaving one at liberty to define
it however you wish.  Correct me if I've misunderstood but you
(following Mostowski?) appear to have chosen to assign "true" to every
non-closed formula, which stops the bleeding, a victory for first aid.

CCA, concrete cylindric algebras, namely subalgebras of the Boolean
algebra 2^D^V, handle all this automatically when D = 0.  When the
formula contains no variables at all, free or bound (i.e. propositional
calculus, V=0), D^V = 0^0 = 1 and B = 2 as appropriate for propositional
calculus.  That is, absent both individuals *and* variables, CCA
automatically becomes ordinary propositional calculus.

But if V is nonempty then D^V = 0 and B = 2^0 = 1, the inconsistent
Boolean algebra.

*CCA automatically recognizes the inconsistency of trying to define
truth in the empty universe when the formula contains variables.*

With CCA there is no need to staunch the bleeding because the patient
was not injured in the first place.  With other semantics, which
invariably disallow B = 1, YMMV as they say.

On 10/22/2011 3:36 PM, Dusko Pavlovic wrote:

  > maybe it's time that we all recall lawvere's "Adjunctions in
  > foundations", that appeared some 35 years ago. in its best times,
  > categorical logic offered powerful tools to expand our logical
  > intuitions.

The version of my proof (that CCA handles this problem in stride) that I
told to Andreka and Nemeti assumed a fixed V, per the usual convention
among cylindric algebraists (whatever their radius).  Knowing how
strongly Bill feels about cylindric algebra, and anticipating that he
would surely object to my argument in that form, I tweaked it slightly
by introducing a master set X of variables so as to be completely
consistent not only with Bill's nice way of handling quantifiers, which
requires allowing V to vary, but even the most egregious ways including
those in the Cylindric Algebra volumes.  You will hopefully have noticed
that the only property of interpretations I_B that I required was that
they interpret propositional formulas (V = 0) so as to make T(L) agree
with standard propositional logic.  The proof does not depend on how
quantification is defined, and is just as sound for Bill's approach as
for anyone else's.

Vaughan


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

Re: Empty algebras

[Dusko Pavlovic]

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

Re: Empty algebras

[Vaughan Pratt]

On 10/23/2011 2:11 PM, 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:

As long as "true" and "valid" are used interchangeably one is going to
encounter repeated confusions.

I don't know what Steve had in mind in his passage from
P(a) --> (exists) x. P(x)
to
((all) a. P(a)) -->  ((exists) x. P(x))
given that these say different things.  The first says that if P holds
of a it holds of some x, for example x = a.  The second says that if P
is the constantly true predicate then it must hold of some x.

But what does the latter mean?  Steve says it's false in the empty
universe, which is to say (exists) x. TRUE(x) is false there.  We can
confirm this by taking the meaning of this formula in the universe {a_1,
a_2, ...} to be TRUE(a_1) v TRUE(a_2) v ..., which in the empty universe
is the empty disjunction, by convention false.

But could it still be valid, meaning true in all interpretations?  The
possible interpretations of a set V of variables form the set D^V.  When
D = 0, D^V can be thought of as the (intuitionistic) negation of V:
there are interpretations iff there are no variables.

So if there are variables there are no interpretations whence Steve's
formula is vacuously valid, consistent with you (Dusko) having a proof
of the formula.

Conversely no variables implies not valid, consistent with what Steve
seems to have in mind.

In the case of a formula with free variables, there is no question there
are variables.  But this particular formula is a (closed) sentence, so
no free variables, so there exist interpretations, whence the formula is
not valid.

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.  It justifies Dusko's
proof, while arguing against Steve's position that the formula is not
valid.  There is no question however that the formula is not true, and
given that Steve has not yet made a sharp distinction between truth and
validity, it is perhaps not unreasonable to defend Steve's position by
interpreting him as talking about the truth of
((all) a. P(a)) -->  ((exists) x. P(x))
rather than its validity.

Vaughan


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

Re: Empty algebras

[Steve Vickers]

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

Re: Empty algebras

[Dusko Pavlovic]

hi steve,

i am afraid that the "falsehood"

(all) x.P(x) => (exists) x.P(x) 

is a *tautology* of predicate logic, in any topos, for any predicate P:A-->Prop, with or without the free variables hanging around. if it helps, think of P:A-->Prop as an A-indexed set of elements of the lattice Prop. then 

  	(all) x.P(x) is the meet of P, whereas
 	(exists) x.P(x) is the join of P,

and the tautology says the meet is lower than the join. or constructively,

 	(all) x.P(x) is the product of the A-indexed family P(x) 
 	(exists)x.P(x) is the coproduct

so that

 	(all) x.P(x) -->P(a) is a projection, and
 	P(a) --> (exists) x.P(x) is an injection.

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

to prove these last two formulas, observe that
from 
 	true |-(b) ((all) a. P(a) --> (exists) x. P(x))
we can derive
 	true |-() (all) b. ((all) a. P(a) --> (exists) x. P(x))
now use the equivalence
 	true |-() ((all) b. ((all) a. P(a) --> (exists) x. P(x))) <-> (((all) a. P(a) --> (exists) x. P(x)))
to conclude that the RHS is true. 

-- dusko

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

Re: Empty algebras

[Steve Vickers]

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.

On 24 Oct 2011, at 13:35, Dusko Pavlovic wrote:

> hi steve,
>
> i am afraid that the "falsehood"
>
> (all) x.P(x) => (exists) x.P(x)
>
> is a *tautology* of predicate logic, in any topos, for any
> predicate P:A-->Prop, with or without the free variables hanging
> around. if it helps, think of P:A-->Prop as an A-indexed set of
> elements of the lattice Prop. then
>
>  	(all) x.P(x) is the meet of P, whereas
> 	(exists) x.P(x) is the join of P,
>
> and the tautology says the meet is lower than the join. or
> constructively,
>
> 	(all) x.P(x) is the product of the A-indexed family P(x)
> 	(exists)x.P(x) is the coproduct
>
> so that
>
> 	(all) x.P(x) -->P(a) is a projection, and
> 	P(a) --> (exists) x.P(x) is an injection.
>
>> 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).
>
> to prove these last two formulas, observe that
> from
> 	true |-(b) ((all) a. P(a) --> (exists) x. P(x))
> we can derive
> 	true |-() (all) b. ((all) a. P(a) --> (exists) x. P(x))
> now use the equivalence
> 	true |-() ((all) b. ((all) a. P(a) --> (exists) x. P(x))) <->
> (((all) a. P(a) --> (exists) x. P(x)))
> to conclude that the RHS is true.
>
> -- dusko



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

Re: Empty algebras

[Michael Barr]

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.
>
> On 24 Oct 2011, at 13:35, Dusko Pavlovic wrote:
>
>> hi steve,
>>
>> i am afraid that the "falsehood"
>>
>> (all) x.P(x) => (exists) x.P(x)
>>
>> is a *tautology* of predicate logic, in any topos, for any
>> predicate P:A-->Prop, with or without the free variables hanging
>> around. if it helps, think of P:A-->Prop as an A-indexed set of
>> elements of the lattice Prop. then
>>
>>   (all) x.P(x) is the meet of P, whereas
>>  (exists) x.P(x) is the join of P,
>>
>> and the tautology says the meet is lower than the join. or
>> constructively,
>>
>>  (all) x.P(x) is the product of the A-indexed family P(x)
>>  (exists)x.P(x) is the coproduct
>>
>> so that
>>
>>  (all) x.P(x) -->P(a) is a projection, and
>>  P(a) --> (exists) x.P(x) is an injection.
>>
>>> 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).
>>
>> to prove these last two formulas, observe that
>> from
>> 	true |-(b) ((all) a. P(a) --> (exists) x. P(x))
>> we can derive
>> 	true |-() (all) b. ((all) a. P(a) --> (exists) x. P(x))
>> now use the equivalence
>> 	true |-() ((all) b. ((all) a. P(a) --> (exists) x. P(x))) <->
>> (((all) a. P(a) --> (exists) x. P(x)))
>> to conclude that the RHS is true.
>>
>> -- dusko
>


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

Re: Empty algebras

[Steve Vickers]

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

Re: Empty algebras

[Vaughan Pratt]

On 10/24/2011 6:57 AM, Steve Vickers wrote:
> while the coproduct is 0

Indeed, as I pointed out on Monday where I wrote:

> Steve says it's false in the empty
> universe, which is to say (exists) x. TRUE(x) is false there.  We can
> confirm this by taking the meaning of this formula in the universe {a_1,
> a_2, ...} to be TRUE(a_1) v TRUE(a_2) v ..., which in the empty universe
> is the empty disjunction, by convention false.

Steve also makes the following nice point.

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

This last step follows from Steve's point that the empty meet is top.

Yet another way of analyzing this, also constructive if we view dynamic
logic as "constructive" in some sense, is as I proposed in my 1976 paper
"Semantical Considerations on Floyd-Hoare Logic," namely as the box and
diamond modalities for the nondeterministic assignment x := ?, which is
the binary relation consisting of all pairs (I, I') where I' is the
interpretation (world, state) obtained from I by setting x to an
arbitrary value from the domain.

For the empty domain, x := ? is the empty program 0, having the property
[0]P = 1 and <0>P = 0 for all formulas P.

That's not to say I agree with Steve's argument, which is the same one
certain universal algebraists (not Tarski to my knowledge) used to make,
both in Volume 1 of the McKenzie, McNulty and Taylor book (1987, out of
print, 2nd hand price $253.99 at Amazon, Volume 2 is currently being
written according to Ralph Freese) and at the 1993 MSRI conference
Universal Algebra and Category Theory, namely that the empty universe
rendered certain standard theorems of predicate calculus false, for
example the one Dusko cited.

Both Dusko's proof of "(all) x.P(x) => (exists) x.P(x)" and Steve's
counterexample to its truth have (modulo precise choice of example) been
standard fare in logic for well over half a century.  (I first heard
about this so-called "logic of the non-empty universe," LNEU, from a
curmudgeonly Philosophy I tutor at St. Andrews college in 1961, and was
duly impressed: how one should reason in the empty universe seemed a
small point in logic but a giant leap for philosophy from the question
of how many angels could dance on the head of a pin.)

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

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


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

Re: Empty algebras

[Steve Vickers]

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

Re: Empty algebras

[Vaughan Pratt]

On 10/26/2011 3:11 AM, Steve Vickers wrote:
> 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.

I guess this would be on p.811 of Volume 2.  But I don't see any mention
of Mostowski there.  Where can one find Mostowski's account?  And when
did he propose it?

> 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_.

Ok, so it would appear that there are two rather different approaches to
making FOL "safe" for the empty universe, one syntactic and the other
semantic.

1.  Replace the usual notion of first order logic (as treated in a great
many textbooks) with one in which formulas carry along contexts governed
by rules that are part of inference rules like Modus Ponens.  The
variables comprising these contexts could be typed or untyped.

2.  Leave the language, axioms, and rules of first order logic unchanged
from how it's been treated for a great many decades, and instead modify
just the semantics so that there is only one truth value in the
inconsistent situation where the universe is empty yet there are free
variables needing values.

I gave pretty complete details of how 2 would work at
http://boole.stanford.edu/Empty , based on D^V being empty when D is
empty and V is not, making 2^D^V = 1.

I am willing to believe that 1 can be made to work consistently, though
I would be interested to see the details.

Since logic courses may not want to be forced to modify their curriculum
to introduce contexts, nor to remove them, it would seem beneficial to
have both the above options, chosen according to the needs of the course
and the preferences of the instructor.

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

This serves as an example of why the rules for option 1 need to be
spelled out in detail.  If the context is empty, where did a come from?
   And how did it get to be universally quantified?  By making
generalization mandatory?  Is all this codified in one place, and if so
where?  If the Elephant, then it would be helpful to have an explicit
list of axioms in one place.  These may exist in the Elephant, but they
seem rather scattered around, making them something of a moving target.
   The rules of the pure untyped predicate calculus are well known, they
were established in the first half of century, and their completeness
was shown by Goedel.

Vaughan


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

Re: Empty algebras

[Steve Vickers]

Dear Vaughan,

There's always a chance I'm wrong about Mostowski. I was going by a
mention in Lambek and Scott, but I'm not sure I tracked down the
reference. In any case, the technique is well developed. The details
in the Elephant are at pp.830-1. It's in sequent form, which allows
it to be applied to logics without implication as a connective.
However, with implication you can move everything to the right.

I looked at your article on the web. As I suspected, your treatment
of all variables, free or bound, as part of the context V loses
subtlety. An empty carrier is in effect treated as an inconsistent
object for the purposes of determining the semantics of any formula
with variables. For them FALSE and TRUE are identified, and so it is
impossible to discriminate between (exists) x. TRUE(x) (as false) and
(all) x. FALSE(x) (as vacuously true). To make that discrimination
you have to be able to work soundly with the empty context.

To put it bluntly, your idea of treating all variables as part of the
context works by saying FALSE is TRUE in the case of empty carriers.
I don't believe your proposed semantics is a satisfactory one.

You ask where a came from in something like (all) a. (exists) x. TRUE
(x). The answer is that it didn't, or not yet. It is symbolic of a
hypothetical element. In asserting the formula we say that _if_
someone brings us an a then we promise to deliver an x such that TRUE
(x) holds. Game theoretically we are safe whatever the carrier, since
our x can just be a. But in addition for the empty carrier we know we
will be undisturbed since no one will ever have an a to bring us.

Regards,

Steve.


On 27 Oct 2011, at 11:08, Vaughan Pratt wrote:

>
> On 10/26/2011 3:11 AM, Steve Vickers wrote:
>> 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.
>
> I guess this would be on p.811 of Volume 2.  But I don't see any
> mention
> of Mostowski there.  Where can one find Mostowski's account?  And when
> did he propose it?
>
>> 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_.
>
> Ok, so it would appear that there are two rather different
> approaches to
> making FOL "safe" for the empty universe, one syntactic and the other
> semantic.
>
> 1.  Replace the usual notion of first order logic (as treated in a
> great
> many textbooks) with one in which formulas carry along contexts
> governed
> by rules that are part of inference rules like Modus Ponens.  The
> variables comprising these contexts could be typed or untyped.
>
> 2.  Leave the language, axioms, and rules of first order logic
> unchanged
> from how it's been treated for a great many decades, and instead
> modify
> just the semantics so that there is only one truth value in the
> inconsistent situation where the universe is empty yet there are free
> variables needing values.
>
> I gave pretty complete details of how 2 would work at
> http://boole.stanford.edu/Empty , based on D^V being empty when D is
> empty and V is not, making 2^D^V = 1.
>
> I am willing to believe that 1 can be made to work consistently,
> though
> I would be interested to see the details.
>
> Since logic courses may not want to be forced to modify their
> curriculum
> to introduce contexts, nor to remove them, it would seem beneficial to
> have both the above options, chosen according to the needs of the
> course
> and the preferences of the instructor.
>
>> 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)
>
> This serves as an example of why the rules for option 1 need to be
> spelled out in detail.  If the context is empty, where did a come
> from?
>   And how did it get to be universally quantified?  By making
> generalization mandatory?  Is all this codified in one place, and
> if so
> where?  If the Elephant, then it would be helpful to have an explicit
> list of axioms in one place.  These may exist in the Elephant, but
> they
> seem rather scattered around, making them something of a moving
> target.
>   The rules of the pure untyped predicate calculus are well known,
> they
> were established in the first half of century, and their completeness
> was shown by Goedel.
>
> Vaughan
>
>
> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]



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

Re: Empty algebras

[Andrej Bauer]

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

The discussion is going in circles, it should have occurred over
several rounds of beer. Anyhow, what Steve is pointing out that you
must not forget the typing context, as any categorical logician will
tell you. Let me write

  a:A | .....

to indicate that stuff is hapenning in the context in which a is a
free variable of type A. Then what we have above is the instance of
Modus Ponens rule:

a:A | TRUE(a)                       a:A | TRUE(a) -> exists x:A, TRUE(x)
--------------------------------------------------------------------------------------------------
                       a:A | exists x:A, TRUE(x)

Thus, the conclusion is _not_

   | exists x:A, TRUE(x)

but rather

   a:A | exists x:A, TRUE(x)

and that's an important difference. Out of curiosity I tested Coq to
see what it would do:

-----
Parameter A : Set.
Parameter P : U -> Prop.

Theorem vaughn:
   (forall a : A, P a) -> exists x : A, P x.
Proof.
   firstorder.
-----

Coq answered with the following:

-----
1 subgoal

   H : forall a : A, P a
   ============================
    A
-----

Coq is telling me that in order to finish the proof, I must provide an
element of A. Just as it should. Of course, the same theorem in the
context a : A goes through:

-----
Theorem steve (a : A):
   (forall a : A, P a) -> exists x : A, P x.
Proof.
   firstorder.
Qed.
-----

Now coq says "proof completed".

With kind regards,

Andrej


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

Re: Empty algebras

[Paul Levy]

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

Re: Empty algebras

[Dusko Pavlovic]

no offense, steve, but we are for some reason telling each other things that we both surely know that we both know them.

>  The composite morphism
> 
>   (all) x.P(x) --> P(a) --> (exists) x.P(x)
> 
> exists only when we have a in A.

internally, of course, every A thinks that there is an a in A. that is what its free variable of type A tells it. when A=0, then the predicate P(a), for free a,  as well as the inverse images of (all) x.P(x) and  of (exists) x.P(x) along the map 0-->1, all boil down to the same predicate 0-->Prop. so they turn out to be quite equivalent.  

> 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,

because i thought that some people would remember that it is just the good old Beck-Benabou-Chevalley-Roubaud condition (to list the discoverers alphabetically); whereas the others would be satisfied that quantifying over a variable b, that does not occur in a predicate, does not change the truth value of that predicate.

but i do see what you are saying when we take P:0-->Prop to be a 0-indexed family of propositions, and interpret the quantifiers as the meet and the join: the empty meet is indeed greater than the empty join. so the logicians are eliminating the empty domain in order to avoid having to specify the inverse images. (i think i used to know that.) 

isn't it unreasonable to sacrifice a part of the structure (a fairly ubiquitous object) to a mere syntactic habit? i thought categorical logic had provided a good solution to the "nonempty domain" nuisance from the 50s logic books.

all the best (and i really have to work now),
-- dusko  




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

Re: Empty algebras

[Dusko Pavlovic]

> Even simpler: P(a) --> (exists) x. P(x) is a theorem of the pure
> predicate calculus, which is "clearly" false in the empty universe when
> P is taken to be the identically true predicate.

i assume that even this pure predicate calculus defines its predicates over a set A as the maps
A --> Prop, where Prop is the set truth values. is that right?

then there is just one predicate P:A-->Prop if A=0 (empty). you may call this predicate identically true, or identically false if you like.

do we also agree (with Gentzen) that a sequent 
(exists x). Q(x,y)=>R(y) 
gives a sequent 
Q(x,y)=>R(y)? 
(tacitly, R gets a dummy variable x in this second sequent.)

if we agree with this, then for the predicate P:0-->Prop the identity sequent
(exists) a. P(a) => (exists) x. P(x)
gives the sequent
P(a)=> (exists) x. P(x)

this is not so unintuitive if you realize that (exists) x. P(x) in this sequent must be a predicate over 0, in order to be compared with the truth value of the predicate P(a) over 0. but there is just one predicate over 0, so these two predicates must be equal.

maybe it's time that we all recall lawvere's "Adjunctions in foundations", that appeared some 35 years ago. in its best times, categorical logic offered powerful tools to expand our logical intuitions. 

-- dusko

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