Re: Comparing DC Proof with Metamath proof software

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

Date: Fri, 1 Oct 2004 14:15:29 -0400

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

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

Relevant Pages

  • Re: Comparing DC Proof with Metamath proof software
    ... > Why not find a book on group theory and take a look at the sort ... > group G then the order of S divides the order of G. ... finite group and and arbitrary subgroup. ... > certainly not a statement about one underlying set. ...
    (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: Comparing DC Proof with Metamath proof software
    ... > group theory, you seem to have conceded the point. ... we start with the group axioms ... for an arbitrary group. ... For most of mathematics then, ...
    (sci.logic)
  • Re: Comparing DC Proof with Metamath proof software
    ... >> And how exactly do you plan to do this, ... >> is derive results from the group axioms? ... > would also need the rudiments of number theory for this proof. ... group theory, you seem to have conceded the point. ...
    (sci.logic)
  • Re: Comparing DC Proof with Metamath proof software
    ... > those results that can be derived from the group axioms. ... I think the usual name for that is "elementary group theory". ... It's only a minuscule fraction of what goes under the name ...
    (sci.logic)
Quantcast