On Thu, 07 Apr 2016 21:47:06 -0700, Dan Christensen wrote:
> A Formal DC Proof Introduction to Group Theory, Part 1 > > The axioms of set theory: > > 1 Set(g) > > 2 ALL(a):ALL(b):[a in g & b in g => a*b in g] > > 3 ALL(a):ALL(b):ALL(c):[a in g & b in g & c in g => a*b*c=a*(b*c)] > > 4 e in g > > 5 ALL(a):[a in g => a*e=a & e*a=a] > > 6 ALL(a):[a in g => inv(a) in g & a*inv(a)=e & inv(a)*a=e] > > where > > g = non-empty set * = composition operator on g e = identity > element under * inv = inverse operator on g
It looks weird.
In which logic are there well-formed statements like this? Set(g) and inv(a) seem undefined here. Line "(4) e in G" seems to express that every set belongs to g, which is meaningless in any consistent theory: what are you quantifying over? It is true in group theory that every element belongs to the group. But in set theory you cannot express that everything is in your set g.
I know what you mean. But you have to combine (4) and (5) into a single statement which says that there exists e such that for all a etc.
Maybe DC is a completely different kind of "formality" than what everyone else is used to. Something new to learn perhaps. I will accept that "DC axioms" are meaningful statements in some kind of logic that I do not understand.
What is usually called axioms of group theory do not express that there exists a unique inv(a) s.t. etc. It says that for each a there exists b s.t. a*b=b*a=e. It is a theorem that there exists exactly one such b, as opposed to an axiom.
There is a `:' following "set theory", what does that mean. Grammatically it should mean that the following are axioms of set theory. I notice they are not.
How do you deal with the fact that group theory is provably consistent in ZF (because groups exist). But ZF is provably not provably consistent in ZF? So in view of that, how can you believe that set theory is a part of group theory?