Re: Does equality between sets contradict the philosophy behind structural set theory?

Re: Does equality between sets contradict the philosophy behind structural set theory?

[Fred E.J. Linton]

Leopold Schlicht <schlicht.leopold@gmail.com> quotes, in part:

> Notation 1.1: The arrow notation f : A -> B just means the domain of f is A
> and the codomain of f is B, and we write dom(f) = A and cod(f) = B.

and continues:

> Here, the authors talk about the equality of two sets (dom(f) = A).

No. The symbolatry dom(f) = A is NOT expressing the equality of two
sets, dom(f), and A, it is an abbreviation for the assertion that the map
f has domain A, which is itself a gloss on (a part of) the significance 
we may attach to the arrow notation f: A -> B. The remaining part of that
significance is expressed in the symbolatry cod(f) = B. There again it's
NOT an expression of the equality of two sets, cod(f), and B.

Rather, it's as if we split f: A -> B into two chunks,
f: A -> _  (abbreviated dom(f) = A)
and
f: _ -> B  (abbreviated cod(f) = B).

(In the above, please treat the simple underscore _ as just more white space:
  my usa.net mail service will not permit a string of 3 or 4 space characters
  to pass through without condensing them into a single space character.)

Taking a fresh breath of air, now, and asking about objects of a category:
does one not have a right to suppose that, should you and I each focus our
respective attentions on one object in a category, you on A, say, and I on B,
it should be possible to determine when we have chosen to focus on ONE AND
THE SAME object, i.e., to determine when your A is my B, i.e., when A =  B ?

No question on elementhood or membership enters into that question.

And we NEVER actually say that TWO sets are equal -- only that ONE set is  
equal to itself. If you and I have focused on sets A and B, respectively,
and if it happens that A = B, it means exactly that we were NOT focused
on TWO distinct sets, but only on ONE. 

Cheers, -- Fred Linton





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

Does equality between sets contradict the philosophy behind structural set theory?

[Leopold Schlicht]

Zermelo-Fraenkel set theory (with choice) is commonly accepted as the
standard foundation of mathematics. It is a material set theory. This
means that for every two objects/sets a,b one can ask whether a=b or
not. Also, one can always ask whether "a is an element of b" is true
or not. So "element" is a global element relation.

As an alternative foundation for set theory, Lawvere proposed ETCS (=
elementary theory of the category of sets). It is the standard example
of a structural set theory. The idea behind structural set theory is
that  elements—in contrast to material set theory—have no internal
structure, i.e. are just "abstract dots". Thus there there is no
global element relation, and "objects" are not indepedent things, they
always lie in a particular structure (for example, we cannot speak
about 2 as an object that exists on its own, but we instead talk about
the "2 in the structure IN" or the "2 in the structure IR", and
strictly speaking, these are not the "same" objects, but we have a
natural injection IN -> IR which maps the "natural number 2" to the
"real number 2").

There have been controversial discussion whether ETCS is more
appropriate as a foundation for mathematics than ZFC. I don't want to
discuss this here, but want to point you to this paper:

"Rethinking set theory" by Tom Leinster (it's available at the arxiv)

in which Tom Leinster introduces ETCS and argues that this
foundational system is much nearer to the practice of mathematicians
than ZFC.

Quite at the end of the paper, Leinster states that *Sets for
Mathematics* by Lawvere and Rosebrugh is the quite the only book that
teaches set theory in the flavour of structural set theory
(ETCS)—which makes sense, since Lawvere is the "founder" of structural
set theory.

Now, let me come to my question: Does equality between sets contradict
the philosophy behind structural set theory? Obviously, when doing set
theory in the spirit of structural set theory, we *don't need equality
between sets*. Instead, we talk about isomorphisms, which makes more
sense structurally. Also, the typical definition of equality between
sets (extensionality) can't be formulated in ETCS. Thus it seems to me
that the notion of "equality between sets" doesn't make much sense in
structural set theory. Of course, we could say that two sets are equal
if there is a bijection between them, or state that equality exists
between sets without further specifying what it does (in particular,
if we identify all isomorphic sets, whether there are infinitely many
isomorphic sets that are *not* equal, ...). But this wouldn't yield to
additional value, and is thus superfluous. Having this thoughts in
mind, I was surprised when I read the following in *Sets for
Mathematics*—the standard text book for structural set theory (on page
2!):

> Notation 1.1: The arrow notation f : A -> B just means the domain of f is  A and
the codomain of f is B, and we write dom(f) = A and cod(f) = B.

Here, the authors talk about the equality of two sets (dom(f) = A).
They also use the "big bag of morphisms"-definition of category and
not the "by pairs (A, B) of objects indexed family of hom-sets". But
in this definition, one must talk about operations dom and cod which
specify for each morphism a unique domain and codomain. But the word
"unique" here presupposes that we have a notion of equality between
objects.

Could someone from the categorical foundations of mathematics clarify
my confusion? On the nLab (see nLab page on "category") there are two
definitions of the term "category":
"With one collection of morphisms" and "With a family of collections
of morphisms",
and to me it seems the second ("With a family of collections of
morphisms") is more appropriate for structural set theory. But then,
why do Lawvere—the founder of structural set theory—and Rosebrugh use
the first one ("With one collection of morphisms") in the only book
about structural set theory?


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

Re: Does equality between sets contradict the philosophy behind structural set theory?

[Patrik Eklund]

Leopold Schlicht's question is rightful, and, of course, not new. I
guess there will be at least a few replies to some specifics in
Schlicht's mail, but in this response I will not provide a reply, but
rather, if I may, take the opportunity to add one further remark to my
"Turing Category" note some month ago.

I didn't say anything more deeply about recursion, and neither will I do
now. However, recursion is tricky, as we see in debates about the
Church-Turing thesis. Some "functions" defined e.g. in Turing's proof of
his thesis are dubious since they rely on (and hide the use of) powers.
In an untyped world it's easier to get away doing so, but if we type
things, we cannot avoid the powertype, and then we are required to move
into type constructors, where CS's CT is not very clean. It may support
"practice of typing" (such as in ML/Haskell and differently as in HoTT),
but it lacks proper foundations.

Leinster's paper scratches the surface only, and does not go more deeply
e.g. into quantifiers (as adjoints, as CT would explain them). The
Subset (or Separation, or Comprehension) Axiom, which enforces and
allows the mix of set theory sentences with underlying first-order
sentences, is in Leinster's
paper mentioned just as "is determined by its effect", but not further
developed in CT. Recursion needs this axiom, and recursion in ZFC must
be connected with recursions as appearing in the
Church-Kleene-Post-Turing thesis as well. It isn't, as far (or near) as
I can see, at least not all that well, and it is very unclear to me if
making foundations totally Lawvere will help at all in that respect.

To me, CT is a bridge (between many things, but also) between "the
practice of mathematicians" and the practice of computing and computer
scientists.

If you ask me, as many implicitly point out about those "Paradoxes", we
have allowed impredicativity to slip away, and become a de facto
standard tool for constructing mathematically nice and acceptable
things. The liberal use of equality fuels that impredicativity drive,
that every once in a while makes you find the ball out of bounds.

Best,

Patrik

"hcp=5"



On 2017-02-25 18:23, Leopold Schlicht wrote:
> Zermelo-Fraenkel set theory (with choice) is commonly accepted as the
> standard foundation of mathematics. It is a material set theory. This
> means that for every two objects/sets a,b one can ask whether a=b or
> not. Also, one can always ask whether "a is an element of b" is true
> or not. So "element" is a global element relation.
>
> As an alternative foundation for set theory, Lawvere proposed ETCS (=
> elementary theory of the category of sets). It is the standard example
> of a structural set theory. The idea behind structural set theory is
> that  elements???in contrast to material set theory???have no internal
> structure, i.e. are just "abstract dots". Thus there there is no
> global element relation, and "objects" are not indepedent things, they
> always lie in a particular structure (for example, we cannot speak
> about 2 as an object that exists on its own, but we instead talk about
> the "2 in the structure IN" or the "2 in the structure IR", and
> strictly speaking, these are not the "same" objects, but we have a
> natural injection IN -> IR which maps the "natural number 2" to the
> "real number 2").
>
> There have been controversial discussion whether ETCS is more
> appropriate as a foundation for mathematics than ZFC. I don't want to
> discuss this here, but want to point you to this paper:
>
> "Rethinking set theory" by Tom Leinster (it's available at the arxiv)
>
> in which Tom Leinster introduces ETCS and argues that this
> foundational system is much nearer to the practice of mathematicians
> than ZFC.
>
> Quite at the end of the paper, Leinster states that *Sets for
> Mathematics* by Lawvere and Rosebrugh is the quite the only book that
> teaches set theory in the flavour of structural set theory
> (ETCS)???which makes sense, since Lawvere is the "founder" of structural
> set theory.
>
> Now, let me come to my question: Does equality between sets contradict
> the philosophy behind structural set theory? Obviously, when doing set
> theory in the spirit of structural set theory, we *don't need equality
> between sets*. Instead, we talk about isomorphisms, which makes more
> sense structurally. Also, the typical definition of equality between
> sets (extensionality) can't be formulated in ETCS. Thus it seems to me
> that the notion of "equality between sets" doesn't make much sense in
> structural set theory. Of course, we could say that two sets are equal
> if there is a bijection between them, or state that equality exists
> between sets without further specifying what it does (in particular,
> if we identify all isomorphic sets, whether there are infinitely many
> isomorphic sets that are *not* equal, ...). But this wouldn't yield to
> additional value, and is thus superfluous. Having this thoughts in
> mind, I was surprised when I read the following in *Sets for
> Mathematics*???the standard text book for structural set theory (on page
> 2!):
>
>> Notation 1.1: The arrow notation f : A -> B just means the domain of f
>> is  A and
> the codomain of f is B, and we write dom(f) = A and cod(f) = B.
>
> Here, the authors talk about the equality of two sets (dom(f) = A).
> They also use the "big bag of morphisms"-definition of category and
> not the "by pairs (A, B) of objects indexed family of hom-sets". But
> in this definition, one must talk about operations dom and cod which
> specify for each morphism a unique domain and codomain. But the word
> "unique" here presupposes that we have a notion of equality between
> objects.
>
> Could someone from the categorical foundations of mathematics clarify
> my confusion? On the nLab (see nLab page on "category") there are two
> definitions of the term "category":
> "With one collection of morphisms" and "With a family of collections
> of morphisms",
> and to me it seems the second ("With a family of collections of
> morphisms") is more appropriate for structural set theory. But then,
> why do Lawvere???the founder of structural set theory???and Rosebrugh use
> the first one ("With one collection of morphisms") in the only book
> about structural set theory?

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