Dan Christensen

2012-10-18 04:46:28 UTC

The class of all groups (g,add) could be defined as:

ALL(g):ALL(add):[(g,add) @ groups

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

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)

For each pair of groups (g,add) and (g',add'), we can define the class

of morphisms

ALL(g):ALL(add):ALL(g'):ALL(add'):[(g,add) @ groups & (g',add') @

groups

=> EXIST(mor):ALL(f):[f @ mor <=> ALL(a):[a @ g => f(a) @ g']

& ALL(a):ALL(b):[a @ g & b @ g => f(add(a,b)) = add'(f(a),f(b))]]]

where mor is the class of morphisms (homomorphisms) .from group

(g,add) to group (g',add')

Comments?

Dan

Download my DC Proof 2.0 software a thttp://www.dcproof.com

ALL(g):ALL(add):[(g,add) @ groups

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

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)

For each pair of groups (g,add) and (g',add'), we can define the class

of morphisms

ALL(g):ALL(add):ALL(g'):ALL(add'):[(g,add) @ groups & (g',add') @

groups

=> EXIST(mor):ALL(f):[f @ mor <=> ALL(a):[a @ g => f(a) @ g']

& ALL(a):ALL(b):[a @ g & b @ g => f(add(a,b)) = add'(f(a),f(b))]]]

where mor is the class of morphisms (homomorphisms) .from group

(g,add) to group (g',add')

Comments?

Dan

Download my DC Proof 2.0 software a thttp://www.dcproof.com