Re: Comparing DC Proof with Metamath proof software

From: David C. Ullrich (ullrich_at_math.okstate.edu)
Date: 10/02/04 

Date: Sat, 02 Oct 2004 06:14:37 -0500

On Fri, 1 Oct 2004 14:15:29 -0400, "Dan Christensen"
<dchris@allstream.net> wrote:

>
>"Mike Oliver" <mike_lists@verizon.net> wrote in message
>news:2s5gebF1h61fnU2@uni-berlin.de...
>> Dan Christensen wrote:
>>
>> > Correct me if I am wrong, but my understanding is that group theory is
>just
>> > those results that can be derived from the group axioms.

You're wrong.

>> I think the usual name for that is "elementary group theory". It's
>> not terribly interesting--it consists of a lot of statements
>> like
>> (forall a)(forall b)(b^2=e --> abba=a^2)
>>
>> It's only a minuscule fraction of what goes under the name
>> "group theory".
>
>You mean the group axioms plus others, e.g. the binary operator being
>commutative, or the underlying set being finite?

Why not find a book on group theory and take a look at the sort
of things that are in it? The things you're talking about above
are just a trivial part of group theory - most of it has to do
with those axioms plus set theory. Take the first significant
theorem in most treatments: If S is a subgroup of the finite
group G then the order of S divides the order of G. That's
not something you can even state in the language we're talking
about above, as far as I can see. Or "the kernel of a homomorphism
from G to another group is a normal subgroup of G" - that's
certainly not a statement about one underlying set.

>Also, in developing the theory (writing proofs in group theory), isn't there
>always just one underlying set (unless, of course, you have a theorem about
>two or more groups), plus maybe the natural numbers under consideration at
>any one time? Don't most proofs start with something like, let (g,+) be an
>arbitary group, with underlying set g and binary operator +, plus any other
>axioms, e.g. + being commatative? That's what we have been disputing here.
>Another opinion would be appreciated.
>
>Dan
>Download DC Proof 1.0 at http://www.dcproof.com
>

************************

David C. Ullrich