Understanding Structural Induction

Question

I have a problem with the intuition behind structural induction. We didn't define it rigorously in my lecture and I don't get the concept yet. The concrete example of what I don't understand is proving that for terms $r$,$s$ and a free variable u, the 'thing' that results when I replace $u$ in $r$ by $s$, in our notation $r[s/u]$, is a term itself. I can do the formal proof by using structural induction, but this is only by applying a formal procedure that I don't have an intuition for yet.

1. if $r$ is a free variable, then r[s/u]=r or r[s/u]=s, and consequently a term (by definition)

2. if $r=f(t_1,...,t_n)$, where f is a function symbol of ${n\in\mathbb{N}}$ variables, and $t_1,...,t_n$ are terms, then $r[s/u]=f(t_1[s/u],...,t_n[s/u])$ by definition. Since $t_1,...,t_n$ are terms, the induction hypothesis provides that $t_1[s/u],...,t_n[s/u]$ are terms as well. Then by definition $f(t_1[s/u],...,t_n[s/u])$ is a term.

Now in the second step we say that $t_1,...,t_n$ are terms. I looked up the formal definition of structural induction and it says that it only applies for 'objects produced in finitely many steps'. Alright, I get this one. One can consider each $t_i$ separately using 1. or 2. and after finitely many steps arrives at the basic notion of free variable or constant, so 1. proves the claim. But how do we now beforehand that the object we consider was formed in finitely many steps? Why can't there be something like $f(t_1)$, where $t_1$ itself is of the form $f(t_2)$, then $t_2$ of the form $f(t_3)$ and so on forever. Or in the other direction, I start with a constant $c$ and put $f(\cdot)$ around it infinitely many times. I assume both of these 'things' aren't defined/definable. But why?

This might seem trivial for some, but for me it's not intuitively clear. Maybe someone can provide me some insight.

Answer 1

The proof works because it "mimicks" the definition by recursion of terms.

A term is :

a variable or a constant : and thus case 1 applies,

or :

a string $f(t_1, \ldots, t_n)$, where $f$ is a function symbol and all the $t_i$s are already "produced" terms : and thus case 2 applies.

---

You cannot have an infinite descending "chain", simply because a term is a string of finite lenght, exactly as a description in human language : you can parse it in finite many words.

If e.g. we have a term $t=f(t_1)$ with $t_1=f'(t_2)$, for sure $t_2$ must be a string shorter than $t$.

Consider for example the f-o language of arithmetic; a well-formed term is :

$x+S(0)$

i.e. : $+(x,S(0))$.

The "procedure" is easy to understand if you consider the parsing-tree for a term; see : Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007), page 114.