Induction proof of transitivity I am trying to solve a three variable induction problem to prove that $e$ is transitive. Formally, the goal is to show:
$∀x∀y∀z:(e(x,y) ∧ e(y,z) ⇒ e(x,z))$
I attempted the complete proof with the below strategy steps, but seem to be hitting a road-block where one inner proof shows the same structure as that of the "Goal" (See step 5 below, where my logic takes me to prove:
$$e(s(x),s(y)) ∧ e(s(y),s(z)) ⇒ e(s(x),s(z))$$
Which step of the strategies written below is incorrect, or am I missing some intermediary proof steps? Is there another way to approach the proof of transitivity? Any advice will greatly help!

Premise:


*

*$e(a,a)$

*$∀x∀y:(e(x,y) ⇒ e(s(x),s(y)))$

*$∀x∀y(e(s(x),s(y)) ⇒ e(x,y))$

*$∀x:-e(a,s(x))$

*$∀x:-e(s(x),a)$
Goal: $$∀x∀y∀z:(e(x,y) ∧ e(y,z) ⇒ e(x,z))$$
For Outermost Induction:
Base Case: 
$∀y∀z:(e(a,y) ∧ e(y,z) ⇒ e(a,z))$
Induction Case: 
$∀x:(∀y∀z:(e(x,y) ∧ e(y,z) ⇒ e(x,z)) ⇒ ∀y∀z:(e(s(x),y) ∧ e(y,z) ⇒ e(s(x),z)))$
Steps:


*

*Prove Base Case

*Prove Base Case of Inner Induction[1]
$∀z:(e(s(x),a) ∧ e(a,z) ⇒ e(s(x),z))$


*Prove Inductive Case for Inner Induction[1]


$∀y:(∀z:(e(s(x),y) ∧ e(y,z) ⇒ e(s(x),z)) ⇒ ∀z:(e(s(x),s(y)) ∧ e(s(y),z) ⇒ e(s(x),z)))$


*Prove Base Case for Inner Induction[2]


$e(s(x),s(y)) ∧ e(s(y),a) ⇒ e(s(x),a)$


*Prove Inductive Case for Inner Induction[2]


$∀z:(e(s(x),s(y)) ∧ e(s(y),z) ⇒ e(s(x),z)) ⇒ ∀z:(e(s(x),s(y)) ∧ e(s(y),s(z)) ⇒ e(s(x),s(z)))$
 A: As Peter Smith wrote, it is unclear what else is assumed as background facts. Clearly you're assuming an induction rule that appears to be copied from Peano Arithmetic (but extended to allow induction over formulas that contain $e$), but how much else from PA do you have?
The language of PA is usually given as $\{{=},0,S,{+},{\times}\}$. Your use of induction seems to require that your $a$ and $s$ are the usual $0$ and $S$, but it looks like your $e$ is an attempt to construct $=$ from scratch without the usual logical equality axioms being stated for it explicitly.
If in addition to $e$ we already have an honest $=$ predicate (with usual equality axioms), as well as at least $+$ and the axioms of PA that don't mention $\times$ -- that is, Presburger arithmetic -- then your assumptions about $e$ are enough to prove $e(x,y)\leftrightarrow x=y$, and thus $e$ must in particular be transitive.
The key steps in this would be first to prove $e(x,x)$ by induction, and then by induction on $x$ prove $\neg e(x,s(x+w))$ and $\neg e(s(x+w),x)$ for fixed $w$. Since Presburger arithmetic proves for any $x$ and $y$ that exactly one of $x=y$ or $\exists w: x=s(x+w))$ or $\exists z: y=s(y+w)$ holds -- for this is true in $\mathbb N$, and Presburger arithmetic is complete -- our goal  $e(x,y)\leftrightarrow x=y$ then follows.

However, the question seems to be more interesting if our language is just $\{a,s,e\}$ so we don't have any primitive equality at all. In that case we can at least manufacture something that behaves like an equality: Define $\approx$ as:
$$ x \approx y \iff \forall z\bigl(e(x,z)\leftrightarrow e(y,z)\bigr) \,\land\, \forall z\bigl(e(z,x)\leftrightarrow e(z,y)\bigr) $$
In other words things are $\approx$ each other if $e$ cannot distinguish them. It is then immediate that $\approx$ is an equivalence relation. We also immediately have
$$ \tag 1 x \approx y \to \bigl( e(x,z) \to e(y,z) \bigr) $$
and
$$ \tag 2 x \approx y \to \bigl( e(z,x) \to e(z,y) \bigr) $$
Since $\approx$ is reflexive it is now an easy induction to prove
$$ \tag 3 x\approx 0 \lor \exists y(x\approx s(y)) $$
and -- now starting to use the explicit premises -- we can now prove
$$ \tag 4 x\approx y \to s(x)\approx s(y) $$
Namely, if $e(s(x),z)$ or $e(s(y),z)$, then $z$ definitely doesn't behave like $0$ in all respect, so due to (3) there is an $s(w)$ that behaves like $z$, and then
$$e(s(x),z)\Leftrightarrow e(s(x),s(w)) \Leftrightarrow e(x,w) \Leftrightarrow e(y,w) \Leftrightarrow e(s(y),s(w)) \Leftrightarrow e(s(y),z)$$
But now (1), (2), and (4) together with being an equivalence relation are exactly what is needed for $\approx$ to be a good equality relation. So without loss of generality we could have assumed that our logic does have a primitive $=$ symbol.
Furthermore it turns out that we necessarily have
$$e(x,y)\leftrightarrow x\approx y$$
The $\leftarrow$ direction is easy, since we already know that $e(x,x)$ directly by induction.
And we can prove $\forall y\bigl( e(x,y) \to x\approx y \bigr)$ by induction on $x$:
In the base case we need to prove $e(0,y)\to 0\approx y$. However, premise 4 says that $y$ cannot be a successor, so $0\approx y$ follows from (3) above.
For the recursion case assume $e(s(x),y)$. As in the argument for (4) above, there must be $w$ such that $s(w)\approx y$. But then $e(s(x),s(w))$ so premise 3 gives $e(s,w)$, and the induction hypothesis followed by (4) then gives us $s(x)\approx s(w)$ which is the same as $s(x)\approx y$, as required.
Since $e$ coincides with $\approx$ which is known to be an equivalence relation, it is in particular transitive.
A: [I tried but, as Henning Makholm noted, quite miserably failed to get a non-standard model of PA extended with $e$ where $e$ fails to be unrestrictedly transitive: but I'll leave this non-answer here to preserve his second comment in particular.]
