Re: Comparing DC Proof with Metamath proof software

From: Dan Christensen (dchris_at_allstream.net)
Date: 10/02/04 

Date: Sat, 2 Oct 2004 12:46:20 -0400

"David C. Ullrich" <ullrich@math.okstate.edu> wrote in message
news:n33tl09v5opl4l2imb307ktb3eq1matnlc@4ax.com...
> 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?

Have done so.

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.

This just proves my point. To prove this theorem, we start with an arbirtary
finite group (G,*) and and arbitrary subgroup (S,*). We would have two
underlying sets: S and G, with S being a subset of G. We then would prove
that the order of S divides the order of G. Then we can generalize for the
infinite number of such cases.

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

Likewise. As with most proofs in mathematics, you start with an arbitrary ca
se, derive a consequence from it, and then generalize for all cases.

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

Relevant Pages

  • Re: Comparing DC Proof with Metamath proof software
    ... You mean the group axioms plus others, e.g. the binary operator being ... 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 ...
    (sci.logic)
  • Re: Comparing DC Proof with Metamath proof software
    ... > a single underlying set. ... So, you must start with an ARBITRARY group, say with a single, ... generalizations that apply to all others. ... Correct me if I am wrong, but my understanding is that group theory is just ...
    (sci.logic)
  • Re: finite group
    ... Group Theory - he attributes it to Frobenius: ...
    (sci.math)
Quantcast