On Jan 10, 8:13 pm, Marshall <marshall.spi...@gmail.com> wrote: > On Jan 10, 2:21 pm, Dan Christensen <Dan_Christen...@sympatico.ca> > wrote: > > On Jan 10, 4:11 pm, Frederick Williams <freddywilli...@btinternet.com> > > wrote: > > > > Dan Christensen wrote: > > > > > [...] On its own, the axiom (Ax)x+0=x, > > > > for example, makes no sense. > > > > It says, does it not, "the binary operator called + has a right identity > > > called 0". > > > > How does it manage to say that if it makes no sense? > > > Let me put this way: (Ax)x+0=x won't get you very far as a formal > > axiom in group theory. A some point, you are going have to make > > statements and derive theorems about two or more DIFFERENT sets. Do > > you see this axiom being applied to every element of those sets, > > whatever they may be? > > Dan, > > I can see here just exactly how and why the conversation goes > awry when you talk with the other folk here. My background is > the same as yours, (AFAIK): I'm a programmer by training and > by vocation, I have an interest in math and especially logic, > which I'm picking up in a very ad hoc way, and I write theorem > prover software as a hobby. So I think I understand your > perspective in a way that, say, someone with a PhD in logic > will not. > > You said: > > > Do you see this axiom being applied to every element of > > those sets, whatever they may be? > > This perfectly embodies the distinction that you're missing, > because the answer to this question is a resounding YES!!! > > Perhaps that may sounds ridiculous; please bear with me. > > You know what a "group" is: roughly, a set with an associative > operation, inverse function, identity, right? (I'm sure I'll > get some details wrong; please let's just do big picture for > now.) > > You know how that describes a bunch of different things, right? > Z with addition and 0; permutation groups, whatever. All those > groups. > > So to return to your question, taking "0" as the identity > element for whatever group we are talking about, we KNOW that > (Ax)x+0=x is going to be true when we have x range over whatever > set is the elements of that group. >
As ridiculous it may sound, the notion of such an underlying set is what ModBlee & Co. seem to be taking exception to here. They seem to believe that you can do serious work in group theory without any reference to an underlying set or even set membership. (I really hope I am wrong about this.) They can't talk about subgroups even in the abstract, because then you would have another set to quantify over. And you can't talk about the order of a group or subgroup because the set of natural numbers is yet another set to quantify over. And this all group theory in the most abstract.
> The rules of first order logic guarantee this. > > In fact, FOL guarantees us a lot of things. And we can use those > things to come up with an entire body of work that consists > EXACTLY and ONLY of those things that, literally, can be > "applied to every element of those sets, whatever they may be?" > This body of work consists of every sentence, and only those > sentences, that are true REGARDLESS of what group we are talking > about. >
I was talking about groups in the abstract as well.
> This body of work has a name, and that name is "group theory." >
And, if formally stated, the axioms given for group theory invariably refer to an underlying set and make use of the set membership predicate. I can't believe that I am arguing with people here about such a fundamental point.
> Note that group theory ***doesn't contain any groups***! It's > an abstraction of all groups. > > It is DIFFERENT from any particular group, or from the collection > of all groups, or from any carrier set for some group. It's different > from numbers, arithmetic, and from anything having to do with > sets. It's just a collection of sentences, considered IN ISOLATION. > That isolation is important. > > For a given group, say Z with +/2, -/1, and 0/0, does group theory > tell us everything we can figure out about that? No, not even > close. We can use lots of other approaches to deal with that > structure. Group theory doesn't exist for that purpose, so in > that light, we may say that "won't get you very far" because > so much is left out. The reason we even bother is because despite > the limitations that group theory has IN THIS CASE, it's still > useful to know ALL and ONLY those things that are true of EVERY > group. > > We use different tools in different contexts. > > If we tried to smush all those tools together into a single > context, we'd have a lot of problems. One thing that we'd > likely have to do is make sure that quantifiers were declared > in such a way that we'd know explicitly what sets they ranged > over. However, if we're just, for a moment, restricting ourselves > to considering ALL and ONLY those sentences that are true of > EVERY group, we don't have to do that. Now you may say that > for that to be useful, we have to consider what happens when > we apply one of those sentences to a particular group, and in > that case we do in fact have this and that sort of machinery > so that we know what that means, and if you want to call that > a "typographic shorthand" then I totally know what you mean. > All this machinery is left unmentioned when we are talking > just about group theory. Know however that when you're talking > to logicians, they will likely reject your perspective; to them, > the machinery is implicit in the definition of "first order > theory" and so you get ALL THIS RESISTANCE from people that you > can't make any sense out of. Consider it a culture clash.
When you write a formal proof in my system, no machinery can be left unmentioned. When I do group theory in my system, as a minimum, I must start with the list of axioms that define a group. I can then use the rules and axioms of logic and set theory that are built-into the program to derive theorems from these axioms. I could define an "is a subgroup of" predicate and include some results from number theory as additional "axioms." As a document, however, the proof must stand on its own with no external references or links. That is were I am coming from. That is my "culture."