I have a proof to the following lemma, and some general questions about the technique.
A real initial part of a $L$-term is not a $L$-term.
Definition of $L$-term:
Let $L$ be a language and $v_0, v_1,\dotso$ a sequence of variables. An $L$-term is a sequence of symbols which is formed by the following rules:
(1) Every variable is an $L$-term.
(2) Every constant symbol is an $L$-term.
(3) If $f$ is an $n$-digit function symbol and $t_1,\dotso, t_n$ are $L$-terms, then $f(t_1,\dotso, t_n)$ is an $L$-term.
Now for the proof:
Let $s,t$ be $L$-terms and $s$ an (real) initial part of $t$.
The proof is done by induction over $|t|$.
Induction beginning:
If $|t|=1$ then $|s|\in\{0,1\}$, but $|s|\neq 0$ because $s$ is a real initial part of $t$. So $|s|=1$ and thus $s=t$.
Inductive step:
$t$ has the form $f(t_1,\dotso, t_n)$. Then is $s=f(s_1,\dotso, s_n)$.
We have to show: $s_1=t_1,\dotso, s_n=t_n$.
Suppose this does not hold, then $s_1=t_1,\dotso, s_n=t_n$ and $s_{k+1}\neq t_{k+1}$ for $k<n$.
Then either $s_{k+1}$ is an initial part of $t_{k+1}$, or $t_{k+1}$ is an initial part of $s_{k+1}$.
This is a contradiction to the inductive assumption, that an inital part of an $L$-term is not an $L$-term, since $|s_{k+1}|, |t_{k+1}|<|t|$.
_
Now I wonder how much induction is in this proof, compared to other inductive proofs, because as it seems we do not show in the inductive step, that if the claim holds for $n$ it does so for $n+1$.
I feel like it reads a little off in comparision to other inductive proofs, and more like a 'seperation of cases'. Also there is only one other instance were I saw a proof by induction combined with a contradiction, but that does not matter here.
The inductive beginning cancels out the form (1) and (2) in the definition, and the inductive step cancels out (3).
So is this induction any different from 'normal' induction?
Thanks in advance.
This is a "normal" proof by induction, though it isn't (at least, as written) a proof by induction where the indexing set is $\mathbb{N}$. Induction is significantly more general than just along $\mathbb{N}$, it can be done on any well-founded relation (https://en.wikipedia.org/wiki/Well-founded_relation#Induction_and_recursion).
There is a way to make the proof you've got here look more like the induction proofs you've seen before. Formally, it is to do induction on a rank function for your recursive definition. It sounds to me like an informal description might be more useful than all the technical details, so that's what I'll write here.
You can think of the terms as being formed in "stages", with clauses (1) and (2) telling you what happened at "stage $0$", and clause (3) telling you that at "stage $n$" you go to "stage $n+1$" by taking terms $t_1, \ldots, t_k$ that you've already created, and forming $f(t_1, \ldots, t_k)$. In this way, the proof that you've written is a proof by induction on the "stage of formation" of the term. If $\vert t \vert = 1$ then we are at "stage 0", so we need to take care of clauses (1) and (2). If $\vert t \vert > 1$ then we are at some "stage $n+1$", so we know (by the recursive definition) that our term has the form $f(t_1, \ldots, t_k)$ for some terms $t_1, \ldots, t_k$, all of which already had been formed at "stage $n$". We can then apply the induction hypothesis to each of $t_1, \ldots, t_k$.