Set Theory versus Category Theory versus Type Theory

[Aaron W. Hsu]

Being a relative noob when it comes to all of these things, I was
wondering if anyone had some good thoughts on the relation and relative
merits of these? I have heard some programming languages researchers claim
that set theory is "just bad" or "just wrong" for everything (obviously
they were being partly inflammatory), but it seems that set theory is
widely used throughout domains other than programming languages research.

Why is set theory so pervasive, why not use something like category theory
or type theory? I'm just interested in understanding the relative
differences in all of them. I come from a background in formal
verification in Isabelle and ACL2. In Isabelle there are two common
systems, one is the ZF Set theory and one is the HOL (Higher-order Logic).
It seems that HOL is the more popular for doing proofs about programs in,
which is no surprise, but I would still like to learn more about the
meta-discussion that goes on about these various formal systems if someone
would care to enlighten me.

--
Aaron W. Hsu | arc...@sacrideo.us | http://www.sacrideo.us
Programming is just another word for the Lost Art of Thinking.

[William Elliot]

On Fri, 5 Oct 2012, Aaron W. Hsu wrote:

> I have heard some programming languages researchers claim that set
> theory is "just bad" or "just wrong" for everything (obviously they were
> being partly inflammatory), but it seems that set theory is widely used
> throughout domains other than programming languages research.
>
> Why is set theory so pervasive, why not use something like category
> theory or type theory?

Because it's more intuitive and useful than abstract nonsense, ie
category theory. I've seen relative simple stuff made complicated
by using nonsense theory stuff.

Sometimes generalizations are less useful for being complex, cumbersome
and harder to use.

[JohnF]

Aaron W. Hsu <arc...@sacrideo.us> wrote:
> Being a relative noob when it comes to all of these things, I was
> wondering if anyone had some good thoughts on the relation and relative
> merits of these? I have heard some programming languages researchers claim
> that set theory is "just bad" or "just wrong" for everything (obviously
> they were being partly inflammatory), but it seems that set theory is
> widely used throughout domains other than programming languages research.
>
> Why is set theory so pervasive, why not use something like category theory
> or type theory? I'm just interested in understanding the relative
> differences in all of them. I come from a background in formal
> verification in Isabelle and ACL2. In Isabelle there are two common
> systems, one is the ZF Set theory and one is the HOL (Higher-order Logic).
> It seems that HOL is the more popular for doing proofs about programs in,
> which is no surprise, but I would still like to learn more about the
> meta-discussion that goes on about these various formal systems if someone
> would care to enlighten me.

Enlightment (even self-) is way beyond my abilities.
From a programming language perspective myself, it seems
to me that category theory naturally embodies/expresses
notions like cartesian closed that are very useful but
much harder to express in (naive or not) set theory alone.
On the other hand, lots of (maybe even most?) useful
mathematical notions are completely and straightforwardly
expressible in set theory alone. Perhaps it's like comparing
the rationals versus integers. Many (maybe even most?)
important computer science (and math) ideas and proofs
work perfectly well with N alone.
--
John Forkosh ( mailto: j...@f.com where j=john and f=forkosh )

[Frederick Williams]

"Aaron W. Hsu" wrote:

>
> Why is set theory so pervasive, why not use something like category theory
> or type theory?

It could be a matter of historical accident. Type theory and set theory
both go back to the early years of the 20th century. Russell's type
theory was unusable without the axiom of reducibility which makes the
type distinction irrelevant. Category theory came along later and
(unlike type theory and set theory) was not initially proposed as a
foundation for mathematics.

It's also a matter of habit. If someone is used to set theory and they
are then told about category theory, the first thing they might ask is
'what is the definition of category in terms of sets?' which, where the
category of category is concerned, is a bit of an embarrassment. Mac
Lane has written about this.

Meanwhile, typed lambda calculi have feet in a number of camps.

--
Where are the songs of Summer?--With the sun,
Oping the dusky eyelids of the south,
Till shade and silence waken up as one,
And morning sings with a warm odorous mouth.

[Ross A. Finlayson]

On Oct 6, 7:58 am, Frederick Williams <freddywilli...@btinternet.com>
wrote:

To each their own. Sure, you can write a computer program to
translate classical and set-theoretic proofs to category- and type-
theoretic proofs. And, lambda calculus is for types, so what. It's
great, so what. And those are Russell's ramified and stratified
types. Sure, and type theory as applied, uses the complete finite
determination as for example of enumerated types or sets.

Heh: geometry. Show me pi in category or here probably as easily,
type theory. Or, here, set theory.

Regards,

Ross Finlayson

[Dan Christensen]

On Oct 5, 10:07 pm, "Aaron W. Hsu" <arcf...@sacrideo.us> wrote:
> Being a relative noob when it comes to all of these things, I was
> wondering if anyone had some good thoughts on the relation and relative
> merits of these? I have heard some programming languages researchers claim
> that set theory is "just bad" or "just wrong" for everything (obviously
> they were being partly inflammatory), but it seems that set theory is
> widely used throughout domains other than programming languages research.
>
> Why is set theory so pervasive, why not use something like category theory
> or type theory? I'm just interested in understanding the relative
> differences in all of them. I come from a background in formal
> verification in Isabelle and ACL2. In Isabelle there are two common
> systems, one is the ZF Set theory and one is the HOL (Higher-order Logic).

If they actually have to use the axioms of ZF, I can understand the
reluctance of computer scientists to use it. Has anyone in the field
seriously considered alternative formulations of set theory? (May I
humbly suggest my own simplified set theory, the basis of my DC Proof
program. It's much easier to use and far more intuitive.)

Dan
Download my DC Proof 2.0 software at http://www.dcproof.com

[Frederick Williams]

Dan Christensen wrote:
>
> [...] Has anyone in the field

> seriously considered alternative formulations of set theory?

Yes, see process algebra which uses non-well-founded sets.

[Nam Nguyen]

On 05/10/2012 8:07 PM, Aaron W. Hsu wrote:
> Being a relative noob when it comes to all of these things, I was
> wondering if anyone had some good thoughts on the relation and relative
> merits of these? I have heard some programming languages researchers
> claim that set theory is "just bad" or "just wrong" for everything
> (obviously they were being partly inflammatory), but it seems that set
> theory is widely used throughout domains other than programming
> languages research.
>
> Why is set theory so pervasive, why not use something like category
> theory or type theory? I'm just interested in understanding the relative
> differences in all of them. I come from a background in formal
> verification in Isabelle and ACL2. In Isabelle there are two common
> systems, one is the ZF Set theory and one is the HOL (Higher-order
> Logic). It seems that HOL is the more popular for doing proofs about
> programs in, which is no surprise, but I would still like to learn more
> about the meta-discussion that goes on about these various formal
> systems if someone would care to enlighten me.

On "Why is set theory so pervasive" I'd think that's because the
epsilon-relation symbol 'e' is a binary predicate symbol which
in turn is a language element that is very semantically expressive.

In fact a function could be defined in term of a binary predicate
symbol expression: (xRy) /\ (xRy') -> y=y'.

As such 'e' is still very expressive even if restricted by certain
basic "set" expressions.

The "bad" thing about set, imho, is people tend to quickly jump to the
band wagon that "ordinary" mathematics could be formalized in term
of "set" theory, without realizing one fundamental weakness in term
of language expression of a typical set theory: it has _only ONE_
epsilon-relation!

A "set" theory with multiple epsilon-relations would be richer in
expressing concepts in general, and would be in a better position
to express certain more difficult concepts, in the realm of mathematical
abstractions: such as AI and "consciousness".

And the horizon within which "ordinary" mathematics reside would
be enlarged. Imho.
--
----------------------------------------------------
There is no remainder in the mathematics of infinity.

NYOGEN SENZAKI
----------------------------------------------------

[Nam Nguyen]

Imagine the natural numbers with only addition as a binary operation!

Odds, evens, can we still define. But where are the primes, except for
a finite number of them?

[Dan Christensen]

On Oct 6, 1:52 pm, Frederick Williams <freddywilli...@btinternet.com>
wrote:

> Dan Christensen wrote:
>
> > [...] Has anyone in the field
> > seriously considered alternative formulations of set theory?
>
> Yes, see process algebra which uses non-well-founded sets.
>

Can process algebra be used to model code in a programming language
like C++?

Dan
Download my DC Proof 2.0 at http://www.dcproof.com

[Dan Christensen]

On Oct 6, 2:36 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> On 05/10/2012 8:07 PM, Aaron W. Hsu wrote:
>
>
>
>
>
>
>
>
>
> > Being a relative noob when it comes to all of these things, I was
> > wondering if anyone had some good thoughts on the relation and relative
> > merits of these? I have heard some programming languages researchers
> > claim that set theory is "just bad" or "just wrong" for everything
> > (obviously they were being partly inflammatory), but it seems that set
> > theory is widely used throughout domains other than programming
> > languages research.
>
> > Why is set theory so pervasive, why not use something like category
> > theory or type theory? I'm just interested in understanding the relative
> > differences in all of them. I come from a background in formal
> > verification in Isabelle and ACL2. In Isabelle there are two common
> > systems, one is the ZF Set theory and one is the HOL (Higher-order
> > Logic). It seems that HOL is the more popular for doing proofs about
> > programs in, which is no surprise, but I would still like to learn more
> > about the meta-discussion that goes on about these various formal
> > systems if someone would care to enlighten me.
>
> On "Why is set theory so pervasive" I'd think that's because the
> epsilon-relation symbol 'e' is a binary predicate symbol which
> in turn is a language element that is very semantically expressive.
>
> In fact a function could be defined in term of a binary predicate
> symbol expression: (xRy) /\ (xRy') -> y=y'.
>

This doesn't convey the notion of a mapping from one set to another.
How about:

Ax [x e S -> f(x) e T]

where f is function of one variable mapping set S to set T.

> As such 'e' is still very expressive even if restricted by certain
> basic "set" expressions.
>
> The "bad" thing about set, imho, is people tend to quickly jump to the
> band wagon that "ordinary" mathematics could be formalized in term
> of "set" theory, without realizing one fundamental weakness in term
> of language expression of a typical set theory: it has _only ONE_
> epsilon-relation!
>
> A "set" theory with multiple epsilon-relations would be richer in
> expressing concepts in general, and would be in a better position
> to express certain more difficult concepts, in the realm of mathematical
> abstractions: such as AI and "consciousness".
>

Can you give a simple example of what you mean here?

Dan
Download my DC Proof 2.0 software at http://www.dcproof.com

[Frederick Williams]

Dan Christensen wrote:
>
> On Oct 6, 1:52 pm, Frederick Williams <freddywilli...@btinternet.com>
> wrote:
> > Dan Christensen wrote:
> >
> > > [...] Has anyone in the field
> > > seriously considered alternative formulations of set theory?
> >
> > Yes, see process algebra which uses non-well-founded sets.
> >
>
> Can process algebra be used to model code in a programming language
> like C++?

Process algebras model concurrent systems.

[Nam Nguyen]

Not quite sure if this would contradict my suggestion that the
power of abstraction expression of a binary predicate symbol
is strong, in general.

>
>> As such 'e' is still very expressive even if restricted by certain
>> basic "set" expressions.
>>
>> The "bad" thing about set, imho, is people tend to quickly jump to the
>> band wagon that "ordinary" mathematics could be formalized in term
>> of "set" theory, without realizing one fundamental weakness in term
>> of language expression of a typical set theory: it has _only ONE_
>> epsilon-relation!
>>
>> A "set" theory with multiple epsilon-relations would be richer in
>> expressing concepts in general, and would be in a better position
>> to express certain more difficult concepts, in the realm of mathematical
>> abstractions: such as AI and "consciousness".
>>
>
> Can you give a simple example of what you mean here?

For example in, say ZFC, the canonical semantic of 'e' would
forbid a set s to reflect on itself in term of being a member
of itself (i.e. ~(s e s) is true). But with another epsilon
symbol say "e'", we could have (s e' s), for at least some set s,
to mean s "thinks of itself", where the binary predicate symbol e'
would be interpreted as "think of". (In a nutshell of course).

[Nam Nguyen]

Note that a group has a good degree of "self-reflection" in that
part of it is also a group.

[Dissitra]

Say Nam...get me OUT, huh! 365 christian days and 13 lunar months
burnt as witches and genes 1 in 7 of conception or arranged mariages


shall i save you first, huh !

[Dan Christensen]

On Oct 6, 3:39 pm, Frederick Williams <freddywilli...@btinternet.com>

wrote:
> Dan Christensen wrote:
>
> > On Oct 6, 1:52 pm, Frederick Williams <freddywilli...@btinternet.com>
> > wrote:
> > > Dan Christensen wrote:
>
> > > > [...] Has anyone in the field
> > > > seriously considered alternative formulations of set theory?
>
> > > Yes, see process algebra which uses non-well-founded sets.
>
> > Can process algebra be used to model code in a programming language
> > like C++?
>
> Process algebras model concurrent systems.
>

So, not code in a programming language. Thanks.

Dan
Download my DC Proof 2.0 software at http://www.dcproof.com

[Dan Christensen]

Certainly Ax Ay Ay' (f(x)=y /\ f(x)=y' -> y=y')

by substitution.

> >> As such 'e' is still very expressive even if restricted by certain
> >> basic "set" expressions.
>
> >> The "bad" thing about set, imho, is people tend to quickly jump to the
> >> band wagon that "ordinary" mathematics could be formalized in term
> >> of "set" theory, without realizing one fundamental weakness in term
> >> of language expression of a typical set theory: it has _only ONE_
> >> epsilon-relation!
>
> >> A "set" theory with multiple epsilon-relations would be richer in
> >> expressing concepts in general, and would be in a better position
> >> to express certain more difficult concepts, in the realm of mathematical
> >> abstractions: such as AI and "consciousness".
>
> > Can you give a simple example of what you mean here?
>
> For example in, say ZFC, the canonical semantic of 'e' would
> forbid a set s to reflect on itself in term of being a member
> of itself (i.e. ~(s e s) is true). But with another epsilon
> symbol say "e'", we could have (s e' s), for at least some set s,
> to mean s "thinks of itself", where the binary predicate symbol e'
> would be interpreted as "think of". (In a nutshell of course).
>

Or just dump ZFC in favour of a set theory that does not ban self-
membership. I don't see how the ZF axiom of regularity, the axiom
which effectively bans self-membership, would ever be used in actual
CS applications (or in ordinary mathematics, for that matter).

[Nam Nguyen]

How would "(f(x)" not "convey the notion" of "(xRy) /\ (xRy') -> y=y'"?

>
>>>> As such 'e' is still very expressive even if restricted by certain
>>>> basic "set" expressions.
>>
>>>> The "bad" thing about set, imho, is people tend to quickly jump to the
>>>> band wagon that "ordinary" mathematics could be formalized in term
>>>> of "set" theory, without realizing one fundamental weakness in term
>>>> of language expression of a typical set theory: it has _only ONE_
>>>> epsilon-relation!
>>
>>>> A "set" theory with multiple epsilon-relations would be richer in
>>>> expressing concepts in general, and would be in a better position
>>>> to express certain more difficult concepts, in the realm of mathematical
>>>> abstractions: such as AI and "consciousness".
>>
>>> Can you give a simple example of what you mean here?
>>
>> For example in, say ZFC, the canonical semantic of 'e' would
>> forbid a set s to reflect on itself in term of being a member
>> of itself (i.e. ~(s e s) is true). But with another epsilon
>> symbol say "e'", we could have (s e' s), for at least some set s,
>> to mean s "thinks of itself", where the binary predicate symbol e'
>> would be interpreted as "think of". (In a nutshell of course).
>>
>
> Or just dump ZFC in favour of a set theory that does not ban self-
> membership. I don't see how the ZF axiom of regularity, the axiom
> which effectively bans self-membership, would ever be used in actual
> CS applications (or in ordinary mathematics, for that matter).

But, again, that's just only one example. There's so much one can
convey via the lone epsilon symbol. As alluded to before, think
of the naturals with just only addition as a binary operation.

[Dan Christensen]

That should be

Ax Ay Ay' (x e S /\ y e T /\ y' e T -> (f(x)=y /\ f(x)=y' -> y=y'))

(You really should restrict the domain of each quantifier.)

> > by substitution.
>
> How would "(f(x)" not "convey the notion" of "(xRy) /\ (xRy') -> y=y'"?
>

That's the beauty of this notion. And it's not like f(x) is some
bizarre new notation for the image of x under f.

> >>>> As such 'e' is still very expressive even if restricted by certain
> >>>> basic "set" expressions.
>
> >>>> The "bad" thing about set, imho, is people tend to quickly jump to the
> >>>> band wagon that "ordinary" mathematics could be formalized in term
> >>>> of "set" theory, without realizing one fundamental weakness in term
> >>>> of language expression of a typical set theory: it has _only ONE_
> >>>> epsilon-relation!
>
> >>>> A "set" theory with multiple epsilon-relations would be richer in
> >>>> expressing concepts in general, and would be in a better position
> >>>> to express certain more difficult concepts, in the realm of mathematical
> >>>> abstractions: such as AI and "consciousness".
>
> >>> Can you give a simple example of what you mean here?
>
> >> For example in, say ZFC, the canonical semantic of 'e' would
> >> forbid a set s to reflect on itself in term of being a member
> >> of itself (i.e. ~(s e s) is true). But with another epsilon
> >> symbol say "e'", we could have (s e' s), for at least some set s,
> >> to mean s "thinks of itself", where the binary predicate symbol e'
> >> would be interpreted as "think of". (In a nutshell of course).
>
> > Or just dump ZFC in favour of a set theory that does not ban self-
> > membership. I don't see how the ZF axiom of regularity, the axiom
> > which effectively bans self-membership, would ever be used in actual
> > CS applications (or in ordinary mathematics, for that matter).
>
> But, again, that's just only one example. There's so much one can
> convey via the lone epsilon symbol.

Did you mean, "There's ONLY so much...?"

If so, I suppose you can define any number of axioms and set element
relations, but IMHO more than one seems like an unnecessary
complication. It would have to solve some very important problem that
could not be solved otherwise. I am not aware of any such problems.

[Nam Nguyen]

On 06/10/2012 9:38 PM, Dan Christensen wrote:
> On Oct 6, 6:48 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
>> On 06/10/2012 4:15 PM, Dan Christensen wrote:
>>> On Oct 6, 3:48 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
>>>> On 06/10/2012 1:22 PM, Dan Christensen wrote:
>>
>>>> Not quite sure if this would contradict my suggestion that the
>>>> power of abstraction expression of a binary predicate symbol
>>>> is strong, in general.
>>
>>> Certainly Ax Ay Ay' (f(x)=y /\ f(x)=y' -> y=y')
>>
>
> That should be
>
> Ax Ay Ay' (x e S /\ y e T /\ y' e T -> (f(x)=y /\ f(x)=y' -> y=y'))
>
> (You really should restrict the domain of each quantifier.)
>
>
>>> by substitution.
>>
>> How would "(f(x)" not "convey the notion" of "(xRy) /\ (xRy') -> y=y'"?
>>
>
> That's the beauty of this notion. And it's not like f(x) is some
> bizarre new notation for the image of x under f.

So what's is your definition of "f(x)", in term of the symbol 'e'?

>>>> For example in, say ZFC, the canonical semantic of 'e' would
>>>> forbid a set s to reflect on itself in term of being a member
>>>> of itself (i.e. ~(s e s) is true). But with another epsilon
>>>> symbol say "e'", we could have (s e' s), for at least some set s,
>>>> to mean s "thinks of itself", where the binary predicate symbol e'
>>>> would be interpreted as "think of". (In a nutshell of course).
>>
>>> Or just dump ZFC in favour of a set theory that does not ban self-
>>> membership. I don't see how the ZF axiom of regularity, the axiom
>>> which effectively bans self-membership, would ever be used in actual
>>> CS applications (or in ordinary mathematics, for that matter).
>>
>> But, again, that's just only one example. There's so much one can
>> convey via the lone epsilon symbol.
>
>
> Did you mean, "There's ONLY so much...?"
>
> If so, I suppose you can define any number of axioms and set element
> relations, but IMHO more than one seems like an unnecessary
> complication. It would have to solve some very important problem that
> could not be solved otherwise. I am not aware of any such problems.

I already alluded to it: when you'd need _both_ reflectivity and
non reflexivity for _2 different part-hood concepts_ on an individual
x. What happens when you also need ZFC and don't want to "just dump
ZFC" as you suggest?

Why did you ignore that?

[Dan Christensen]

On Oct 7, 12:01 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> On 06/10/2012 9:38 PM, Dan Christensen wrote:
>
> > On Oct 6, 6:48 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> >> On 06/10/2012 4:15 PM, Dan Christensen wrote:
> >>> On Oct 6, 3:48 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> >>>> On 06/10/2012 1:22 PM, Dan Christensen wrote:
>
> >>>> Not quite sure if this would contradict my suggestion that the
> >>>> power of abstraction expression of a binary predicate symbol
> >>>> is strong, in general.
>
> >>> Certainly Ax Ay Ay' (f(x)=y /\ f(x)=y' -> y=y')
>
> > That should be
>
> > Ax Ay Ay' (x e S /\ y e T /\ y' e T -> (f(x)=y /\ f(x)=y' -> y=y'))
>
> > (You really should restrict the domain of each quantifier.)
>
> >>> by substitution.
>
> >> How would "(f(x)" not "convey the notion" of "(xRy) /\ (xRy') -> y=y'"?
>
> > That's the beauty of this notion. And it's not like f(x) is some
> > bizarre new notation for the image of x under f.
>
> So what's is your definition of "f(x)", in term of the symbol 'e'?
>

Again: Ax (x e S -> f(x) e T)

Informally, as usually interpreted, f(x) is the image of x under f.

> >>>> For example in, say ZFC, the canonical semantic of 'e' would
> >>>> forbid a set s to reflect on itself in term of being a member
> >>>> of itself (i.e. ~(s e s) is true). But with another epsilon
> >>>> symbol say "e'", we could have (s e' s), for at least some set s,
> >>>> to mean s "thinks of itself", where the binary predicate symbol e'
> >>>> would be interpreted as "think of". (In a nutshell of course).
>
> >>> Or just dump ZFC in favour of a set theory that does not ban self-
> >>> membership. I don't see how the ZF axiom of regularity, the axiom
> >>> which effectively bans self-membership, would ever be used in actual
> >>> CS applications (or in ordinary mathematics, for that matter).
>
> >> But, again, that's just only one example. There's so much one can
> >> convey via the lone epsilon symbol.
>
> > Did you mean, "There's ONLY so much...?"
>
> > If so, I suppose you can define any number of axioms and set element
> > relations, but IMHO more than one seems like an unnecessary
> > complication. It would have to solve some very important problem that
> > could not be solved otherwise. I am not aware of any such problems.
>
> I already alluded to it: when you'd need _both_ reflectivity and
> non reflexivity for _2 different part-hood concepts_ on an individual
> x.

And when would that be? Can you give an example?

> What happens when you also need ZFC and don't want to "just dump
> ZFC" as you suggest?
>
> Why did you ignore that?
>

When would you need, say, the ZF axiom of regularity in CS
applications? It's just silly.

[Nam Nguyen]

You already asked; and I already did give an example:

<quote>

to mean s "thinks of itself", where the binary predicate symbol e'
would be interpreted as "think of". (In a nutshell of course).

</quote>

>
>> What happens when you also need ZFC and don't want to "just dump
>> ZFC" as you suggest?
>>
>> Why did you ignore that?
>>
>
> When would you need, say, the ZF axiom of regularity in CS
> applications? It's just silly.

This is sci.logic and I wasn't talking about CS: I was talking about
FOL formal language expression capability.

[Dan Christensen]

This is hardly an example of a serious problem that cannot be solved
without recourse to having multiple kinds of set membership. Remember,
you can postulate any binary relation you want, but it doesn't have to
have anything to do with any kind of set membership.

>
>
> >> What happens when you also need ZFC and don't want to "just dump
> >> ZFC" as you suggest?
>
> >> Why did you ignore that?
>
> > When would you need, say, the ZF axiom of regularity in CS
> > applications? It's just silly.
>
> This is sci.logic and I wasn't talking about CS: I was talking about
> FOL formal language expression capability.
>

The OP seemed to be interested in how set theory is used in formal
verification (of computer-programming code.) It's hard to imagine, but
he said that ZF is actually used in some formal verification packages.
Unless he is talking about a substantially modified form of ZF, IMHO
this can't be a very productive approach.

[Aaron W. Hsu]

On Sun, 07 Oct 2012 13:33:55 -0400, Dan Christensen
<Dan_Chr...@sympatico.ca> wrote:

> The OP seemed to be interested in how set theory is used in formal
> verification (of computer-programming code.) It's hard to imagine, but
> he said that ZF is actually used in some formal verification packages.
> Unless he is talking about a substantially modified form of ZF, IMHO
> this can't be a very productive approach.

Actually, originally, this discussion came up as a general assertion that
set theory was simply the wrong paradigm for any formal reasoning. The
assertion in question goes something like, "trying to do anything in set
theory is simply always the wrong abstraction; category theory is the
right one, or at least intuitionistic type theory." The fact that this
came up in the course of discussion among computer scientists means that
the resulting assertion does not surprise me. However, the claim seemed to
be made going far beyond just the verification of computer programs. The
claim seemed to encompass all formal reasoning.

Where formal verification comes in is that my background in formal
reasoning is largely among using interactive theorem provers to prove
properties about computer programs or recursive structures. This is not to
say that I am only concerned with this domain when talking about the above
assertion. However, the system which I currently use is Isabelle, which
provides two primary theories for use: HOL and ZF. Isabelle targets both
verification of computer software as well as generalized mathematics. It
has been used to do proofs on various "normal" mathematics as well as
computational mathematics.

My main interest is understanding the tradeoffs of set theory versus
something like category theory or type theory, as I have always found set
theory a little easier to think about. Indeed, when I work in HOL, despite
its type system, types to me are just sets, and I chose Isabelle partly
because it had such a relatively weak type system and did not fully
embrace the intuitionist theory of constructive types and all that which
systems like Agda and Coq seem to do. Working in an untyped world has
always been a bit more comfortable for me. However, I am surrounded on all
sides by intuitionist zealots (I jest, in part) who really embrace type
theory or category theory as the solution to all manner of things, to the
point where they really have an abhorrence of set theory. I am trying to
understand why, and why, if their abhorrence is so justified, the rest of
the mathematical community seems to do a great deal of their practical
mathematics using set theory rather than category theory.

--
Aaron W. Hsu | arc...@sacrideo.us | http://www.sacrideo.us
Programming is just another word for the Lost Art of Thinking.

[LudovicoVan]

"Aaron W. Hsu" <arc...@sacrideo.us> wrote in message
news:op.wltrtgig0p3ku8@localhost...
<snipped>

> Working in an untyped world [in Computer Science] has always been a bit

> more comfortable for me. However, I am surrounded on all sides by
> intuitionist zealots (I jest, in part) who really embrace type theory or
> category theory as the solution to all manner of things, to the point
> where they really have an abhorrence of set theory. I am trying to
> understand why, and why, if their abhorrence is so justified, the rest of
> the mathematical community seems to do a great deal of their practical
> mathematics using set theory rather than category theory.

Just a passing remark, that reminds me of `the hype on strongly-typed
languages, aka the OO-uber-alles paradigm.

-LV

[Frederick Williams]

"Aaron W. Hsu" wrote:
>
> On Sun, 07 Oct 2012 13:33:55 -0400, Dan Christensen
> <Dan_Chr...@sympatico.ca> wrote:
>
> > The OP seemed to be interested in how set theory is used in formal
> > verification (of computer-programming code.) It's hard to imagine, but
> > he said that ZF is actually used in some formal verification packages.
> > Unless he is talking about a substantially modified form of ZF, IMHO
> > this can't be a very productive approach.
>
> Actually, originally, this discussion came up as a general assertion that
> set theory was simply the wrong paradigm for any formal reasoning.

I should warn you that Dan Christensen, Nam Nguyen, Ludovico Van and
Ross A. Finlayson are all ignorant of logic. The are so ignorant, they
don't know how ignorant they are; and they are unwilling to learn.

[LudovicoVan]

"Frederick Williams" <freddyw...@btinternet.com> wrote in message
news:5071F928...@btinternet.com...

> "Aaron W. Hsu" wrote:
>> On Sun, 07 Oct 2012 13:33:55 -0400, Dan Christensen
>> <Dan_Chr...@sympatico.ca> wrote:
>>
>> > The OP seemed to be interested in how set theory is used in formal
>> > verification (of computer-programming code.) It's hard to imagine, but
>> > he said that ZF is actually used in some formal verification packages.
>> > Unless he is talking about a substantially modified form of ZF, IMHO
>> > this can't be a very productive approach.
>>
>> Actually, originally, this discussion came up as a general assertion that
>> set theory was simply the wrong paradigm for any formal reasoning.
>
> I should warn you that Dan Christensen, Nam Nguyen, Ludovico Van and
> Ross A. Finlayson are all ignorant of logic. The are so ignorant, they
> don't know how ignorant they are; and they are unwilling to learn.

Thanks, Frederick, for warning our guest. As far as I am concerned, I take
it you are talking about mathematical logic specifically: in fact, here is a
distinction that is not popular in sci.logic.

-LV

[Aaron W. Hsu]

On Sun, 07 Oct 2012 17:50:32 -0400, Frederick Williams
<freddyw...@btinternet.com> wrote:

> "Aaron W. Hsu" wrote:
>>
>> On Sun, 07 Oct 2012 13:33:55 -0400, Dan Christensen
>> <Dan_Chr...@sympatico.ca> wrote:
>>
>> > The OP seemed to be interested in how set theory is used in formal
>> > verification (of computer-programming code.) It's hard to imagine, but
>> > he said that ZF is actually used in some formal verification packages.
>> > Unless he is talking about a substantially modified form of ZF, IMHO
>> > this can't be a very productive approach.
>>
>> Actually, originally, this discussion came up as a general assertion
>> that
>> set theory was simply the wrong paradigm for any formal reasoning.
>
> I should warn you that Dan Christensen, Nam Nguyen, Ludovico Van and
> Ross A. Finlayson are all ignorant of logic. The are so ignorant, they
> don't know how ignorant they are; and they are unwilling to learn.

The very idea of taking any random Internet poster as having authoritative
information without real world references or having a corresponding CV
that demonstrates their good track record seems like a crazy idea, so, no
worries. :-) Then again, this applies equally well to you and me, as well.

[Nam Nguyen]

Very well said. :-)

[Nam Nguyen]

On 07/10/2012 2:13 PM, Aaron W. Hsu wrote:
> On Sun, 07 Oct 2012 13:33:55 -0400, Dan Christensen
> <Dan_Chr...@sympatico.ca> wrote:
>
>> The OP seemed to be interested in how set theory is used in formal
>> verification (of computer-programming code.) It's hard to imagine, but
>> he said that ZF is actually used in some formal verification packages.
>> Unless he is talking about a substantially modified form of ZF, IMHO
>> this can't be a very productive approach.
>
> Actually, originally, this discussion came up as a general assertion
> that set theory was simply the wrong paradigm for any formal reasoning.

This would somewhat contradict to the general belief that most important
mathematics (the natural numbers, real continuity, topological spaces
[Hausdorff for instance] , etc...) can be formalized in say ZFC.

> The assertion in question goes something like, "trying to do anything in
> set theory is simply always the wrong abstraction; category theory is
> the right one, or at least intuitionistic type theory." The fact that
> this came up in the course of discussion among computer scientists means
> that the resulting assertion does not surprise me. However, the claim
> seemed to be made going far beyond just the verification of computer
> programs.

> The claim seemed to encompass all formal reasoning.

I'm wondering though how much of "formal reasoning" would those CS's
would really care? Or even really realize?

>
> Where formal verification comes in is that my background in formal
> reasoning is largely among using interactive theorem provers to prove
> properties about computer programs or recursive structures. This is not
> to say that I am only concerned with this domain when talking about the
> above assertion. However, the system which I currently use is Isabelle,
> which provides two primary theories for use: HOL and ZF. Isabelle
> targets both verification of computer software as well as generalized
> mathematics. It has been used to do proofs on various "normal"
> mathematics as well as computational mathematics.
>
> My main interest is understanding the tradeoffs of set theory versus
> something like category theory or type theory, as I have always found
> set theory a little easier to think about.

I'd think so too. But there's a not-so-great side of set theory,
even in practicality.

For example, one wouldn't have a problem to undersealed a definition of
say "string" [finite, left to right], but it's so unpleasant to note
that for a string s, we would also have look-alike-strings: {s}, {{s}},
etc... At certain point in a formalization, these look-alike-strings
might impact on our intention to formalize our theory about "strings".

Sorry I have to go now but at next chance I'd present a similar
situation: instead of "string" formalization, it would be "elementary
particle", "atom", "molecule" formalizations. There, we'd judge for
ourselves how good, cumbersome (or even "abhorrent") an 1-epsilon
symbol set theory such as ZFC might be.

> Indeed, when I work in HOL,
> despite its type system, types to me are just sets, and I chose Isabelle
> partly because it had such a relatively weak type system and did not
> fully embrace the intuitionist theory of constructive types and all that
> which systems like Agda and Coq seem to do. Working in an untyped world
> has always been a bit more comfortable for me. However, I am surrounded
> on all sides by intuitionist zealots (I jest, in part) who really
> embrace type theory or category theory as the solution to all manner of
> things, to the point where they really have an abhorrence of set theory.
> I am trying to understand why, and why, if their abhorrence is so
> justified, the rest of the mathematical community seems to do a great
> deal of their practical mathematics using set theory rather than
> category theory.


--

[Nam Nguyen]

"... wouldn't have a problem to understand a definition ..." I meant
(Sorry)

[Aaron W. Hsu]

On Sun, 07 Oct 2012 19:55:01 -0400, Nam Nguyen <namduc...@shaw.ca>
wrote:

> This would somewhat contradict to the general belief that most important
> mathematics (the natural numbers, real continuity, topological spaces
> [Hausdorff for instance] , etc...) can be formalized in say ZFC.

The claim had nothing to do with the power of ZFC, which they were willing
to acknowledge. It was whether or not expressing concepts in something
like ZFC (and, I suspect, any classical system) was worthwhile, rather
than being unnecessarily complex, unintuitive, and cumbersome, as opposed
to using category theory or type theory.

[Aaron W. Hsu]

On Sun, 07 Oct 2012 19:55:01 -0400, Nam Nguyen <namduc...@shaw.ca>
wrote:

> For example, one wouldn't have a problem to undersealed a definition of
> say "string" [finite, left to right], but it's so unpleasant to note
> that for a string s, we would also have look-alike-strings: {s}, {{s}},
> etc... At certain point in a formalization, these look-alike-strings
> might impact on our intention to formalize our theory about "strings".

Wouldn't you normally formalize the concept of a sequence first, with a
definition of equality and so forth, and only then formalize the concept
of a "string" on top of that as being a sequence of elements whose
elements are members of the set of characters considered valid for that
string? I would imagine then that this would isolate the issue of similar
strings behind the concept of a sequence. Or, wait, were you talking about
strings as sequences? I've always thought of sequences as nothing more
than ordered sets that may contain repeated elements, and then thought of
strings as sequences whose elements are all of a particular, finite
domain, usually with the assumption that members of that domain are only
to be dealt with as atomic entities, not to be decomposed; that is, you
wouldn't have strings of characters where the characters themselves might
be sets of characters, though, you might, for instance, represent
characters as code-points if you were in unicode, in which case you would
have some way of determining whether two characters were equal, even if
they were composed of different code-points. This sort of thing does come
up in practical CS applications and language specifications.

[Frederick Williams]

"Aaron W. Hsu" wrote:
>
> On Sun, 07 Oct 2012 17:50:32 -0400, Frederick Williams
> <freddyw...@btinternet.com> wrote:
>
> > "Aaron W. Hsu" wrote:
> >>
> >> On Sun, 07 Oct 2012 13:33:55 -0400, Dan Christensen
> >> <Dan_Chr...@sympatico.ca> wrote:
> >>
> >> > The OP seemed to be interested in how set theory is used in formal
> >> > verification (of computer-programming code.) It's hard to imagine, but
> >> > he said that ZF is actually used in some formal verification packages.
> >> > Unless he is talking about a substantially modified form of ZF, IMHO
> >> > this can't be a very productive approach.
> >>
> >> Actually, originally, this discussion came up as a general assertion
> >> that
> >> set theory was simply the wrong paradigm for any formal reasoning.
> >
> > I should warn you that Dan Christensen, Nam Nguyen, Ludovico Van and
> > Ross A. Finlayson are all ignorant of logic. The are so ignorant, they
> > don't know how ignorant they are; and they are unwilling to learn.
>
> The very idea of taking any random Internet poster as having authoritative
> information without real world references or having a corresponding CV
> that demonstrates their good track record seems like a crazy idea, so, no
> worries. :-) Then again, this applies equally well to you and me, as well.

Oh indeed yes, I nothing about logic and yet I still manage to know more
than those I named.

[Frederick Williams]

Frederick Williams wrote:

>
> Oh indeed yes, I nothing about logic and yet I still manage to know more
> than those I named.

Silly me, I meant to write 'I know nothing...' Sorry.

[Frederick Williams]

Nam Nguyen wrote:
>
> On 07/10/2012 4:36 PM, Aaron W. Hsu wrote:

> >
> > The very idea of taking any random Internet poster as having
> > authoritative information without real world references or having a
> > corresponding CV that demonstrates their good track record seems like a
> > crazy idea, so, no worries. :-) Then again, this applies equally well to
> > you and me, as well.
>
> Very well said. :-)

I await with interest your real world references or CV that demonstrates
your good track record.

[Nam Nguyen]

My issue isn't with the definition of "string" as a set, which
of course in ZFC for instance everything is a set.

It's the issue that however the definition for a "string" is, {s}
is usually isn't a string by the definition, which depending
on some application of abstraction might not make much sense.

For example, given 2 string s and s' the ordered pair of these
2 strings would be:

(*) {{s}, {s,s'}}

so technically the following wouldn't be an ordered pair of s, s':

(*) {{{s}}, {{s},{{{{{s'}}}}}}}

but from an abstraction point of view it doesn't make much sense
to consider (*) as an ordered pair while not (**). And in some
application of set theory, this can cause problems in expressing
the underlying concepts through the language of the set theory
in question.

[MoeBlee]

On Oct 9, 10:21 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:

> It's the issue that however the definition for a "string" is, {s}
> is usually isn't a string by the definition, which depending
> on some application of abstraction might not make much sense.

We may stipulate that a 'string' means 'finite sequence'. Also, we may
stipuate that with formal languages, no symbol is a string of other
symbols. Thus a string of symbols is such that no symbol in the string
is itself a string of other symbols.

What, if anything, do you think wouldn't make sense with that?

> For example, given 2 string s and s' the ordered pair of these
> 2 strings would be:
>
> (*) {{s}, {s,s'}}
>
> so technically the following wouldn't be an ordered pair of s, s':
>
> (*) {{{s}}, {{s},{{{{{s'}}}}}}}

I think you mean:

(**) {{{s}}, {{s},{{{{{s'}}}}}}}

> but from an abstraction point of view it doesn't make much sense
> to consider (*) as an ordered pair while not (**).

{{{s}}, {{s},{{{{{s'}}}}}}}

is an ordered pair?

It's not the ordered pair of s and s', i.e., <s s'>, i.e. {{s} {s
s'}}, but it's still an ordered pair.

I don't see what problem you find with this regarding strings.

MoeBlee

[MoeBlee]

Nam Nguyen: There haven't been any objections to my post below. Should
I take it that my post clears up the matter of symbols and strings for
you?

[Nam Nguyen]

On 16/10/2012 3:16 PM, MoeBlee wrote:
> Nam Nguyen: There haven't been any objections to my post below. Should
> I take it that my post clears up the matter of symbols and strings for
> you?

There had been nothing to be cleared up by anybody, in my explanation
of the string viz-a-viz _one_ epsilon predicate symbol.

>
> On Oct 10, 12:49 pm, MoeBlee <modem...@gmail.com> wrote:
>> On Oct 9, 10:21 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
>>
>>> It's the issue that however the definition for a "string" is, {s}
>>> is usually isn't a string by the definition, which depending
>>> on some application of abstraction might not make much sense.
>>
>> We may stipulate that a 'string' means 'finite sequence'. Also, we may
>> stipuate that with formal languages, no symbol is a string of other
>> symbols. Thus a string of symbols is such that no symbol in the string
>> is itself a string of other symbols.
>>
>> What, if anything, do you think wouldn't make sense with that?
>>
>>> For example, given 2 string s and s' the ordered pair of these
>>> 2 strings would be:
>>
>>> (*) {{s}, {s,s'}}
>>
>>> so technically the following wouldn't be an ordered pair of s, s':
>>
>>> (*) {{{s}}, {{s},{{{{{s'}}}}}}}
>>
>> I think you mean:
>>
>> (**) {{{s}}, {{s},{{{{{s'}}}}}}}
>>
>>> but from an abstraction point of view it doesn't make much sense
>>> to consider (*) as an ordered pair while not (**).
>>
>> {{{s}}, {{s},{{{{{s'}}}}}}}
>>
>> is an ordered pair?
>>
>> It's not the ordered pair of s and s', i.e., <s s'>, i.e. {{s} {s
>> s'}}, but it's still an ordered pair.
>>
>> I don't see what problem you find with this regarding strings.

As I had explained, the problem is that the _one_ epsilon predicate
symbol is so generic a binary predicate that it`d cause problems
in applying its interpretation to certain specific cases.

For instance, if you have 2 characters a and b as sets, then
you could define the string 'ab' as the following ordered pair:

>>> (*) {{a}, {a,b}}

However, that doesn't mean the the following can't be an equivalent
definition of the string 'ab':

>> (**) {{{a}}, {{a},{{{{{b}}}}}}}

The fact that within the same set context with _one_ epsilon symbol
one could interpret a concept (e.g. "string") in more than one way
would be problematic in some applications.

That's what I had conveyed.

[Frederick Williams]

Nam Nguyen wrote:

>
> As I had explained, the problem is that the _one_ epsilon predicate
> symbol is so generic a binary predicate that it`d cause problems
> in applying its interpretation to certain specific cases.
>
> For instance, if you have 2 characters a and b as sets, then
> you could define the string 'ab' as the following ordered pair:
>
> >>> (*) {{a}, {a,b}}
>
> However, that doesn't mean the the following can't be an equivalent
> definition of the string 'ab':
>
> >> (**) {{{a}}, {{a},{{{{{b}}}}}}}
>
> The fact that within the same set context with _one_ epsilon symbol
> one could interpret a concept (e.g. "string") in more than one way
> would be problematic in some applications.

In what applications? In a usual set theory, with just '=' and 'in' as
its extralogical symbols, one could define the string ab to be either
{{a}, {a,b}} or one could define it to be {{{a}}, {{a},{{{{{b}}}}}}}.
(Surely one wouldn't define it to be both; in any theory to define the
same thing in two different ways would be perverse.) There is no need
for the usual 'in' and some further 'in' to handle the (**) definition.

Also, in what sense is (**) an equivalent definition to (*). Since

{{a}, {a,b}} =/= {{{a}}, {{a},{{{{{b}}}}}}}

'equivalent' would seem to be the wrong word. The inequality holds in
the usual set theories, and I don't deny that in some set theory {x} may
= x for some x. Do you have in mind such a set theory?

[MoeBlee]

On Oct 16, 9:57 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:

> you could define the string 'ab' as the following ordered pair:
>
> >>> (*) {{a}, {a,b}}
>
> However, that doesn't mean the the following can't be an equivalent
> definition of the string 'ab':
>
> >> (**) {{{a}}, {{a},{{{{{b}}}}}}}

They're not equivalent definitions, since (*) is not (**).

Equivalent definitions D1 and D2 are ones in which, for a predicate we
have "definiens of D1 iff definiens of D2", and for a function we have
"definiens of D1 = definiens of D2".

But, yes, of course, any author is free to make his own stipulative
definitions. So what?

Indeed, you're free to stipulate that by 'dog' you mean a typewriter.

MoeBlee

[Nam Nguyen]

On 17/10/2012 10:03 AM, MoeBlee wrote:
> On Oct 16, 9:57 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
>
>> you could define the string 'ab' as the following ordered pair:
>>
>>>>> (*) {{a}, {a,b}}
>>
>> However, that doesn't mean the the following can't be an equivalent
>> definition of the string 'ab':
>>
>>>> (**) {{{a}}, {{a},{{{{{b}}}}}}}
>
> They're not equivalent definitions, since (*) is not (**).

You misunderstood what I said. I didn't say (*) <-> (**) is a tautology.
I only said both definitions could equally, equivalently, express the
concept-definition of a string. Note earlier I had said:

>> For example, one wouldn't have a problem to understand a definition

>> of say "string" [finite, left to right],


>

> Equivalent definitions D1 and D2 are ones in which, for a predicate we
> have "definiens of D1 iff definiens of D2", and for a function we have
> "definiens of D1 = definiens of D2".
>
> But, yes, of course, any author is free to make his own stipulative
> definitions. So what?
>
> Indeed, you're free to stipulate that by 'dog' you mean a typewriter.

Indeed, the realm of mathematical abstraction is vast - infinite - and
if one limits one's own imagination to only dog-to-typewriter kinds
of examples then of course dog-to-typewriter illustrations one could
only see.

On the other hand, I did have some examples to illustrate the problem
of defining strings using only one epsilon symbol, using say a
generalized Kuratowski's string definition:

(a,b) <-> {{a}, {a,b}}
(a1, a2, ..., an-1, an) <-> (an-1,an).

Now, given a 2-dimensional infinite grid of squares (a la John Conway)
each of which has a finite range of states. We could define a string
worm life form as a series of finite consecutive square of a certain
states.

So, without loss of generality, a (worm) string of length n would be:

s1s2s3....sn-1sn

But then, using the generalized Kuratowski's definition above,
would the _sub-string_ s1s2 be expressed in the same way as
say the _sub-string_ sn-1sn?

Would a sub-string be of the same concept as that of a string,
under Kuratowski's definition?

Apparently not. So, there is the problem that you and Frederick
have missed.

[Frederick Williams]

Above, what does <-> mean? I'm used to it meaning the material
biconditional.

[MoeBlee]

On Oct 17, 9:49 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> On 17/10/2012 10:03 AM, MoeBlee wrote:
>
> > On Oct 16, 9:57 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
>
> >> you could define the string 'ab' as the following ordered pair:
>
> >>>>> (*) {{a}, {a,b}}
>
> >> However, that doesn't mean the the following can't be an equivalent
> >> definition of the string 'ab':
>
> >>>> (**) {{{a}}, {{a},{{{{{b}}}}}}}
>
> > They're not equivalent definitions, since (*) is not (**).
>
> You misunderstood what I said. I didn't say (*) <-> (**) is a tautology.

No, I did not misunderstand what you said. I did not say that you
claimed "(*) <-> (**)" is a tautology.

> I only said both definitions could equally, equivalently, express the
> concept-definition of a string.

You said, "that doesn't mean the the following can't be an equivalent
definition of the string 'ab': [...]"

And I replied that they're not equivalent definitions.

You're welcome to say now that what you meant is something else, but I
responded to what you actually said.

> > Equivalent definitions D1 and D2 are ones in which, for a predicate we
> > have "definiens of D1 iff definiens of D2", and for a function we have
> > "definiens of D1 = definiens of D2".
>
> > But, yes, of course, any author is free to make his own stipulative
> > definitions. So what?
>
> > Indeed, you're free to stipulate that by 'dog' you mean a typewriter.
>
> Indeed, the realm of mathematical abstraction is vast - infinite - and
> if one limits one's own imagination to only dog-to-typewriter kinds
> of examples then of course dog-to-typewriter illustrations one could
> only see.

I don't "only" see such examples. Indeed, I mentioned that example in
analogy with YOUR example.

> On the other hand, I did have some examples to illustrate the problem
> of defining strings using only one epsilon symbol, using say a
> generalized Kuratowski's string definition:
>
> (a,b) <-> {{a}, {a,b}}

> (a1, a2, ..., an-1, an) <-> (an-1,an).

In both instances, you have two terms with a biconditional between
them. I don't know what that means.

Moreover, even if you mean "=" instead of "<->" there, the second
instance is not the ordinary generalization of the Kuratowski
definition. Instead, it is:

<a1 a2 ... an-1 an> = <<a1 a2 ... an-1> an>

And again, I completely agree that one can stipulate alternative
defintions of mathematical terminology and notation, just as one can
stipulate that by 'dog' one means typewriter. Yes, if two people use
different defintions, then they may get different results. I don't see
any point you've made beyond that obvious fact.

MoeBlee

[Frederick Williams]

Nam Nguyen wrote:
>
> [...] using say a

> generalized Kuratowski's string definition:
>
> (a,b) <-> {{a}, {a,b}}

That's ok if we read '<->' as 'is defined to be'. (Which is
nonstandard, but never mind.)

> (a1, a2, ..., an-1, an) <-> (an-1,an).

But we can hardly read that as meaning (a1, a2, ..., an-1, an) is
defined to be (an-1,an). If that were so (1,2,3,4) and (5,6,3,4) would
both be defined to be (3,4).

You can define (a,b,c) as ((a,b),c) or as (a,(b,c)). I've seen both.
And similarly with quadruples, etc. Or you can define n-tuples as
functions on {1,2,...,n} (or on {0,2,...,n-1}) with the appropriate
codomain.

[Nam Nguyen]

On 18/10/2012 12:59 PM, Frederick Williams wrote:
> Nam Nguyen wrote:
>>
>> [...] using say a
>> generalized Kuratowski's string definition:
>>
>> (a,b) <-> {{a}, {a,b}}
>
> That's ok if we read '<->' as 'is defined to be'. (Which is
> nonstandard, but never mind.)

Yes: for clarity, it should have been the notation "df=" here.

>
>> (a1, a2, ..., an-1, an) <-> (an-1,an).
>
> But we can hardly read that as meaning (a1, a2, ..., an-1, an) is
> defined to be (an-1,an). If that were so (1,2,3,4) and (5,6,3,4) would
> both be defined to be (3,4).

It was a typo on my part. It should have been (as you alluded to below):

(a1, a2, ..., an-1, an) df= ((a1,...,an-1),an)

>
> You can define (a,b,c) as ((a,b),c) or as (a,(b,c)). I've seen both.
> And similarly with quadruples, etc.

Now that it seems clear on the definition, would you see my point about
the problem of there being only 1 epsilon symbol, viz-a-viz the concept
of "sub-string", in relation to that of "string"?

[Nam Nguyen]

On 18/10/2012 9:24 AM, MoeBlee wrote:
> On Oct 17, 9:49 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:

>
>> On the other hand, I did have some examples to illustrate the problem
>> of defining strings using only one epsilon symbol, using say a
>> generalized Kuratowski's string definition:
>>
>> (a,b) <-> {{a}, {a,b}}
>
>> (a1, a2, ..., an-1, an) <-> (an-1,an).
>
> In both instances, you have two terms with a biconditional between
> them. I don't know what that means.

As I've just mentioned to Frederick, it was meant to be "df=";
and ...

>
> Moreover, even if you mean "=" instead of "<->" there, the second
> instance is not the ordinary generalization of the Kuratowski
> definition. Instead, it is:
>
> <a1 a2 ... an-1 an> = <<a1 a2 ... an-1> an>

it was a typo in my previous posts: your above is what I really meant.

>
> And again, I completely agree that one can stipulate alternative
> defintions of mathematical terminology and notation, just as one can
> stipulate that by 'dog' one means typewriter. Yes, if two people use
> different defintions, then they may get different results. I don't see
> any point you've made beyond that obvious fact.

With the definitions clarified, you'd see that the problem is about
"sub-string" vs. "string", not "dog" and "typewriter" as you might
have "feared". Would you not?

In summary, hope that you now would understand the point I made to
the op that there being only 1 epsilon (binary) relation symbol would
be a weakness in some applications of (typical) set-theories.

[MoeBlee]

On Oct 18, 9:19 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> hope that you now would understand the point I made to
> the op that there being only 1 epsilon (binary) relation symbol would
> be a weakness in some applications of (typical) set-theories.

Sorry, I don't.

MoeBlee

[Frederick Williams]

Nam Nguyen wrote:

> Now that it seems clear on the definition, would you see my point about
> the problem of there being only 1 epsilon symbol, viz-a-viz the concept
> of "sub-string", in relation to that of "string"?

Strings and their substrings can be discussed without the need for set
theory, for example as in generative grammar. Or as in the theory of
free monoids. It would seem to me that the symbol epsilon is
irrelevant.

[Nam Nguyen]

What didn't you understand?

- You were unable to understand the concept of "string" (finite,
adjacent, 1 direction)?

- You were unable to understand the concept of "sub-string" which
is also a string?

- You were unable to express "strings" in L(ZF)?

What specifically prevented you from understanding what seems
to be a simple point, problem?

[Nam Nguyen]

On 19/10/2012 12:18 PM, Frederick Williams wrote:
> Nam Nguyen wrote:
>
>> Now that it seems clear on the definition, would you see my point about
>> the problem of there being only 1 epsilon symbol, viz-a-viz the concept
>> of "sub-string", in relation to that of "string"?
>
> Strings and their substrings can be discussed without the need for set
> theory, for example as in generative grammar. Or as in the theory of
> free monoids.


> It would seem to me that the symbol epsilon is irrelevant.

You just forgot the op, I and others, were talking about "Why is
set theory so pervasive"!

So the weakness, the problem, of there being 1-epsilon symbol is
very much part of what we're talking about.

In fact the op did clarify:

> Actually, originally, this discussion came up as a general assertion
> that set theory was simply the wrong paradigm for any formal
> reasoning.

Note his "set theory was simply the wrong paradigm for any formal
reasoning", which seems to be in tuned with my presented example
of "string"/"sub-string problem.

[At least you seemed to understand the problem I raised. (The other
poster, MoeBlee, didn't seem to understand).]

[Frederick Williams]

Nam Nguyen wrote:
>
> On 19/10/2012 12:18 PM, Frederick Williams wrote:
> > Nam Nguyen wrote:
> >
> >> Now that it seems clear on the definition, would you see my point about
> >> the problem of there being only 1 epsilon symbol, viz-a-viz the concept
> >> of "sub-string", in relation to that of "string"?
> >
> > Strings and their substrings can be discussed without the need for set
> > theory, for example as in generative grammar. Or as in the theory of
> > free monoids.
>
> > It would seem to me that the symbol epsilon is irrelevant.
>
> You just forgot the op, I and others, were talking about "Why is
> set theory so pervasive"!

The answer is because mathematics can be formalized in it, and its
intuitive meaning is clear.

> So the weakness, the problem, of there being 1-epsilon symbol is
> very much part of what we're talking about.
>
> In fact the op did clarify:
>
> > Actually, originally, this discussion came up as a general assertion
> > that set theory was simply the wrong paradigm for any formal
> > reasoning.
>
> Note his "set theory was simply the wrong paradigm for any formal
> reasoning", which seems to be in tuned with my presented example
> of "string"/"sub-string problem.

I saw no problem.

[Nam Nguyen]

On 20/10/2012 8:13 AM, Frederick Williams wrote:
> Nam Nguyen wrote:
>>
>> On 19/10/2012 12:18 PM, Frederick Williams wrote:
>>> Nam Nguyen wrote:
>>>
>>>> Now that it seems clear on the definition, would you see my point about
>>>> the problem of there being only 1 epsilon symbol, viz-a-viz the concept
>>>> of "sub-string", in relation to that of "string"?
>>>
>>> Strings and their substrings can be discussed without the need for set
>>> theory, for example as in generative grammar. Or as in the theory of
>>> free monoids.
>>
>>> It would seem to me that the symbol epsilon is irrelevant.
>>
>> You just forgot the op, I and others, were talking about "Why is
>> set theory so pervasive"!
>
> The answer is because mathematics can be formalized in it, and its
> intuitive meaning is clear.

OK. Let's evaluate your assessment, below ...

>
>> So the weakness, the problem, of there being 1-epsilon symbol is
>> very much part of what we're talking about.
>>
>> In fact the op did clarify:
>>
>> > Actually, originally, this discussion came up as a general assertion
>> > that set theory was simply the wrong paradigm for any formal
>> > reasoning.
>>
>> Note his "set theory was simply the wrong paradigm for any formal
>> reasoning", which seems to be in tuned with my presented example
>> of "string"/"sub-string problem.
>
> I saw no problem.

So, why don't you, using _the lone_ epsilon relation symbol 'e' express
a sub-string s' of a general string s and s' is a string as s is.

Until you could express so, there seems to be a problem you'd be unable
to see.

[Frederick Williams]

Nam Nguyen wrote:

>
> So, why don't you, using _the lone_ epsilon relation symbol 'e' express
> a sub-string s' of a general string s and s' is a string as s is.
>
> Until you could express so, there seems to be a problem you'd be unable
> to see.

Let S be a non-empty sets. Its elements are the symbols of which the
strings will be constructed. It matters not whether the elements of S
are sets or urelemente, but I'll take them to be sets. Let M be some
non-empty finite set of natural numbers. An M-string over S is either
the empty set or a function

f:M -> S.

The empty set is call the null string. If K is a subset of M, then a
K-string is called a substring of an M-string.

A string is just a J-string for some suitable choice of J, a non-empty
finite set of natural numbers.

All of the above can be expressed in the language of (say) ZF.

[My first thought was that M should be {0,1,...,n} for some natural
number n, but then a substring that was not an initial substring would
not be a string. Hence the use of a more general M. Note that a string
in my sense can always be "re-domained" so that it is a "my first
thought string". So strings as I've defined them (as M-strings for
suitable M) are isomorphic to my first thought strings (those being as
finite sequences in (say) ZF are usually defined). Others can express
this better than I can.]

[Frederick Williams]

Frederick Williams wrote:
>
> Nam Nguyen wrote:
>
> >
> > So, why don't you, using _the lone_ epsilon relation symbol 'e' express
> > a sub-string s' of a general string s and s' is a string as s is.
> >
> > Until you could express so, there seems to be a problem you'd be unable
> > to see.
>
> Let S be a non-empty sets.

'set' not 'sets'.

> Its elements are the symbols of which the
> strings will be constructed. It matters not whether the elements of S
> are sets or urelemente, but I'll take them to be sets. Let M be some
> non-empty finite set of natural numbers. An M-string over S is either
> the empty set or a function
>
> f:M -> S.
>
> The empty set is call the null string. If K is a subset of M, then a
> K-string is called a substring of an M-string.

That will define substring in a broader sense that usual. Never mind.

[MoeBlee]

On Oct 19, 6:55 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> On 19/10/2012 9:05 AM, MoeBlee wrote:
>
> > On Oct 18, 9:19 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> >> hope that you now would understand the point I made to
> >> the op that there being only 1 epsilon (binary) relation symbol would
> >> be a weakness in some applications of (typical) set-theories.
>
> > Sorry, I don't.
>
> What didn't you understand?
>
> - You were unable  to  understand the concept of "string" (finite,
>    adjacent, 1 direction)?

> - You were unable to understand the concept of "sub-string" which
>    is also a string?
>
> - You were unable to express "strings" in L(ZF)?

I understand the notions of string and substrings and as expressed in
set theory.

> What specifically prevented you from understanding what seems
> to be a simple point, problem?

I take it that your point is in this challenge?:

"using _the lone_ epsilon relation symbol 'e' express
a sub-string s' of a general string s and s' is a string as s is."

I don't see a problem here since I take 'string' and 'substring' in
the sense of sequence and subsequence, which are rigorously defined
in, for example, set theory. But if you challenge me to produce the
definitions, my question to you would be: Are you asking me from real
curiosity as you REALLY are not familiar with such definitions or are
you asking me just to have me prove that I myself know them?

MoeBlee

[MoeBlee]

On Oct 22, 12:08 pm, MoeBlee <modem...@gmail.com> wrote:
> On Oct 19, 6:55 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:

> > On 19/10/2012 9:05 AM, MoeBlee wrote:
>
> > > On Oct 18, 9:19 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> > >> hope that you now would understand the point I made to
> > >> the op that there being only 1 epsilon (binary) relation symbol would
> > >> be a weakness in some applications of (typical) set-theories.
>
> > > Sorry, I don't.
>
> > What didn't you understand?
>
> > - You were unable  to  understand the concept of "string" (finite,
> >    adjacent, 1 direction)?
> > - You were unable to understand the concept of "sub-string" which
> >    is also a string?
>
> > - You were unable to express "strings" in L(ZF)?
>
> I understand the notions of string and substrings and as expressed in
> set theory.
>
> > What specifically prevented you from understanding what seems
> > to be a simple point, problem?
>
> I take it that your point is in this challenge?:
>
> "using _the lone_ epsilon relation symbol 'e' express
> a sub-string s' of a general string s and s' is a string as s is."
>
> I don't see a problem here since I take 'string' and 'substring' in
> the sense of sequence and subsequence, which are rigorously defined
> in, for example, set theory.

Unless Nguyen gets back to this, I'm going to dismiss his claim that
there is an actual "problem" that he's found.

MoeBlee

[Frederick Williams]

Nam Nguyen wrote:

>
> Would a sub-string be of the same concept as that of a string,
> under Kuratowski's definition?
>
> Apparently not. So, there is the problem that you and Frederick
> have missed.

Guilty as charged: I missed it. Indeed I missed it so well that I don't
even know what I missed. But more seriously: what to you are a string
and a sub-string? If this

abcdef

is a string, is

bde

a sub-string? Or do the elements of the sub-string have to be
contiguous as in

cde ?

[Nam Nguyen]

First thing first, by a sequence a1, a2, ..., an you mean the
generalized Kuratowski' definition of ordered n-tuple we mentioned
before?

[Nam Nguyen]

On 23/10/2012 1:38 PM, Frederick Williams wrote:
> Nam Nguyen wrote:
>
>>
>> Would a sub-string be of the same concept as that of a string,
>> under Kuratowski's definition?
>>
>> Apparently not. So, there is the problem that you and Frederick
>> have missed.
>
> Guilty as charged: I missed it. Indeed I missed it so well that I don't
> even know what I missed. But more seriously: what to you are a string
> and a sub-string? If this
>
> abcdef
>
> is a string, is
>
> bde
>
> a sub-string? Or do the elements of the sub-string have to be
> contiguous as in
>
> cde ?

Right. "cde" is a sub-string but not "bde". Not different from
the concept of a formula string.

[MoeBlee]

On Oct 23, 7:50 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> On 23/10/2012 10:54 AM, MoeBlee wrote:

> > Unless Nguyen gets back to this, I'm going to dismiss his claim that
> > there is an actual "problem" that he's found.
>
> First thing first, by a sequence a1, a2, ..., an you mean the
> generalized Kuratowski' definition of ordered n-tuple we mentioned
> before?

Some authors use tuples and other authors use functions.

I prefer to use functions. So a sequence is a function whose domain is
an ordinal. A finite sequence is a function whose domain is a finite
ordinal (i.e. natural number).

However for every finite sequence there is a corresponding tuple and,
inversely, for every tuple there is the corresponding finite sequence.
So we can translate between finite sequences and tuples at will.

One difference though is that to have the theorem that for any set S
there exists the set of all finite sequences of members of S does not
require the axiom schema of replacement, but to prove the theorem that
for any set S there exists that set of all tuples of members of S does
use the axiom schema of replacement.

Anyway, as I said, I see no "problem" that you've found.

MoeBlee

[MoeBlee]

Nam Nguyen:

I'm just wondering whether you will respond here (of course, in you
own time, which is fair) or whether this will be yet another instance
in which I wasted my time tracking with you virtually point by point -
and here again answering your question to me - only to arrive at the
dead end that you have no coherent point to sustain.

[Nam Nguyen]

Since you don't seem to see any problem, why don't you go helping
Frederick answering my questions about strings.

[Frederick Williams]

Nam Nguyen wrote:

>
> Since you don't seem to see any problem, why don't you go helping
> Frederick answering my questions about strings.

The question ids answered: the notion of a string can be expressed in
set theory with only $\in$ as its extra-logical symbol.

--
I have seen elephants paint very competently... but not in Cumbria.

[Frederick Williams]

Frederick Williams wrote:

>
> The question ids answered:

Ids? Is, I suppose.

[Frederick Williams]

Nam Nguyen wrote:

>
> Since you don't seem to see any problem, why don't you go helping
> Frederick answering my questions about strings.

If I recall the problem was to talk about strings, and in particular
substrings, in the language of set theory. Thereby refuting your daft
claim that there needed to be more than one epsilon or more than one
interpretation of epsilon.

Let Sigma be a non-empty finite set. A finite string over Sigma is a
function

f : X --> Sigma

where X is a finite (possibly empty) set of natural numbers. A
substring of f is f restricted to Y a subset of X. Since any such Y is
also a finite (possibly empty) set of natural numbers, a substring is a
string.

Everything above is expressible in the FO language of $\in$. $\in$ only
needs one interpretation.