I am completing a self study guide from Stanfords "Teach yourself Logic" course, and I am stuck on a problem regarding multidimensional induction.
"Starting with the axioms for e given in Section 12.6, it is possible to prove that e is transitive, i.e. ∀x.∀y.∀z.(e(x,y) ∧ e(y,z) ⇒ e(x,z)). Doing this requires a three variable induction, and it is quite messy. Your job in this problem is to prove just the base case for the outermost induction, i.e. prove ∀y.∀z.(e(a,y) ∧ e(y,z) ⇒ e(a,z)). Hint: Use the strategy illustrated in section 12.6. Extra credit: Do the full proof of transitivity."
Editors note: Please be aware that this course provides show answer buttons in its questions. For this reason it will be more constructive to explain the general methods of solving all problems of this sort, rather than provide an answer.
In the Herbrand logic course, Linear Induction if of the form:
\begin{align} &p(a)\\ &\forall n.(p(n)\implies p(s(n)))\\ &---------\\ &\forall n.(p(n)) \end{align}
While Multidimensional induction is of the form:
\begin{align} &\forall m.(p(a,m))\\ &\forall n.(\forall m.\big(p(n,m)\big)\implies \forall m.\big(p(s(n),m) \big))\\ &-----------------\\ &\forall n.(\forall m.\big(p(n,m)\big)) \end{align}
It is called multidimensional induction because in effect you are doing induction on $n$ for each and every $m$, which there could be multiple of.
In both forms, the goal is to find the base case, then assume a particular case, and then prove from this particular case that the next case is true. When using multidimensional induction, the assumption of a particular case is always quantified over $\forall m.\big(p(n,m)\big)$, which narrows the search of where to start.
In this particular example, you are asked to prove $\forall y.(\forall z.(e(a,y) \land e(y,z) \implies e(a,z)))$, this means your base case should be $(1)$, and the particular case $(2)$.
$$\tag{1}\forall z.(e(a,a) \land e(a,z) \implies e(a,z))$$
$$\tag{2}\forall z.(e(a,y) \land e(y,z) \implies e(a,z))$$
It is noteworthy that the particular case $(2)$ is the same as the thing you are trying to prove, less one universal quantifier. This is true for all multidimensional induction problems (including linear induction).
After assuming $(2)$, your goal will be to prove $\forall z.(e(a,s(y)) \land e(s(y),z) \implies e(a,z))$. This can be done by assuming its antecedent, $e(a,s(y)) \land e(s(y),z)$, then using the fact that $e(a,s(y))$ is in contradiction with premises $4$ of the question to prove $e(a,z)$.
Once this has been done, you can universally quantify over everything, and then use induction in the last step to complete the question.
EDIT: After your edit, you have completed the base case and are now on the inductive step. Your goal is to prove $(3)$.
$$\tag{3}\big(\forall z.(e(a,y) \land e(y,z) \implies e(a,z))\big)\implies\big(\forall z.(e(a,s(y)) \land e(s(y),z) \implies e(a,z))\big)$$
You have already made the first step toward this goal, by assuming $\forall z.(e(a,y) \land e(y,z) \implies e(a,z))$.
The next step is to arrive at $e(a,s(y)) \land e(s(y),z) \implies e(a,z)$, and universally quantify over it. This is best achieved by assuming $(4)$, and deriving $e(a,z)$.
$$e(a,s(y)) \land e(s(y),z)\tag{4}$$
The derivation of $e(a,z)$ from the assumption $(4)$ can be made by exploiting the fact that your assumption is in contradiction with the $4^{th}$ premises. It is possible to assume $\sim e(a,z)$, then derive $e(a,s(y))$ and $\sim e(a,s(y))$.