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.

  • 1
    $\begingroup$ Structural induction is just another name for well-founded induction (a.k.a. Noetherian induction), that is, induction on well-founded structures. Given dependent choice, a well-founded relation amounts precisely to a relation that does not allow for countable infinite descending chains, if you proceed top-down. Contrapositively, for this very reason, every object constructed bottom-up by well-founded (structural) recursion must be constructed in finitely many steps. $\endgroup$ – J Marcos Oct 19 '15 at 22:44

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 :


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.

  • $\begingroup$ Thank you for your answer, but to be honest I still don't get it. Our definition of terms in the lecture was: 1. Variables and Constants are terms & 2. For a function symbol f with $n\in\mathbb{N}$ 'digits' and $t_1,...,t_n$ terms, $f(t_1,...,t_n)$ is a term. If I assume there is a term with infinitely many symbols, how do I lead this to a contradiction? I understand that structural induction makes sense for finite strings, but the definition doesn't say anything about that. If the definition was 'terms are strings of finite length formed by using 1. and 2., I could accept it, but it isn't. $\endgroup$ – azureai Oct 16 '15 at 15:08
  • $\begingroup$ @see - The "usual" math log textbooks does not allow for terms (or formulae) with infinitely many symbols. See Enderton, page 73 : "An expression is any finite sequence of symbols. [...] The set of terms is the set of expressions that can be built up from ...". $\endgroup$ – Mauro ALLEGRANZA Oct 16 '15 at 15:14
  • 1
    $\begingroup$ Of course, you have to check the details with your instructor. $\endgroup$ – Mauro ALLEGRANZA Oct 16 '15 at 15:30
  • $\begingroup$ Alright, if this is the canonical definition then I will just ask my instructor to clarify. Thank you very much. $\endgroup$ – azureai Oct 16 '15 at 16:10
  • $\begingroup$ @see - You can check it also in Heinz-Dieter Ebbinghaus & Jörg Flum & Wolfgang Thomas, Mathematical logic (2nd ed 1994) page 11 for the def of string as a "finite sequences of symbols from an alphabet $\mathcal A$", and page 15 for the def of term : "terms are precisely those strings in $\mathcal A$ which can be obtained by finitely many applications of the following rules: (1) Every variable is a term. (2) Every constant is a term. (3) If the strings $t_1, \ldots, t_n$ are terms and $f$ is an $n$-ary function symbol ... $\endgroup$ – Mauro ALLEGRANZA Oct 16 '15 at 19:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.