How do I derive $(\forall x)(\forall y)(\exists z)(x = y \circ z)$ from these three group axioms and some previously established theorems?

Question

I am currently self-studying Patrick Suppes' Introduction to Logic and I am stuck on exercise 5.2.4. I've successfully worked out proofs for Theorems 1 to 7, but I am having trouble coming up with a proof for Theorem 8, $(\forall x)(\forall y)(\exists z)(x = y \circ z)$.

This exercise deals with elementary group theory. Using the axioms for groups and the theorems already established, provide formal derivations for the following theorems.

A previous section of the book gives an overview of the non-logical symbols used in this exercise.

The axioms use three non-logical symbols: the binary operation symbol '$\circ$', the unary operation symbol '$^{-1}$', and the individual constant '$e$'. The most familiar interpretation is to take as the domain of interpretation the set of integers (positive, negative, and zero), to interpret '$\circ$' as '+', to interpret '$^{-1}$' as the operation symbol for negating a number, and to interpret '$e$' as the name of zero.

The three axioms are as follows.

Ax. 1. $(\forall x)(\forall y)(\forall z)(x \circ (y \circ z)) = (x\circ y)\circ z)$.

Ax. 2. $(\forall x)(x \circ e = x)$.

Ax. 3. $(\forall x)(x \circ x^{-1} = e)$.

The theorems to be proved are as follows.

Th. 1. $(\forall x)(\forall y)(\forall z)(x\circ z = y \circ z \rightarrow x = y)$.

Th. 2. $(\forall x)(x \circ e = e \circ x)$.

Th. 3. $(\forall y)((\forall x)(x \circ y = x) \rightarrow y = e)$.

Th. 4. $(\forall x)(x \circ x^{-1} = x^{-1} \circ x)$.

Th. 5. $(\forall x)(\forall y)(\forall z)(z \circ x = z \circ y \rightarrow x = y)$.

Th. 6. $(\forall x)(\forall y)(x \circ y = e \rightarrow y = x^{-1})$.

Th. 7. $(\forall x)((x^{-1})^{-1} = x)$.

Th. 8. $(\forall x)(\forall y)(\exists z)(x = y \circ z)$.

I am still trying to figure out my angle of attack for Theorem 8. My first thought was to assume the negation of the theorem and derive a proof by contradiction, but that didn't go anywhere.

I tried using Axiom 2 to existentially generalize $e$ as z, but that left me with x = x instead of x = y.

I also spent a rather long time specifying various values for the previously established theorems, hoping to come across something useful.

My latest intuitive notion was that Theorem 7 must play some role in this, and that I should specify two values for x, but I wasn't able to make much progress that way.

Answer 1

I finally managed to derive the following proof by contradiction, but I still think there must be an alternate approach.

$$\begin{array}{} \{1,2,3\} & \vdash & (\forall x)(\forall y)(\exists z)(x = y \circ z) & \cr\cr \{1\} & 1 & (\forall x)(\forall y)(\forall z)(x \circ (y \circ z)) = (x\circ y)\circ z) & \hbox{Premise (Axiom 1)} \cr \{2\} & 2 & (\forall x)(x \circ e = x) & \hbox{Premise (Axiom 2)} \cr \{3\} & 3 & (\forall x)(x \circ x^{-1} = e) & \hbox{Premise (Axiom 3)} \cr\cr \{4\} & 4 & \hphantom{---}(\forall z)(x \neq y \circ z) & \hbox{Premise (Assumption)} \cr \{4\} & 5 & \hphantom{---}x \neq y \circ (y^{-1} \circ x) & \hbox{Universal Specification 4} \cr \{1\} & 6 & \hphantom{---}y \circ (y^{-1} \circ x) = (y \circ y^{-1}) \circ x \hphantom{} & \hbox{Universal Specification 1 ($\times 3$)}\cr \{1,4\} & 7 & \hphantom{---} x \neq (y \circ y^{-1}) \circ x & \hbox{Identity 5,6} \cr \{3\} & 8 & \hphantom{---} y \circ y^{-1} = e& \hbox{Universal Specification 3} \cr \{1,3,4\} & 9 & \hphantom{---} x \neq e \circ x & \hbox{Identity 7,8} \cr \{1,2,3\} & 10 & \hphantom{---} (\forall x)(x \circ e = e \circ x) & \hbox{Theorem 2} \cr \{1,2,3\} & 11 & \hphantom{---} x \circ e = e \circ x & \hbox{Universal Specification 10} \cr \{1,2,3,4\} & 12 & \hphantom{---} x \neq x \circ e & \hbox{Identity 9,11} \cr \{2\} & 13 & \hphantom{---} x \circ e = x& \hbox{Universal Specification 2} \cr \{1,2,3,4\} & 14 & \hphantom{---} x \neq x & \hbox{Identity 12,13} \cr \Lambda & 15 & \hphantom{---} x = x& \hbox{Identity} \cr \{1,2,3,4\} & 16 & \hphantom{---} x = x \land x \neq x& \hbox{Tautology (Adjunction 15,14)} \cr \{1,2,3\} & 17 & \lnot(\forall z)(x \neq y \circ z) & \hbox{Reductio Ad Absurdum 4,16} \cr \{1,2,3\} & 18 & (\exists z)(x = y\circ z) & \hbox{Quantifier Interchange 17 (Q1)} \cr \{1,2,3\} & 19 & (\forall x)(\forall y)(\exists z)(x = y\circ z) & \hbox{Universal Generalization 18} \cr\cr \Box \end{array}$$

Answer 2

Here is how I would think about how to solve this problem: Groups are an abstraction of the nice properties of a ring under the operation of addition. That is, when you add two integers, you get another integer, addition is associative, you have an identity (0), and every element has an inverse ($(x)+(-x)=0$). (Warning: Commutativity is not (necessarily) a property of groups!!!!!!!!!!!!!!!!).

The theorem that you are trying to prove is analogous to solving:

$x=y+z$.

As we know from elementary algebra, we add the inverse of $y$ to both sides, and in this case, since the operation in a group need not be commutative, we do it on the left to both sides. $(-y)+x=(-y)+(y+z)$.

So we get $z=(-y)+x$ (Steps to be filled on how you get here) or in your notation, $z=y^{-1}\circ x$.