On Nov 1, 4:41 pm, Dan Christensen <
Dan_Christen...@sympatico.ca>
wrote:
> Notation:
>
> ob = class of objects
> mor = class of morphisms
> dom(f) = domain of f
> cod(f) = codomain of f
> comp(g,f) = the composition operator (for functions f and g, comp(g,f)
> = g o f)
> hom(x,y) = the class of morphisms with domain of x and codomain of y
>
> @ = epsilon (indicates class membership)
> & = AND-operator
> => = IMPLIES-operator
> <=> = IFF-operator
>
> The ordered sextuple (ob, mor, dom, cod, comp, hom) comprises a
> category iff the following axioms hold:
>
> Axioms 1-3 define dom and cod. Each morphisms has a unique domain and
> codomain. Note that morphisms are seen here only as are mappings from
> the ELEMENTS of one object to the elements of another object. If, for
> example, you want to define to define a category on the set of natural
> numbers, you would have to use the set of singletons of natural
> numbers for ob = {{1}, {2}, {3}, ...}. This should not be an onerous
> requirement.
It is hard to say that anything "defines" any functor in a first-order
language.
If it TRULY "defined" it then the functor WOULD BE ELIMINABLE in FAVOR
OF its definition.
What is INSTEAD true in this kind of treatment is that EVERY functor
is jointly "defined" by EVERY axiom IN WHICH IT OCCURS.
All the ZFC axioms -- for example -- the conjoined infinity of them,
are just one long definition of epsilon.
>
> 1 ALL(f):[f @ mor => dom(f) @ ob]
>
> 2 ALL(f):[f @ mor => cod(f) @ ob]
>
> 3 ALL(f):[f @ mor => ALL(a):ALL(b):[(a,b) @ f => a @ dom(f) & b @
> cod(f)]]
>
> Identity morphisms exist for all objects.
>
> 4 ALL(a):[a @ ob => EXIST(i):[i @ mor & ALL(b):[b @ a => (b,b) @ i]]]
>
> The composition operator comp
>
> 5 ALL(f):ALL(g):[f @ mor & g @ mor => [cod(f)=dom(g) => comp(g,f) @
> mor
> & dom(comp(g,f))=dom(f)
> & cod(comp(g,f))=cod(g)
> & ALL(a):ALL(b):[(a,b) @ comp(g,f) <=> EXIST(c):[(a,c) @ f & (c,b) @
> g]]]]
>
> Associativity of composition
>
> 6 ALL(f):ALL(g):ALL(h):[f @ mor & g @ mor & h @ mor => [cod(f)=dom(g)
> & cod(g)=dom(h)
> => comp(comp(h,g),f)=comp(h,comp(g,f))]]
>
> hom classes exist for each ordered pair of objects.
>
> 7 ALL(a):ALL(b):[a @ ob & b @ ob => ALL(f):[f @ mor => [f @ hom(a,b)
> <=> dom(f)=a & cod(f)=b]]]
>
> Your comments are welcomed.
>
> Dan
> Download my DC Proof 2.0 athttp://
www.dcproof.com
Here is a 3-axiom treatment from a founder of the field (McLarty):
> DEFINITION: An arrow u is an "identity" iff, for every arrow f with the composite fu defined, fu=f.
> AXIOM C1: If u is an identity, then for any arrow g with the composite ug defined, ug=g.
> AXIOM C2: For every arrow f there is a unique identity u with the composite fu defined, and a unique identity v with vf defined.
> We write f:u-->v to say u and v are identities and the composites are defined.
> AXIOM C3: For any arrows f, g, h, if gf and hg are defined then the associativity equation holds and both sides are defined:
> h(gf) = (hg)f
> These are first order axioms for a theory of arrows (i.e. for > a category).
I find this treatment odd in that "defined" is not normally considered
a first-order primitive where I come from, but you might find
"defined" to be both well-defined and well-implementable in the
context of a machine-parseable treatment. Downsides of this version
include that it seems to require fol WITH equality as opposed to
without, and it seems to require adding a constant "undefined" (one
could then express the requirement that x be defined as
~[x=undefined] ).
But his is arguably better in that it only needs = whereas you need
both = and @.