Toward a Formal Definition of the Category of Groups in DC Proof

In what language, axioms, inference rules is this definition being
given?

MoeBlee

Frederick Williams

2012-10-18 17:12:28 UTC

Post by MoeBlee
In what language,

Danish.

Post by MoeBlee
axioms, inference rules is this definition being
given?

Excuse the groanful joke, but one needs no axioms or inference rules to
give a definition. I think.

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

MoeBlee

2012-10-18 18:16:23 UTC

On Oct 18, 12:12 pm, Frederick Williams

Post by Frederick Williams
one needs no axioms or inference rules to
give a definition. I think.

To define a constant "THE class of [...]" requires axioms/rules to
prove that there exists a unique such object.

MoeBlee

Frederick Williams

2012-10-18 19:01:06 UTC

On Oct 18, 12:12 pm, Frederick Williams

Post by Frederick Williams
one needs no axioms or inference rules to
give a definition. I think.

To define a constant "THE class of [...]" requires axioms/rules to
prove that there exists a unique such object.

Good batting Thinkman! I must pay more attention.

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

MoeBlee

2012-10-18 19:29:41 UTC

Post by Frederick Williams
Good batting Thinkman!

Rxactly, Eobin.

MoeBlee

David C. Ullrich

2012-10-20 15:56:21 UTC

On Thu, 18 Oct 2012 18:12:28 +0100, Frederick Williams

Post by MoeBlee
In what language,

Danish.

Heh-heh. That's actually very funny.

Post by MoeBlee
axioms, inference rules is this definition being
given?

Excuse the groanful joke, but one needs no axioms or inference rules to
give a definition. I think.

Dan Christensen

2012-10-18 17:50:34 UTC

Post by MoeBlee
In what language, axioms, inference rules is this definition being
given?

Notation (with the usual meanings):

& = AND-operator
=> = IMPLIES-operator
<=> = IFF-operator
ALL = universal quantifier
EXIST = existential quantifier
@ = epsilon (set or class membership)

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

MoeBlee

2012-10-18 18:37:58 UTC

Post by MoeBlee
In what language, axioms, inference rules is this definition being
given?

& = AND-operator
=> = IMPLIES-operator
<=> = IFF-operator
ALL = universal quantifier
EXIST = existential quantifier
@ = epsilon (set or class membership)

Probably, you also have a sentential negation sign and an identity
sign too.

To define "THE class of all groups" requires axioms/rules to prove
there exists a unique object that has the properties in the definens
of the definition.

On the other hand, if you merely want to define the property "is a
group" then, of course, the language of set theory, irrespective of
rules/axioms, you just mentioned is adequate. But then, why not just
use one of the ordinary definitions?

G is a group
<->
Esf(G = <s f> &
f:sXs->s &
f is associative &
ExesAyes(f(<x y>)=f(<y x>)=y & AyesEzes f(<y z)=f(<z y)=x))

MoeBlee

Dan Christensen

2012-10-18 19:49:39 UTC

Post by MoeBlee
In what language, axioms, inference rules is this definition being
given?

& = AND-operator
=> = IMPLIES-operator
<=> = IFF-operator
ALL = universal quantifier
EXIST = existential quantifier
@ = epsilon (set or class membership)

Probably, you also have a sentential negation sign and an identity
sign too.

Yes. '~' and '=' also with the usual meanings.

Post by MoeBlee
To define "THE class of all groups" requires axioms/rules to prove
there exists a unique object that has the properties in the definens
of the definition.

Essentially, what I have is:

ALL(a):ALL(b):[(a,b) @ groups <=> G(a,b)]

The class of groups is just all those ordered pairs (a,b) with
property G. Isn't that sufficient to define a class?

Post by MoeBlee
On the other hand, if you merely want to define the property "is a
group" then, of course, the language of set theory, irrespective of
rules/axioms, you just mentioned is adequate. But then, why not just
use one of the ordinary definitions?
G is a group
<->
Esf(G = <s f> &
f:sXs->s &
f is associative &
ExesAyes(f(<x y>)=f(<y x>)=y & AyesEzes f(<y z)=f(<z y)=x))

I think you are missing some brackets in the last line:

Exes(Ayes(f(<x y>)=f(<y x>)=y) & AyesEzes(f(<y z>)=f(<z y)=x)))

I also like to define an negation (inverse) function.

I also want to define the class of morphisms (homomorphisms) for every
ordered pair of groups. For that, I must refer to the add function for
both groups. And the add functions are NOT uniquely determined by the
underlying set.

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

MoeBlee

2012-10-18 19:55:45 UTC

Post by Dan Christensen
The class of groups is just all those ordered pairs (a,b) with
property G. Isn't that sufficient to define a class?

Depends on the theory. For example, In NBG, you'd have to restrict to
sets as members of any proper class. In Z set theories, there is no
such class, and instead "class" is a figure of speech to indicate
formulas, not actual objects ranged over by the quantifier. I don't
know how it works in category theory.

MoeBlee

Dan Christensen

2012-10-18 20:19:27 UTC

Post by Dan Christensen
The class of groups is just all those ordered pairs (a,b) with
property G. Isn't that sufficient to define a class?

I haven't done much work with classes, but I have an "is a set"
predicate in my system. If an object is not assumed or shown to be a
set, you cannot apply the axioms of set theory to it. To "declare" a
class, I am wondering if it is enough in my system to simply not
declare an object to be a set and still have elements in it.

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

MoeBlee

2012-10-18 21:17:15 UTC

Post by Dan Christensen
I have an "is a set"
predicate in my system.

I thought you just gave me your primitives. Now another one - set?

Post by Dan Christensen
If an object is not assumed or shown to be a
set, you cannot apply the axioms of set theory to it. To "declare" a
class, I am wondering if it is enough in my system to simply not
declare an object to be a set and still have elements in it.

I can't make sense of that.

Why don't you start by telling me all your primitives, axioms, and
rules?

MoeBlee

Dan Christensen

2012-10-18 22:39:30 UTC

Post by Dan Christensen
I have an "is a set"
predicate in my system.

I thought you just gave me your primitives. Now another one - set?

I just gave you the ones in the my original posting.

I can't make sense of that.
Why don't you start by telling me all your primitives, axioms, and
rules?

I have discussed them in detail over the years here. I don't want to
rehash them again. If you are genuinely interested, it's all
documented in the User Reference Guide that comes with my freeware
program. If there is sufficient interest, I can post the user
documentation separately at my website. I would welcome any input or
suggestions.

For now, I just want to make sure I have the definitions right for the
category of groups as expressed in my original posting here.

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

MoeBlee

2012-10-18 22:46:49 UTC

Post by Dan Christensen
I have an "is a set"
predicate in my system.

I thought you just gave me your primitives. Now another one - set?

I just gave you the ones in the my original posting.

Yes, and then you added one. Are there more to add? If so, I don't see
why you don't give them all together.

MoeBlee

Graham Cooper

2012-10-19 02:04:35 UTC

Post by Dan Christensen
I just gave you the ones in the my original posting.

Yes, and then you added one. Are there more to add? If so, I don't see
why you don't give them all together.
MoeBlee

Do you read the WINDOWS 8 Manual?

www.DCPROOF.com

Herc

MoeBlee

2012-10-19 15:30:05 UTC

Post by Graham Cooper
Do you read the WINDOWS 8 Manual?

Do you tip at least 15% when you go out to eat?

MoeBlee

Frederick Williams

2012-10-18 21:34:58 UTC

Post by Dan Christensen
& = AND-operator
=> = IMPLIES-operator
<=> = IFF-operator
ALL = universal quantifier
EXIST = existential quantifier
@ = epsilon (set or class membership)

Probably, you also have a sentential negation sign and an identity
sign too.

Yes. '~' and '=' also with the usual meanings.

Shirley given a theory of sets, with 0, =, ordered pairs, {.|.}, and
<->, you should proceed as follows:

True =df 0 = 0
phi & psi =df <phi,psi> = <True,True>
phi -> psi =df (phi & psi) <-> phi
forall x phi =df {x|phi} = {x|x=x}
False =df forall P P
~phi =df phi -> False
phi v psi =df forall P(((phi -> P) & (psi -> P)) -> P)
exists x psi =df forall P((forall x(phi -> P)) -> P).

You can even conflate = and <->.

Which reminds me, when you've mastered categories, you should turn to
toposes.

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

Graham Cooper

2012-10-18 22:26:56 UTC

Post by MoeBlee
In what language, axioms, inference rules is this definition being
given?

& = AND-operator
=> = IMPLIES-operator
<=> = IFF-operator
ALL = universal quantifier
EXIST = existential quantifier
@ = epsilon (set or class membership)

Probably, you also have a sentential negation sign and an identity
sign too.

Yes. '~' and '=' also with the usual meanings.

Post by MoeBlee
To define "THE class of all groups" requires axioms/rules to prove
there exists a unique object that has the properties in the definens
of the definition.

<<HUFFT!>>

This is how I define individual sets in PROLOG.

SET ........... PREDICATE

e(X,abstract) :- abstract(X).
e(X,curriculum) :- curriculum(X).
e(X,animals) :- animals(X).
e(X,selfish) :- selfish(X).

abstract(art).
abstract(emotion).
abstract(abstract). *** a e a

curriculum(teaching).
curriculum(discipline).
curriculum(curriculum). *** c e c

animals(dog).
animals(cat).

e(X,selfish) :- e(X,X).

-----------------------

This calculates the set of all sets that contain themselves:

?-e(M,selfish).

M = abstract
M = curriculum

----------------

Just a method to convert predicate names into predicate arguments to
do procedures on them. ALL(f): f(a)

Herc

Dan Christensen

2012-10-21 16:22:58 UTC

My latest thoughts....

Post by Dan Christensen
add(a,add(b,c))]
where
@ = epsilon (class membership)
add = a binary function on g that is associative
neg = negation function on g
0 = identity element in g (call it e if you don't want to quantify on
0)

Now, I define a Group predicate as follows:

ALL(g):ALL(add):[Group(g,add)
<=> Set(g)
& ALL(a):ALL(b):[a @ g & b @ g => add(a,b) @ g]
& ALL(a):ALL(b):ALL(c):[a @ g & b @ g & c @ g =>
add(add(a,b),c)=add(a,add(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a @ g => neg(a) @ g]
& 0 @ g
& ALL(a):[a @ g => add(0,a)=a & add(a,0)=a]
& ALL(a):[a @ g => add(a,neg(a))=0 & add(neg(a),a)=0]]]

I define the class of objects that are groups:

ALL(a):ALL(b):[(a,b) @ ob <=> Group(a,b)]

I define an "is a homomorphism" predicate Hom:

ALL(f):ALL(g1):ALL(add1):ALL(g2):ALL(add2):[Hom(f,g1,add2,g2,add2)
<=> Set'(f)
& ALL(a):ALL(b):[(a,b) @ f => a @ g1 & b @ g2]
& ALL(a):[a @ g1 => EXIST(b):[b @ g2 & (a,b) @ f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) @ f & (a,b2) @ f => b1=b2]
& ALL(a):ALL(b):ALL(c):[a @ g1 & b @ g1 & c @ g1 => [add1(a,b)=c =>
add2(f(a),f(b))=f(c)]]]

I then prove that for every pair of groups (g1,add1) and (g2,add2)
there exists a set of all homomorphisms from g1 to g2:

ALL(g1):ALL(add1):ALL(g2):ALL(add2):[Group(g1,add1) & Group(g2,add2)
=> EXIST(homs):[Set(homs)
& ALL(f):[f @ homs <=> Hom(f,g1,add2,g2,add2)]]]

I then prove that for each group, there exists an identity
homomorphism:

ALL(g):ALL(add):[Group(g,add)
=> EXIST(id):[ALL(a):[a @ g => id(a)=a] & Hom(id,g,add,g,add)]]

I may not sure what to do about the associativity of composition. I am
having trouble formalizing this notion. Perhaps nothing is necessary
since composition of morphisms is just "ordinary composition of
functions," but this seems to be a bit much hand waving for my
liking.

I will post my formal proof (212 lines so far) at a later date.

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

Dan Christensen

2012-10-21 23:54:29 UTC

(Correction)

Post by Dan Christensen
My latest thoughts....

ALL(g):ALL(add):[Group(g,add)
<=> Set(g)
add(add(a,b),c)=add(a,add(b,c))]
ALL(f):ALL(g1):ALL(add1):ALL(g2):ALL(add2):[Hom(f,g1,add2,g2,add2)
<=> Set'(f)

That should be:

ALL(a):ALL(b):[a @ g1 & b @ g2 => (a,b) @ f]

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

|-| E R C

2012-10-22 00:05:12 UTC

You guys are all over the place redefining everything from 50 years
ago, General Problem Solver operands, Semantic -ISA- Networks, ..

Welcome to Relational Algebra!

RELATION = { <field1, field2,..,fieldn> , <field1,
field2,..,fieldn> , ... }

Herc

Dan Christensen

2012-10-22 01:18:17 UTC

Post by Dan Christensen
(Correction)

Post by Dan Christensen
My latest thoughts....

ALL(g):ALL(add):[Group(g,add)
<=> Set(g)
add(add(a,b),c)=add(a,add(b,c))]
ALL(f):ALL(g1):ALL(add1):ALL(g2):ALL(add2):[Hom(f,g1,add2,g2,add2)
<=> Set'(f)

Oops! The original was correct.

Dan

Jesse F. Hughes

2012-10-22 01:22:24 UTC

Post by Dan Christensen
(Correction)

Post by Dan Christensen
My latest thoughts....

ALL(g):ALL(add):[Group(g,add)
<=> Set(g)
add(add(a,b),c)=add(a,add(b,c))]
ALL(f):ALL(g1):ALL(add1):ALL(g2):ALL(add2):[Hom(f,g1,add2,g2,add2)
<=> Set'(f)

Surely not.

What you've done here is define g1 x g2 (as a set).

But never mind. You're such a clever lad, I'm sure you've got it right.

--
"Sale or rental of this disc is ILLEGAL. If you have rented or
purchased this disc, please call the MPAA at 1-800-NO-COPYS."
-- The MPAA begins a new anti-piracy program,
found on a DVD purchased in China

Dan Christensen

2012-10-22 06:15:50 UTC

Post by Dan Christensen
My latest thoughts....

ALL(g):ALL(add):[Group(g,add)
<=> Set(g)
add(add(a,b),c)=add(a,add(b,c))]
ALL(f):ALL(g1):ALL(add1):ALL(g2):ALL(add2):[Hom(f,g1,add1,g2,add2)
<=> Set'(f)
add2(f(a),f(b))=f(c)]]]
I then prove that for every pair of groups (g1,add1) and (g2,add2)
ALL(g1):ALL(add1):ALL(g2):ALL(add2):[Group(g1,add1) & Group(g2,add2)
=> EXIST(homs):[Set(homs)
I then prove that for each group, there exists an identity
ALL(g):ALL(add):[Group(g,add)
I may not sure what to do about the associativity of composition. I am
having trouble formalizing this notion. Perhaps nothing is necessary
since composition of morphisms is just "ordinary composition of
functions," but this seems to be a bit much hand waving for my
liking.
I will post my formal proof (206 lines so far) at a later date.

See: http://www.dcproof.com/CategoryGroup.htm

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

|-| E R C

2012-10-22 06:53:18 UTC

Post by Dan Christensen
My latest thoughts....

See:http://www.dcproof.com/CategoryGroup.htm

Looks very impressive, might I suggest an abstract of the proof for us
onlookers and perhaps unwind from the formal side of things a little..

Herc

Dan Christensen

2012-10-22 12:48:28 UTC

Post by |-| E R C

Post by Dan Christensen
My latest thoughts....

See:http://www.dcproof.com/CategoryGroup.htm

Looks very impressive, might I suggest an abstract of the proof for us
onlookers and perhaps unwind from the formal side of things a little..

Will do. Thanks for the suggestion.

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

Dan Christensen

2012-10-22 18:36:45 UTC

Post by |-| E R C

Post by Dan Christensen
My latest thoughts....

See: http://www.dcproof.com/CategoryGroup.htm

Looks very impressive, might I suggest an abstract of the proof for us
onlookers and perhaps unwind from the formal side of things a little..

First, I prove that for all pairs of groups (g1,add1) and (g2,add2),
there exists a set of all those homomorphisms from (g1,add1) to
(g2,add2). To prove the existence of these sets, you start with the
two sets g1 and g2. From these two sets, construct their Cartesian
product g1xg2. From this set, construct the power set pg1xg2. From
this set, select the subset fg1g2 of all those sets of ordered pairs
that are functions mapping g1 to g2. (There is no way of escaping
looking at functions as sets of ordered pairs. The category theorists
here won't be happy, but, oh well!) From fg1g2, select those functions
that represent homomorphisms.

In a similar way, I then prove the existence of an identity
homomorphism for each group. This, too, requires looking at functions
as sets of ordered pairs.

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

MoeBlee

2012-10-22 19:55:17 UTC

Post by Dan Christensen
First, I prove that for all pairs of groups (g1,add1) and (g2,add2),
there exists a set of all those homomorphisms from (g1,add1) to
(g2,add2). To prove the existence of these sets, you start with the
two sets g1 and g2. From these two sets, construct their Cartesian
product g1xg2. From this set, construct the power set pg1xg2. From
this set, select the subset fg1g2 of all those sets of ordered pairs
that are functions mapping g1 to g2.

You don't need to do that each time. We've already done those steps to
prove that for any two sets S and T there exists the set of functions
from S into T, which we denote by 'T^S'. Then, of course (as you
mentioned), just take the subset that is the set of homorphisms from
one structure into the other.

In other words, you're just reporting old news.

MoeBlee

Frederick Williams

2012-10-22 20:44:40 UTC

In what theory of sets is Dan doing his category theory?

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

MoeBlee

2012-10-22 20:58:48 UTC

Post by Frederick Williams
In what theory of sets is Dan doing his category theory?

How would I know?

But isn't it the case that category theory can be axiomatized as an
extension of ZFC?

MoeBlee

Frederick Williams

2012-10-22 21:40:57 UTC

Post by Frederick Williams
In what theory of sets is Dan doing his category theory?

How would I know?
But isn't it the case that category theory can be axiomatized as an
extension of ZFC?

I think ZFC + "a strongly inaccessible cardinal exists" might do.

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

MoeBlee

2012-10-22 21:43:41 UTC

Post by Frederick Williams
I think ZFC + "a strongly inaccessible cardinal exists" might do.

That was my impression, but I'm not versed in it.

What I'm curious to see is an axiomatization in a different language
from set theory - some axiomatization in a special language for
category theory. Is there such a thing?

MoeBlee

Jesse F. Hughes

2012-10-22 22:08:11 UTC

Post by Frederick Williams
I think ZFC + "a strongly inaccessible cardinal exists" might do.

That was my impression, but I'm not versed in it.

Far as I can tell, these subtleties don't really matter in this context,
since so far, if I've skimmed Dan's (really, truly, remarkable and
groundbreaking) work correctly, he's defined an IsAGroup predicate, and
has not defined the category group as a structure in some set theoretic
universe.

Post by MoeBlee
What I'm curious to see is an axiomatization in a different language
from set theory - some axiomatization in a special language for
category theory. Is there such a thing?

You know how most mathematicians avoid worrying too much about
foundational nonsense? In my experience, the same is true about
category theorists. There *is*, of course, work on category theory as a
mathematical foundation, but unless that's your particular interest,
you're likely to ignore it.

At least I did. I was interested in studying categories and their
properties, not what the appropriate foundational setting is for
category theory. I'm afraid I just wasn't curious about that.

Alan Smaill

2012-10-23 11:38:36 UTC

Post by Frederick Williams
I think ZFC + "a strongly inaccessible cardinal exists" might do.

That was my impression, but I'm not versed in it.
What I'm curious to see is an axiomatization in a different language
from set theory - some axiomatization in a special language for
category theory. Is there such a thing?

Not quite what you ask for, but still gives a category-theoretic
foundation for set theory, rather than the other way round
(from way way back):

http://tac.mta.ca/tac/reprints/articles/11/tr11.pdf

Post by MoeBlee
MoeBlee

--
Alan Smaill

MoeBlee

2012-10-23 15:36:23 UTC

Post by Alan Smaill
http://tac.mta.ca/tac/reprints/articles/11/tr11.pdf

Thanks for that. Actually, it is very much along the lines of what
I've been curious to see.

MoeBlee

FredJeffries

2012-10-23 16:16:08 UTC

Post by Alan Smaill

Post by Frederick Williams
I think ZFC + "a strongly inaccessible cardinal exists" might do.

That was my impression, but I'm not versed in it.
What I'm curious to see is an axiomatization in a different language
from set theory - some axiomatization in a special language for
category theory. Is there such a thing?

Not quite what you ask for, but still gives a category-theoretic
foundation for set theory, rather than the other way round
http://tac.mta.ca/tac/reprints/articles/11/tr11.pdf

Lawvere's "Cohesive toposes and Cantor’s 'lauter Einsen'"
referred to in McLarty's introduction is available at
http://ncatlab.org/nlab/files/LawvereCohesiveToposes.pdf

Dan Christensen

2012-10-23 02:36:24 UTC

In what theory of sets is Dan doing his category theory?

It's a kind working subset of ZFC and standard FOL -- the stuff I
believe the average mathematician actually uses in their work. I would
think than any result I derive in this system could also be derived in
ZFC and a more standard FOL.

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

Dan Christensen

2012-10-23 02:29:16 UTC

You don't need to do that each time. We've already done those steps to
prove that for any two sets S and T there exists the set of functions
from S into T, which we denote by 'T^S'.

And those functions would be seen as sets of ordered pairs. There is
no denying it -- the notion of a function supposedly put forward by
category theorists are inadequate even for what must be chapter-one
exercises like this. It seems to me that you cannot separate set and
category theories.

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

Jesse F. Hughes

2012-10-23 03:05:34 UTC

You don't need to do that each time. We've already done those steps to
prove that for any two sets S and T there exists the set of functions
from S into T, which we denote by 'T^S'.

Yes, but you don't know anything about category theory, so how things
seem to you really aren't that interesting.

Category theorists don't much care what sort of things are in T^S, just
so long as the object T^S satisfies the appropriate universal mapping
property (and if it didn't, then it isn't T^S).

All these details about how we encode ordered pairs, what sort of set a
function is, and so on, are useful only to show that there is at least
one object satisfying the defining properties of T^S, but just as soon
as you know that, then you might as well forget the details of the
construction and rely on the definition of exponential.

Of course, you haven't a clue what I mean because you refuse to learn
any category theory. You are stubbornly ignorant.

--
"Am I am [sic] misanthrope? I would say no, for honestly I never heard
of this word until about 1994 or thereabouts on the Internet reading a
post from someone who called someone a misanthrope."
-- Archimedes Plutonium

Dan Christensen

2012-10-23 03:48:10 UTC

You don't need to do that each time. We've already done those steps to
prove that for any two sets S and T there exists the set of functions
from S into T, which we denote by 'T^S'.

Yes, but you don't know anything about category theory, so how things
seem to you really aren't that interesting.

Granted, my impressions of category theory are those of an absolute
beginner.

Post by Jesse F. Hughes
Category theorists don't much care what sort of things are in T^S, just
so long as the object T^S satisfies the appropriate universal mapping
property (and if it didn't, then it isn't T^S).
All these details about how we encode ordered pairs, what sort of set a
function is, and so on, are useful only to show that there is at least
one object satisfying the defining properties of T^S, but just as soon
as you know that, then you might as well forget the details of the
construction and rely on the definition of exponential.

As one expert was quoted, under the heading of "Why Category Theory?"
as saying: "[Category theory] offers a pure theory of functions, not a
theory of functions derived from sets." (D.S. Scott)
http://wwwhome.ewi.utwente.nl/~fokkinga/mmf92b.pdf

Like I said, even one of the most fundamental notions of category
theory -- that a function is nothing more than an arrow connecting a
domain and codomain -- seems inadequate even in the most elementary
application such as this.

From the same source:

"Category theory is quite the most general and abstract branch of pure
mathematics. [...] The corollary of a high degree of generality and
abstraction is that the theory gives almost no assistance in solving
the more specific problems within any of the subdisciplines to which
it applies. It is a tool for the generalist, of little benefit to the
practitioner [...]." (C.A.R. Hoare)

Perhaps it is possible to be TOO abstract, even in pure mathematics.

Unless the above is a gross mischaracterization of category theory, I
think I will stick to the more established set theory. Less glamorous
and trendy perhaps, but at least it can be widely applied in every
branch of mathematics and science. Thanks all for your, ummm...
patience.

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

William Hale

2012-10-23 04:02:12 UTC

In article

You don't need to do that each time. We've already done those steps to
prove that for any two sets S and T there exists the set of functions
from S into T, which we denote by 'T^S'.

Yes, but you don't know anything about category theory, so how things
seem to you really aren't that interesting.

Granted, my impressions of category theory are those of an absolute
beginner.

I don't understand what you are claiming. Are you saying that a
set-theory function cannot be a category-theory function since a
category-theory is nothing more than an arrow connecting a domain and a
codomain? Or, are you saying that a set-theory function cannot be a
category-theory function since a set-theory function doesn't have a
domain and a codomain, but only a set of tuples?

Post by Dan Christensen
"Category theory is quite the most general and abstract branch of pure
mathematics. [...] The corollary of a high degree of generality and
abstraction is that the theory gives almost no assistance in solving
the more specific problems within any of the subdisciplines to which
it applies. It is a tool for the generalist, of little benefit to the
practitioner [...]." (C.A.R. Hoare)
Perhaps it is possible to be TOO abstract, even in pure mathematics.
Unless the above is a gross mischaracterization of category theory, I
think I will stick to the more established set theory. Less glamorous
and trendy perhaps, but at least it can be widely applied in every
branch of mathematics and science. Thanks all for your, ummm...
patience.
Dan
Download my DC Proof 2.0 software at http://www.dcproof.com

Dan Christensen

2012-10-23 04:17:09 UTC

Post by William Hale
In article

You don't need to do that each time. We've already done those steps to
prove that for any two sets S and T there exists the set of functions
from S into T, which we denote by 'T^S'.

Yes, but you don't know anything about category theory, so how things
seem to you really aren't that interesting.

Granted, my impressions of category theory are those of an absolute
beginner.

Neither. I am saying that the set-theoretic notion of a function (as a
set of ordered pairs) should be adequate for every application. The
category-theoretic notion of a function is does not seem adequate for
even the simplest application of category theory itself.

These, of course, are only the opinions of an absolute beginner to the
field. From what I have read so far, however, I am not inspired to
pursue the study of category theory much further. (Yes, I can tell you
are all heart-broken!)

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

William Hale

2012-10-23 04:30:53 UTC

In article

Post by William Hale
In article

You don't need to do that each time. We've already done those steps to
prove that for any two sets S and T there exists the set of functions
from S into T, which we denote by 'T^S'.

Yes, but you don't know anything about category theory, so how things
seem to you really aren't that interesting.

Granted, my impressions of category theory are those of an absolute
beginner.

Neither. I am saying that the set-theoretic notion of a function (as a
set of ordered pairs) should be adequate for every application.

I am not discussing whether set-theoretic notion of a function is
adequate.

Post by Dan Christensen
The category-theoretic notion of a function is does not seem adequate for
even the simplest application of category theory itself.

This is what I am discussing (or asking you about). Are you saying that
category-theoretic notion of a function is not adequate for being
applied to groups? Are you saying that there is no category of groups?

Post by Dan Christensen
These, of course, are only the opinions of an absolute beginner to the
field. From what I have read so far, however, I am not inspired to
pursue the study of category theory much further. (Yes, I can tell you
are all heart-broken!)
Dan
Download my DC Proof 2.0 software at http://www.dcproof.com

FredJeffries

2012-10-23 12:38:35 UTC

Post by Dan Christensen
Neither. I am saying that the set-theoretic notion of a function (as a
set of ordered pairs) should be adequate for every application.

But it isn't.

Shmuel (Seymour J.) Metz

2012-10-23 23:28:10 UTC

In <billh04-***@news.eternal-september.org>, on
10/22/2012

Post by William Hale
I don't understand what you are claiming.

I don't even understand the sources that he is citing. In some
applications of Category Theory the morphisms do not represent
functions, so how can Category Theory be "a pure theory of functions"?
The statement from Hoare, "The corollary of a high degree of
generality and abstraction is that the theory gives almost no
assistance in solving the more specific problems within any of the
subdisciplines to which it applies.", is quite shocking since Category
Theory clearly gives support in the discipline of Algebraic Topology.

--
Shmuel (Seymour J.) Metz, SysProg and JOAT <http://patriot.net/~shmuel>

Unsolicited bulk E-mail subject to legal action. I reserve the
right to publicly post or ridicule any abusive E-mail. Reply to
domain Patriot dot net user shmuel+news to contact me. Do not
reply to ***@library.lspace.org

Frederick Williams

2012-10-23 23:42:28 UTC

Post by Shmuel (Seymour J.) Metz
I don't even understand the sources that he is citing. In some
applications of Category Theory the morphisms do not represent
functions, so how can Category Theory be "a pure theory of functions"?

Dan is only interested in concrete categories. But I don't think he
knows enough category theory to be able to understand the definition of
concrete category. And since he's already decided that category theory
is a waste of time, I doubt that he'll bother to learn even that small
amount.

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

Jesse F. Hughes

2012-10-23 10:51:03 UTC

You don't need to do that each time. We've already done those steps to
prove that for any two sets S and T there exists the set of functions
from S into T, which we denote by 'T^S'.

Yes, but you don't know anything about category theory, so how things
seem to you really aren't that interesting.

Granted, my impressions of category theory are those of an absolute
beginner.

First, this is because you don't understand that category theory can
serve as an alternate foundation to mathematics, without depending on
the category Set at all. It's not surprising you don't understand how
this works. It takes some considerable work in category theory to get
to that point (and since I was never that interested in the foundational
aspects, I have only the haziest of understandings myself).

But, in this respect, category theory does not give a theory of
functions derived from sets.

You're certainly in no position to make that claim, given that you don't
know category theory.

The abstraction is the benefit of category theory, allowing one to prove
theorems for wide varieties of mathematical fields at once, but thereby
also entailing that you're not using any of the details of the
individual fields themselves, and so incapable of solving the *more
specific* problems thereby.

But, of course, not everyone likes the abstraction of category theory.
Nothing wrong with choosing not to study a branch of math you don't
like.

Post by Dan Christensen
Unless the above is a gross mischaracterization of category theory, I
think I will stick to the more established set theory. Less glamorous
and trendy perhaps, but at least it can be widely applied in every
branch of mathematics and science. Thanks all for your, ummm...
patience.

Do what you want.

--
Scientists have calculated that the chance of anything so patently
absurd actually existing are millions to one. But magicians have
calculated that million-to-one chances crop up nine times out of ten.
-- Terry Pratchett on Intelligent Design. Or something.

FredJeffries

2012-10-23 12:28:18 UTC

Post by Dan Christensen
As one expert was quoted, under the heading of "Why Category Theory?"
as saying: "[Category theory] offers a pure theory of functions, not a
theory of functions derived from sets." (D.S. Scott)http://wwwhome.ewi.utwente.nl/~fokkinga/mmf92b.pdf
Like I said, even one of the most fundamental notions of category
theory -- that a function is nothing more than an arrow connecting a
domain and codomain -- seems inadequate even in the most elementary
application such as this.

No category theorist has ever said that "a function is nothing more
than
an arrow connecting a domain and codomain". No one in these
conversations has ever made such a (ridiculous) claim.

It is YOU who claim that every arrow in every category must be
a function with a domain set and a range set. That claim
is just wrong.

In SOME categories, arrows are indeed functions. But not in all
categories.

It is

Post by Dan Christensen
of category theory, I
think I will stick to the more established set theory. Less glamorous
and trendy perhaps, but at least it can be widely applied in every
branch of mathematics and science. Thanks all for your, ummm...
patience.

You do not have to choose one or the other. Use the proper tool
for the job at hand.

Once again, you quote from a very good paper, but you refuse to
read beyond the first page.

Dan Christensen

2012-10-23 14:23:51 UTC

Post by FredJeffries

No category theorist has ever said that "a function is nothing more
than
an arrow connecting a domain and codomain". No one in these
conversations has ever made such a (ridiculous) claim.
It is YOU who claim that every arrow in every category must be
a function with a domain set and a range set. That claim
is just wrong.
In SOME categories, arrows are indeed functions. But not in all
categories.

It is

How so? Of what assistance have any of the theorems of CT been to
ordinary mathematics (e.g. number theory, algebra, analysis) that
could not also have been handled by set theory?

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

FredJeffries

2012-10-23 15:32:01 UTC

Post by Dan Christensen
How so? Of what assistance have any of the theorems of CT been to
ordinary mathematics (e.g. number theory, algebra, analysis) that
could not also have been handled by set theory?

http://mathoverflow.net/questions/19325/most-striking-applications-of-category-theory

FredJeffries

2012-10-23 15:54:32 UTC

http://mathoverflow.net/questions/4235/relating-category-theory-to-programming-language-theory

http://mathoverflow.net/questions/3721/programming-languages-based-on-category-theory

http://cstheory.stackexchange.com/questions/944/solid-applications-of-category-theory-in-tcs

You have written at least one computer program. Presumably in that
program there are functions.
Those functions are not sets of ordered pairs, but they can be
considered to be arrows
between data types.

Dan Christensen

2012-10-23 19:23:58 UTC

http://mathoverflow.net/questions/19325/most-striking-applications-of...

Thanks for the link, Fred. Without a detailed knowledge of the fields
in question, however, it is impossible for me to say whether the same
(probably informal) results could be formally obtained in set theory.

Intuitively and for what it is worth given my limited experience in
this area, I still strongly suspect that any result in formal CT could
also be obtained in formal set theory. I can't imagine that any other
foundational language could surpass the descriptive power of set
theory and FOL.

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

MoeBlee

2012-10-23 19:38:27 UTC

Post by Dan Christensen
Intuitively and for what it is worth given my limited experience in
this area, I still strongly suspect that any result in formal CT could
also be obtained in formal set theory. I can't imagine that any other
foundational language could surpass the descriptive power of set
theory and FOL.

You're blurring the distinction between "expresses" and "proves".

Category theory can be axiomatized in the language of set theory.
Adding "there exists an inaccessible cardinal" to ZFC gives category
theory in the language of set theory. So, anything that category
theory can express can be expressed in set theory (since they have the
same language), but there are statements that category proves that set
theory does not prove.

However, this may itself only skim the surface, since, as suggested by
certain other posters, the mathematician's interest in category theory
is not limited to or even very much concerned with such formal
particulars.

MoeBlee

Dan Christensen

2012-10-23 20:15:04 UTC

You're blurring the distinction between "expresses" and "proves".
Category theory can be axiomatized in the language of set theory.

That's reassuring. There has been some hints in recent discussions
here of CT as an alternative foundation of mathematics. I couldn't see
it.

Post by MoeBlee
Adding "there exists an inaccessible cardinal" to ZFC gives category
theory in the language of set theory.

A simpler approach might be to have an "is a set" predicate that
allows the axioms of set theory to be applicable to only those objects
declared to be sets. You could, for example, have the class of all
sets and avoid the self-contradictions of naive set theory as long as
you don't declare that class to be a set.

Ax (x in S <-> Set(x))

Since S is not declared to be a set (we can call it a "class"), we
can't select from it the subset R, the so-called Russell Set.

Post by MoeBlee
So, anything that category
theory can express can be expressed in set theory (since they have the
same language), but there are statements that category proves that set
theory does not prove.

How can that be if, as you said above, "Category theory can be
axiomatized in the language of set theory?" Do you not include the
axioms of set theory in the "language of set theory?"

Post by MoeBlee
However, this may itself only skim the surface, since, as suggested by
certain other posters, the mathematician's interest in category theory
is not limited to or even very much concerned with such formal
particulars.

That smacks of so much ad hoc hand-waving, does it not?

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

MoeBlee

2012-10-23 20:28:25 UTC

You're blurring the distinction between "expresses" and "proves".
Category theory can be axiomatized in the language of set theory.

That's reassuring. There has been some hints in recent discussions
here of CT as an alternative foundation of mathematics. I couldn't see
it.

Nothing I said contests that category theory may be a foundation for
mathematics.

Post by MoeBlee
Adding "there exists an inaccessible cardinal" to ZFC gives category
theory in the language of set theory.

That's bascially NBG, not category theory.

How can that be if, as you said above, "Category theory can be
axiomatized in the language of set theory?" Do you not include the
axioms of set theory in the "language of set theory?"

The language of set theory is defined by the signature whose only
predicate symbols are 'e' and '='. An axiom of set theory is written
in the language of set theory, but the language itself and the set of
axioms are different things. A language is one thing; a set of
formulas written in said language is a different thing.

Why don't you get a good book on mathematical logic so that you'd have
an informed perspective on this subject?

That smacks of so much ad hoc hand-waving, does it not?

No. 'handwaving' means to try to fake that one has a proof even though
one has not supplied the required logical links that would make a
correct proof. But here I'm not talking about proving anything. I'm
referring merely to what things may or may not interest certain
mathematicians and to certain overall perspectives regarding
mathematics.

MoeBlee

Dan Christensen

2012-10-23 21:10:09 UTC

You're blurring the distinction between "expresses" and "proves".
Category theory can be axiomatized in the language of set theory.

That's reassuring. There has been some hints in recent discussions
here of CT as an alternative foundation of mathematics. I couldn't see
it.

Nothing I said contests that category theory may be a foundation for
mathematics.

Back to square one. (Sigh!)

Post by MoeBlee
Adding "there exists an inaccessible cardinal" to ZFC gives category
theory in the language of set theory.

That's bascially NBG, not category theory.

Are you saying that CT cannot be axiomatized in set theory?

How can that be if, as you said above, "Category theory can be
axiomatized in the language of set theory?" Do you not include the
axioms of set theory in the "language of set theory?"

[snip]

You seem to be needlessly splitting hairs here. Can the axioms of CT
be expressed in set theory and FOL or not? In other words, can CT be
seen as an application of set theory?

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

MoeBlee

2012-10-23 21:46:25 UTC

You're blurring the distinction between "expresses" and "proves".
Category theory can be axiomatized in the language of set theory.

That's reassuring. There has been some hints in recent discussions
here of CT as an alternative foundation of mathematics. I couldn't see
it.

Nothing I said contests that category theory may be a foundation for
mathematics.

Back to square one. (Sigh!)

Why are you sighing in my face? Whatever your squares are - one or
whatever - nothing I've posted to you is incorrect.

Post by MoeBlee
Adding "there exists an inaccessible cardinal" to ZFC gives category
theory in the language of set theory.

That's bascially NBG, not category theory.

Are you saying that CT cannot be axiomatized in set theory?

How could I be any clearer than I've been? I said that (as I've read),
category theory can be formulated in the language of set theory with
the axiomatization ZFC+"there is a strongly inaccessible cardinal".

Usually, by "set theory" we mean ZFC or ZF or along those lines, but
not including "there is a strongly inaccessible cardinal". So, in that
way, category theory is strictly stronger than set theory.

How can that be if, as you said above, "Category theory can be
axiomatized in the language of set theory?" Do you not include the
axioms of set theory in the "language of set theory?"

[snip]
You seem to be needlessly splitting hairs here.

You asked me a damn question and I answered it exactly, but then you
call it "splitting hairs".

My giving you the exact information that is needed to answer your
question is not "splitting hairs".

Post by Dan Christensen
Can the axioms of CT
be expressed in set theory and FOL or not?

I've already said, category theory can be formulated in the first
order language of set theory.

Post by Dan Christensen
In other words, can CT be
seen as an application of set theory?

I don't know what you mean by "application of set theory".

Anyway, AGAIN, I cannot say it any more clearly:

Category theory (as I have read) can be formulated in the language of
set theory and axiomatized by ZFC+"there exists a strongly
inaccessbile cardinal". Now, since set theory as ordinarily taken (say
ZFC or ZF or along those lines) does not prove "there exists a
strongly inacessible cardinal", we have that category theory, as
formulated in the LANGUAGE OF set theory, is strictly stronger than
the THEORY that is set theory.

If still you don't understand that difference between a language and a
theory in said language, then please get a book on mathematical logic.

MoeBlee

Dan Christensen

2012-10-23 22:17:08 UTC

On Oct 23, 5:46 pm, MoeBlee <***@gmail.com> wrote:

[snip]

Post by MoeBlee
Adding "there exists an inaccessible cardinal" to ZFC gives category
theory in the language of set theory.

That's bascially NBG, not category theory.

Are you saying that CT cannot be axiomatized in set theory?

[snip]

Or have an "is a set" predicate (as in NBG and my own DC Proof
program) to avoid the contradictions of naive set theory as I have
outlined above. Correct?

Just to confirm my understanding:

Do you mean that the axioms of CT can be written in the notation of a
suitable set theory and FOL, and that all of the theorems of CT could
be formally derived from only these axioms and the axioms of that set
theory and FOL?

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

FredJeffries

2012-10-23 22:38:47 UTC

Post by Dan Christensen
[snip]

Post by MoeBlee
Adding "there exists an inaccessible cardinal" to ZFC gives category
theory in the language of set theory.

That's bascially NBG, not category theory.

Are you saying that CT cannot be axiomatized in set theory?

[snip]
Or have an "is a set" predicate (as in NBG and my own DC Proof
program) to avoid the contradictions of naive set theory as I have
outlined above. Correct?
Do you mean that the axioms of CT can be written in the notation of a
suitable set theory and FOL, and that all of the theorems of CT could
be formally derived from only these axioms and the axioms of that set
theory and FOL?

http://arxiv.org/abs/0810.1279
http://antimeta.wordpress.com/2007/12/01/foundations-of-category-theory/
http://therisingsea.org/notes/FoundationsForCategoryTheory.pdf

MoeBlee

2012-10-23 22:54:33 UTC

Post by MoeBlee
Adding "there exists an inaccessible cardinal" to ZFC gives category
theory in the language of set theory.

That's bascially NBG, not category theory.

Are you saying that CT cannot be axiomatized in set theory?

Or have an "is a set" predicate (as in NBG and my own DC Proof
program) to avoid the contradictions of naive set theory as I have
outlined above. Correct?

No. Not correct. I already addressed that. Even in your POST HERE, you
QUOTED me about it.

Post by Dan Christensen
Do you mean that the axioms of CT can be written in the notation of a
suitable set theory and FOL, and that all of the theorems of CT could
be formally derived from only these axioms and the axioms of that set
theory and FOL?

No, category theory can't be derived from merely logical axioms. It
takes also the axioms of ZFC (set theory) plus the axiom "there exists
a strongly inaccessible cardinal." That is, category theory can be
formulated so that it is a first order theory whose language is the
language of set theory and such that its axioms are those of ZFC plus
the axiom "there exists an inaccessible cardinal".

Are you trolling just to waste my time?

For the third time:

Category theory can be formulated so that its theorems are all
formulas in the language of set theory and such that those theorems
are all consequences of the axioms of ZFC plus the axiom (which also
is in the language of set theory) "there exists a stongly inaccessible
cardinal".

Why are you not understanding this?

Oh, wait, right, it's because you don't understand the difference
between a language and a theory that is in said language. And you
don't understand that because you won't read a first book in
mathematical logic.

MoeBlee

Dan Christensen

2012-10-24 03:41:59 UTC

Post by MoeBlee
Adding "there exists an inaccessible cardinal" to ZFC gives category
theory in the language of set theory.

That's bascially NBG, not category theory.

Are you saying that CT cannot be axiomatized in set theory?

Or have an "is a set" predicate (as in NBG and my own DC Proof
program) to avoid the contradictions of naive set theory as I have
outlined above. Correct?

No. Not correct. I already addressed that.

You did not adequately address it. You said only, "That's bascially
NBG, not category theory." Did you not understand it? It seems a much
more natural solution than this strange additional axiom of yours.

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

Dan Christensen

2012-10-24 13:12:09 UTC

Post by MoeBlee
Adding "there exists an inaccessible cardinal" to ZFC gives category
theory in the language of set theory.

That's bascially NBG, not category theory.

Are you saying that CT cannot be axiomatized in set theory?

Or have an "is a set" predicate (as in NBG and my own DC Proof
program)

As I understand, NBG has the equivalent of an "is a CLASS" predicate
(indicated by upper-case letters) with sethood and objecthood
(indicated lower-case letters)being the default types . In my system,
I have the opposite: I have an "is a SET" predicate with classhood and
objecthood beng the default, although nowhere in my documentation do I
refer to classes. It just turns out, by happy coincidence, that my
system may be a better way to handle classes. Yes, I know, the
"experts" aren't likely to dump ZF, but they will be saddled with
wonky, ad hoc patches like this additional axiom of yours until they
do.

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

Jesse F. Hughes

2012-10-24 13:17:55 UTC

It just turns out, by happy coincidence, that my system may be a
better way to handle classes. Yes, I know, the "experts" aren't likely
to dump ZF, but they will be saddled with wonky, ad hoc patches like
this additional axiom of yours until they do.

Can I just say that, deep down, I love the bravado of this guy? Lordy,
lordy, but it must be really comforting to know that you are a great
mathematical genius despite the fact that you've spent next to no time
actually studying the existing body of mathematics.

Man, he must get the chicks. Such confidence!

--
Jesse F. Hughes

"It's not a very good combination: adolescence and existentialism."
-- Dragnet TV show (1970)

Frederick Williams

2012-10-24 15:12:03 UTC

Post by Dan Christensen
As I understand, NBG has the equivalent of an "is a CLASS" predicate
(indicated by upper-case letters) with sethood and objecthood
(indicated lower-case letters)being the default types .

NBG (which has different formulations) doesn't need an "is a class"
predicate, if by predicate you mean an undefined symbol (of a certain
kind), "x is a set" is definable by "Ey, x in y" and "x is a class" by
"~(x is a set)".

Post by Dan Christensen
Yes, I know, the
"experts" aren't likely to dump ZF, but they will be saddled with
wonky, ad hoc patches like this additional axiom of yours until they
do.

By "this additional axiom of yours", do you mean "a strongly
inaccessible cardinal exists"? That's just an axiom of infinity which
like the usual axiom of infinity ensures that one has big enough sets.
Using it is the same as accepting that there is a Grothendiek universe
in which one can work, and it is no more controversial than assuming
that the cumulative hierarchy goes up high enough. (Which is not to say
it might not be false, if you think true and false apply to such
things.)

(Apologies to G. if I misspelt his name.)

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

Dan Christensen

2012-10-24 15:58:30 UTC

On Oct 24, 11:12 am, Frederick Williams

NBG (which has different formulations) doesn't need an "is a class"
predicate,

From Wiki:

"NBG is presented here as a two-sorted theory, with lower case letters
denoting variables ranging over sets, and upper case letters denoting
variables ranging over classes."
http://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory

Post by Frederick Williams
if by predicate you mean an undefined symbol (of a certain
kind), "x is a set" is definable by "Ey, x in y" and "x is a class" by
"~(x is a set)".

I mean a predicate Set in the usual sense of FOL. There is no need to
state that a set actually has any elements. After all, a set can be
empty.

Post by Dan Christensen
Yes, I know, the
"experts" aren't likely to dump ZF, but they will be saddled with
wonky, ad hoc patches like this additional axiom of yours until they
do.

By "this additional axiom of yours", do you mean "a strongly
inaccessible cardinal exists"?

Yes.

Post by Frederick Williams
That's just an axiom of infinity which
like the usual axiom of infinity ensures that one has big enough sets.

It would be unnecessary with a Set predicate.

Post by Frederick Williams
Using it is the same as accepting that there is a Grothendiek universe
in which one can work, and it is no more controversial than assuming
that the cumulative hierarchy goes up high enough.

A Set predicate is a much more elegant solution. It has solved a
number of problems in my system, making it much more user-friendly.
Now, it appears to be an effective tool for dealing with so-called
large classes (if you really must).

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

Frederick Williams

2012-10-24 17:43:05 UTC

On Oct 24, 11:12 am, Frederick Williams

NBG (which has different formulations) doesn't need an "is a class"
predicate,

"NBG is presented here as a two-sorted theory, with lower case letters
denoting variables ranging over sets, and upper case letters denoting
variables ranging over classes."
http://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory

That doesn't contradict what I wrote. I pointed out that there are
different formulations and that NBG doesn't _need_ an "is a class"
predicate (stress added). Wikipedia says "is presented here". I didn't
want you to think that NBG always has an "is a class" predicate.

Post by Frederick Williams
if by predicate you mean an undefined symbol (of a certain
kind), "x is a set" is definable by "Ey, x in y" and "x is a class" by
"~(x is a set)".

I omitted "proper" from "x is a proper class"; and you may never need it
anyway.

I mean a predicate Set in the usual sense of FOL. There is no need to
state that a set actually has any elements. After all, a set can be
empty.

Nor did I state that a set actually has any elements, rather it is a
matter of can a collection _be_ an element?

Post by Dan Christensen
Yes, I know, the
"experts" aren't likely to dump ZF, but they will be saddled with
wonky, ad hoc patches like this additional axiom of yours until they
do.

By "this additional axiom of yours", do you mean "a strongly
inaccessible cardinal exists"?

Yes.

Post by Frederick Williams
That's just an axiom of infinity which
like the usual axiom of infinity ensures that one has big enough sets.

It would be unnecessary with a Set predicate.

A Set predicate is a much more elegant solution. It has solved a
number of problems in my system,

Good. But if you want to formalize category theory in some system of
set theory, you'll need big enough sets. It's no different from wishing
to formalize other things, say analysis, and needing a set big enough to
hold, say, all the natural numbers.

making it much more user-friendly.
Now, it appears to be an effective tool for dealing with so-called
large classes (if you really must).

"You"? Isn't it you who want to deal with, for example, the category of
groups and group homomorphisms? The collections of all groups and of
all group homomorphisms are rather large.

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

Jack Campin

2012-10-24 21:31:31 UTC

Post by Frederick Williams
NBG (which has different formulations) doesn't need an "is a class"
predicate,

That's a rather unusual presentation (whose?) but it doesn't have an
"is a class" predicate.

Post by Frederick Williams
By "this additional axiom of yours", do you mean "a strongly
inaccessible cardinal exists"?

Yes.

Post by Frederick Williams
That's just an axiom of infinity which like the usual axiom of
infinity ensures that one has big enough sets.

It would be unnecessary with a Set predicate.

Simply having a Set predicate doesn't tell you how big sets can get.
That's what the existence of an inaccessible tells you. You can't
prove large cardinals exist simply by formulating your set theory in
an NBG-like way.

Just noticed another substantial category theory text you can get free -
Adamek, Herrlich and Strecker's "Abstract and Concrete Categories":

http://katmat.math.uni-bremen.de/acc/

-----------------------------------------------------------------------------
e m a i l : j a c k @ c a m p i n . m e . u k
Jack Campin, 11 Third Street, Newtongrange, Midlothian EH22 4PU, Scotland
mobile 07800 739 557 <http://www.campin.me.uk> Twitter: JackCampin

Frederick Williams

2012-10-24 17:39:26 UTC

Post by Frederick Williams
NBG (which has different formulations) doesn't need an "is a class"
predicate, if by predicate you mean an undefined symbol (of a certain
kind), "x is a set" is definable by "Ey, x in y" and "x is a class" by
"~(x is a set)".

Scrub 'and "x is a class" by "~(x is a set)"' since sets are classes. I
meant 'and "x is a proper class" by "~(x is a set)"'. Sorry.

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

MoeBlee

2012-10-24 16:33:38 UTC

Post by Dan Christensen
As I understand, NBG has the equivalent of an "is a CLASS" predicate

It has an "is a set" predicate.

In NBG, everything is a class. But only certain classes are sets. And
there are also classes that are not sets, which are called 'proper
classes'.

MoeBlee

Dan Christensen

2012-10-24 17:30:17 UTC

Post by Dan Christensen
As I understand, NBG has the equivalent of an "is a CLASS" predicate

It has an "is a set" predicate.
In NBG, everything is a class. But only certain classes are sets. And
there are also classes that are not sets, which are called 'proper
classes'.

I'm not really interested in NBG. (It is actually closer to ZFC than
to my own system.) But no comment on the rest? Since you snipped it,
here it is again:

In my system, I have the opposite: I have an "is a SET" predicate with
classhood and objecthood being the default, although nowhere in my
documentation do I refer to classes. It just turns out, by happy
coincidence, that my system may be a better way to handle classes
[just don't call them sets]. Yes, I know, the "experts" aren't likely
to dump ZF, but they will be saddled with wonky, ad hoc patches like
this additional axiom of yours until they do.

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

MoeBlee

2012-10-24 18:01:01 UTC

Post by Dan Christensen
As I understand, NBG has the equivalent of an "is a CLASS" predicate

It has an "is a set" predicate.
In NBG, everything is a class. But only certain classes are sets. And
there are also classes that are not sets, which are called 'proper
classes'.

I'm not really interested in NBG.

Then why post as you just did that NBG has an 'is a class' predicate?

Post by Dan Christensen
In my system, I have the opposite: I have an "is a SET" predicate

You're not listening. That is NOT the opposite of NBG. NBG has the 'is
a set' predicate.

MoeBlee

Dan Christensen

2012-10-24 18:31:05 UTC

Post by Dan Christensen
As I understand, NBG has the equivalent of an "is a CLASS" predicate

It has an "is a set" predicate.
In NBG, everything is a class. But only certain classes are sets. And
there are also classes that are not sets, which are called 'proper
classes'.

I'm not really interested in NBG.

Then why post as you just did that NBG has an 'is a class' predicate?

Post by Dan Christensen
In my system, I have the opposite: I have an "is a SET" predicate

You're not listening. That is NOT the opposite of NBG. NBG has the 'is
a set' predicate.

Again, I don't give a sh_t about NBG. You brought it up.

But it seems you would rather not comment on my alternative to your
strange, additional axiom to ZFC. Oh, well.

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

MoeBlee

2012-10-24 18:39:54 UTC

Post by Dan Christensen
As I understand, NBG has the equivalent of an "is a CLASS" predicate

It has an "is a set" predicate.
In NBG, everything is a class. But only certain classes are sets. And
there are also classes that are not sets, which are called 'proper
classes'.

I'm not really interested in NBG.

Then why post as you just did that NBG has an 'is a class' predicate?

Post by Dan Christensen
In my system, I have the opposite: I have an "is a SET" predicate

You're not listening. That is NOT the opposite of NBG. NBG has the 'is
a set' predicate.

Again, I don't give a sh_t about NBG. You brought it up.

I brought it up because your earlier proposal was very much like NBG.
Whether that 's interesting to you or not, I don't wish to control.

But then you kept bringing it up again and again, but getting it
wrong, so I corrected you.

Post by Dan Christensen
But it seems you would rather not comment on my alternative to your
strange, additional axiom to ZFC. Oh, well.

Didn't I answer? Didn't I say something to the effect that your
proposal is not, as far as I can tell a formal (pace, Aatu, the other
poster here is specifically proposing a FORMAL system for category
theory) axiomatization of category theory? Just adding a predicate
'set' and having a comprehension axiom for it, does not, as far as I
know (I could be wrong), axiomatize category theory.

MoeBlee

Dan Christensen

2012-10-24 19:07:18 UTC

Post by Dan Christensen
As I understand, NBG has the equivalent of an "is a CLASS" predicate

It has an "is a set" predicate.
In NBG, everything is a class. But only certain classes are sets. And
there are also classes that are not sets, which are called 'proper
classes'.

I'm not really interested in NBG.

Then why post as you just did that NBG has an 'is a class' predicate?

Post by Dan Christensen
In my system, I have the opposite: I have an "is a SET" predicate

You're not listening. That is NOT the opposite of NBG. NBG has the 'is
a set' predicate.

Again, I don't give a sh_t about NBG. You brought it up.

I brought it up because your earlier proposal was very much like NBG.
Whether that 's interesting to you or not, I don't wish to control.
But then you kept bringing it up again and again, but getting it
wrong, so I corrected you.

Post by Dan Christensen
But it seems you would rather not comment on my alternative to your
strange, additional axiom to ZFC. Oh, well.

Didn't I answer?

You said only that it was "basically NBG." It isn't, but I mistakenly
agreed with you.

Post by MoeBlee
Didn't I say something to the effect that your
proposal is not, as far as I can tell a formal (pace, Aatu, the other
poster here is specifically proposing a FORMAL system for category
theory) axiomatization of category theory? Just adding a predicate
'set' and having a comprehension axiom for it, does not, as far as I
know (I could be wrong), axiomatize category theory.

If you said that, I missed it. But thanks for your input.

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

MoeBlee

2012-10-24 19:48:16 UTC

Post by Dan Christensen
You said only that it was "basically NBG." It isn't, but I mistakenly
agreed with you.

Adding a predicate 'set' and comprehension for it is subsumed by NBG.

But the axiomatization for categroy theory I mentioned is not subsumed
by NBG.

Put those together and you have that your alternative is not enough to
axiomatize category theory.

MoeBlee

Jesse F. Hughes

2012-10-24 18:42:51 UTC

Post by Dan Christensen
As I understand, NBG has the equivalent of an "is a CLASS" predicate

It has an "is a set" predicate.
In NBG, everything is a class. But only certain classes are sets. And
there are also classes that are not sets, which are called 'proper
classes'.

I'm not really interested in NBG.

Then why post as you just did that NBG has an 'is a class' predicate?

Post by Dan Christensen
In my system, I have the opposite: I have an "is a SET" predicate

You're not listening. That is NOT the opposite of NBG. NBG has the 'is
a set' predicate.

Again, I don't give a sh_t about NBG. You brought it up.
But it seems you would rather not comment on my alternative to your
strange, additional axiom to ZFC. Oh, well.

You don't have an alternative to "his" strange, additional axiom,
because you don't understand how it's relevant.

Truth be told, neither do I, because I don't know how it comes up in
foundations of category theory. The difference is that, unlike you, I
don't thereby assume it's stupid and I can do better.

Aatu Koskensilta

2012-10-24 18:05:43 UTC

Post by MoeBlee
Usually, by "set theory" we mean ZFC or ZF or along those lines, but
not including "there is a strongly inaccessible cardinal". So, in that
way, category theory is strictly stronger than set theory.

"Category theory" and "set theory" are not (in usual mathematical
parlance) names of formal theories. It makes little mathematical sense
to say either set theory or category theory is stronger or weaker than
the other. In any case, most of standard category theory can be carried
out in a theory conservative over ZFC. It is very rare that universes
actually prove necessary, in any logical sense.

--
Aatu Koskensilta (***@uta.fi)

"Wovon man nicht sprechen kann, darüber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus

MoeBlee

2012-10-24 18:21:48 UTC

I thought I was clear enough that I meant a context in which we are
considering certain formalizations. Indeed as you quoted me saying,
"in that way", I am not making some broader claim about set theory and
category theory regarded as general fields of study.

MoeBlee

Aatu Koskensilta

2012-10-24 18:25:40 UTC

Post by MoeBlee
I thought I was clear enough that I meant a context in which we are
considering certain formalizations. Indeed as you quoted me saying,
"in that way", I am not making some broader claim about set theory and
category theory regarded as general fields of study.

You're right. My apologies. It remains that virtually all uses of
universes in ordinary mathematics are unnecessary. It is a different
matter that formalizing what we may call the category theoretical way of
thinking seems to require (a proper class of) inaccessible cardinals.

--
Aatu Koskensilta (***@uta.fi)

"Wovon man nicht sprechen kann, darüber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus

MoeBlee

2012-10-24 18:29:27 UTC

Post by Aatu Koskensilta
virtually all uses of
universes in ordinary mathematics are unnecessary.

That and your related comment about conservative extension over ZFC
are informative to me.

MoeBlee

Jack Campin

2012-10-23 21:59:10 UTC

Post by MoeBlee
Category theory can be axiomatized in the language of set theory.

That's reassuring. There has been some hints in recent discussions
here of CT as an alternative foundation of mathematics. I couldn't
see it.

It was done about 40 years ago by Lawvere. Justfuckingoogleit.

Post by MoeBlee
Adding "there exists an inaccessible cardinal" to ZFC gives category
theory in the language of set theory.

You get a more natural model using Grothendieck universes, which are
(not quite obviously) equivalent to ZFC + existence of an inaccessible.
You need to model large categories somehow.

-----------------------------------------------------------------------------
e m a i l : j a c k @ c a m p i n . m e . u k
Jack Campin, 11 Third Street, Newtongrange, Midlothian EH22 4PU, Scotland
mobile 07800 739 557 <http://www.campin.me.uk> Twitter: JackCampin

Aatu Koskensilta

2012-10-24 17:58:11 UTC

It's heartening to see this sober assessment of the importance of
formalities from you. To my mind, stressing the relative insignificance
of tedious formalities in cases like this is a necessary prerequisite to
recognizing when formal stuff can actually tell us something of
mathematical and philosophical significance.

--
Aatu Koskensilta (***@uta.fi)

"Wovon man nicht sprechen kann, darüber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus

MoeBlee

2012-10-24 18:02:04 UTC

I do it only as a concession to you and Jesse.

MoeBlee

Jesse F. Hughes

2012-10-24 18:07:43 UTC

I do it only as a concession to you and Jesse.

It's all a matter of what floats your boat. I love category theory, but
I've never had any real interest in learning about the details of its
foundational aspects. I just like doing pointless diagram chases.

--
Jesse F. Hughes
"We need to counter the shockwave of the evildoer by having individual
rate cuts accelerated and by thinking about tax rebates."
-- George W. Bush, Oct. 4, 2001

Aatu Koskensilta

2012-10-24 18:28:11 UTC

Post by Jesse F. Hughes
It's all a matter of what floats your boat. I love category theory, but
I've never had any real interest in learning about the details of its
foundational aspects. I just like doing pointless diagram chases.

I hate category theory. It makes my head hurt. The diagrams in
particular.

--
Aatu Koskensilta (***@uta.fi)

"Wovon man nicht sprechen kann, darüber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus

Jesse F. Hughes

2012-10-24 18:40:29 UTC

Post by Aatu Koskensilta

I hate category theory. It makes my head hurt. The diagrams in
particular.

Because you are a lesser strain of human being. Duh.

Look, I am superior to you. This shouldn't be news.

--
Jesse F. Hughes
"The future is a fascinating thing, and so is history. And you people
are a fascinating part of history, for those in the future."
-- James S. Harris is fascinating, too

MoeBlee

2012-10-24 18:46:26 UTC

Post by Aatu Koskensilta
I hate category theory. It makes my head hurt. The diagrams in
particular.

The diagrams are cute. How could anyone not like the diagrams?

MoeBlee

Jesse F. Hughes

2012-10-24 18:54:30 UTC

Post by Aatu Koskensilta
I hate category theory. It makes my head hurt. The diagrams in
particular.

The diagrams are cute. How could anyone not like the diagrams?

By "cute", I assume you mean, "insightful, powerful, nigh omnipotent."

--
"Quincy, would you rather do epistemology or conceptual analysis?"
"You know what? I'd rather fight on an aircraft carrier.... And Mama
and Baba (Papa) would fight on an aircraft carrier, too."
-- Quincy P. Hughes, age 3 1/2

Frederick Williams

2012-10-24 21:10:51 UTC

Post by Aatu Koskensilta
I hate category theory. It makes my head hurt. The diagrams in
particular.

Even an ophidiophobe should like the snake lemma.

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

Frederick Williams

2012-10-24 21:01:58 UTC

[...] I just like doing pointless diagram chases.

Is that pointless as in without a purpose, or pointless as in pointless
topology?

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

Jesse F. Hughes

2012-10-23 19:42:14 UTC

http://mathoverflow.net/questions/19325/most-striking-applications-of...

Thanks for the link, Fred. Without a detailed knowledge of the fields
in question, however, it is impossible for me to say whether the same
(probably informal) results could be formally obtained in set theory.
Intuitively and for what it is worth given my limited experience in
this area, I still strongly suspect that any result in formal CT could
also be obtained in formal set theory. I can't imagine that any other
foundational language could surpass the descriptive power of set
theory and FOL.

It's not really an issue of whether CT proves things that ZFC can't.
When it comes to standard mathematics, it would be troubling if this
were the case.

It's a matter of naturality of the proof, whether CT, at least in some
cases, presents an argument that evidently gets to the heart of the
matter more easily, clearly, cleanly, etc. Category theory is useful
because it focuses on certain parts of mathematics that are of interest
in disparate fields and does so without having to worry about the
tedious details of set-theoretic representations.

So, you're asking the wrong questions. If Category Theory is an
alternative foundation for mathematics, then it ought to provide an
alternative setting for proving essentially the same theorems as set
theory. If not, (at least) one of the two theories must be broke.

--
"So how do you go on? [...] How will you keep moving for the next few
weeks or months until you are known for what you are, the story
becomes huge all over the world, and you have reporters at your
schools asking you, why?" -- Another JSH mystery

Dan Christensen

2012-10-23 20:57:13 UTC

http://mathoverflow.net/questions/19325/most-striking-applications-of...

Thanks for the link, Fred. Without a detailed knowledge of the fields
in question, however, it is impossible for me to say whether the same
(probably informal) results could be formally obtained in set theory.
Intuitively and for what it is worth given my limited experience in
this area, I still strongly suspect that any result in formal CT could
also be obtained in formal set theory. I can't imagine that any other
foundational language could surpass the descriptive power of set
theory and FOL.

It's not really an issue of whether CT proves things that ZFC can't.
When it comes to standard mathematics, it would be troubling if this
were the case.

Agreed.

Post by Jesse F. Hughes
It's a matter of naturality of the proof, whether CT, at least in some
cases, presents an argument that evidently gets to the heart of the
matter more easily, clearly, cleanly, etc.

Like applying topology to a problem in real analysis?

Post by Jesse F. Hughes
Category theory is useful
because it focuses on certain parts of mathematics that are of interest
in disparate fields and does so without having to worry about the
tedious details of set-theoretic representations.

OK.

Post by Jesse F. Hughes
So, you're asking the wrong questions. If Category Theory is an
alternative foundation for mathematics, then it ought to provide an
alternative setting for proving essentially the same theorems as set
theory. If not, (at least) one of the two theories must be broke.

So, CT can be looked at generalizations akin to group theory or
topology that can be applied to many different "spaces." They are all
axiomatizable in set theory. That would make more sense than CT being
some alternative foundation of mathematics as some have suggested
here. Still, it seems weird and counter-intuitive to think of
functions (morhpisms) as being determined even in part by their
codomains instead of their range (image set).

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

Jesse F. Hughes

2012-10-23 21:16:04 UTC

http://mathoverflow.net/questions/19325/most-striking-applications-of...

Thanks for the link, Fred. Without a detailed knowledge of the fields
in question, however, it is impossible for me to say whether the same
(probably informal) results could be formally obtained in set theory.
Intuitively and for what it is worth given my limited experience in
this area, I still strongly suspect that any result in formal CT could
also be obtained in formal set theory. I can't imagine that any other
foundational language could surpass the descriptive power of set
theory and FOL.

It's not really an issue of whether CT proves things that ZFC can't.
When it comes to standard mathematics, it would be troubling if this
were the case.

Agreed.

Like applying topology to a problem in real analysis?

Yes. I don't mean to speak for others, but I appreciate category theory
for its capacity to abstract. In this respect, using category theory is
similar to using purely topological reasoning to prove a real analysis
result.

That said, those who are interested in such matters also tout category
theory as an *alternative* to set theory as a foundation for
mathematics. Despite my background in logic, this is not my interest,
and so I can't speak knowledgeably about it.

OK.

This is not an either/or proposition. Category theory is useful *both*
because it is a generalization/abstraction like group theory *and*
because it is an alternative foundation for mathematics.

As far as what you think seems "weird", it's simply a matter that you
haven't bothered to learn category theory and see why, from a
categorical perspective, the identity N -> N is a very different
function that the inclusions N -> N + N <- N.

--
Jesse F. Hughes

"Sir, if you won't say sorry for killing father and mother, then I'll
shoot you." -- Quincy P. Hughes (age 4), screenwriter

Aatu Koskensilta

2012-10-24 18:01:18 UTC

Still, it seems weird and counter-intuitive to think of functions
(morhpisms) as being determined even in part by their codomains
instead of their range (image set).

Your intuitions are out of whack. It would be a good idea for you to
work through some good category theory text.

--
Aatu Koskensilta (***@uta.fi)

"Wovon man nicht sprechen kann, darüber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus

Dan Christensen

2012-10-24 18:53:51 UTC

Still, it seems weird and counter-intuitive to think of functions
(morhpisms) as being determined even in part by their codomains
instead of their range (image set).

Your intuitions are out of whack. It would be a good idea for you to
work through some good category theory text.

I am getting bogged down with the initial concepts. I was trying to
put together some formal axioms/definitions so that users could play
around with category theory using my program.

Perhaps you can explain the advantages of obtaining a different
function simply by expanding the codomain. I can see getting a new
function if you change the range (image set).

Or maybe you (or anyone else here) could suggest a workable set of
formal axioms/definitions that would at enable users to do a few
introductory exercises in CT, assuming, say, some knowledge set theory
or abstract algebra.

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

FredJeffries

2012-10-24 20:36:26 UTC

Post by Dan Christensen
Perhaps you can explain the advantages of obtaining a different
function simply by expanding the codomain. I can see getting a new
function if you change the range (image set).

You write computer programs. You ought to be able to answer that
yourself.
How would you declare a function that only takes on some of the
possible
values of the return data type? How would you even know what the
"range set" was in order to declare it?

Or look up "exact sequence".

Or look up "homotopy" or "knot theory" where what is important is the
complement of
the range of a function.

Post by Dan Christensen
Or maybe you (or anyone else here) could suggest a workable set of
formal axioms/definitions that would at enable users to do a few
introductory exercises in CT, assuming, say, some knowledge set theory
or abstract algebra.

Harold Simmons has course notes with exercises:
www.cs.man.ac.uk/~hsimmons/zCATS.pdf
http://www.cs.man.ac.uk/~hsimmons/BOOKS/CatTheory.pdf
http://www.cs.man.ac.uk/~hsimmons/MAGIC-CATS/CourseNotes-Nov-29.pdf

So does Tom Leinster:
http://www.maths.gla.ac.uk/~tl/ct/

Jonathan Kirby has a page of elementary exercises:
http://www.uea.ac.uk/~ccf09tku/CTcourse08/ctex1.pdf

I have already recommended Chris Hillman's primer:
http://synrc.com/publications/cat/Category%20Theory/General%20Theory/hillman01categorical.pdf
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.24.3264&rep=rep1&type=pdf

You could also see if your library has Lawvere and Schanuel's
"Conceptual Mathematics: A First Introduction to Categories"
http://books.google.com/books/about/Conceptual_Mathematics.html?id=o1tHw4W5MZQC

FredJeffries

2012-10-23 12:37:10 UTC

The paper of Dana Scott referred to is at
http://mathgate.info/cebrown/notes/scott80.php

That exact quote does not appear, though Scott does say:

"General category theory provides a much purer theory of functions
than
set theory. Category theory gives a theory of functions under
composition
and is also a theory of types. Category theory is extensional in the
sense
that functions (arrows) defined in different ways may be identical and
that
identical functions (arrows) can always replace one another. Some
intensional theories of functions do not provide categories."

If you read further in the Fokkinga paper, you will come to his first
theorem on page 15. After the proof of this theorem, he remarks:
"it is nowhere used that A, B are sets (there is nowhere a membership
[relation])
or that f, g, + are functions or operations, respectively."

FredJeffries

2012-10-23 12:06:20 UTC

Post by Dan Christensen
And those functions would be seen as sets of ordered pairs. There is
no denying it -- the notion of a function supposedly put forward by
category theorists are inadequate even for what must be chapter-one
exercises like this. It seems to me that you cannot separate set and
category theories.

Category theorists DO NOT put forward any notion of function.

Category theorists allow you to use whatever notion of function
suits whatever task is at hand.

FredJeffries

2012-10-23 12:01:29 UTC