What is "induction on complexity of formula"

Question

The fundamental theorem of ultraproducts

Given a language $L$ and a family of models $M_i$ of $L$ and ultrafilter $\mathcal U$ on $I$ and $\varphi$ a formula of $L$ then $$ \prod_{i \in I}A_i/\mathcal U \models \varphi(s_0/_{\mathcal U}, \dots, s_n/_{\mathcal U}) \iff \{i \in I : \varphi (s_0(i), \dots, s_n (i))\}\in \mathcal U$$

Is proved by induction on the complexity of $\varphi$. I expect the proof to do atomic formula case first. Atomic formula is formula of form $\varphi = (t_1 = t_2)$ or of form $\varphi = R(t_1, \dots , t_n)$ where $t_i$ are term. But the proofs for example this prove something about terms not atomic formula. Can someone explain me please what is it we need to show if not atomic formula case first? Why terms?

Answer 1

The construction of terms usually proceeds through the following recursive definition:

• Any variable $x$ is a term;
• Any constant $c$ is a term;
• For an $n$-ary function symbol $f$ and terms $t_1,\ldots, t_n$, $f(t_1,\ldots,t_n)$ is a term.

(Some texts define constants as nullary function symbols, but this does not guarantee that this special case does not require special attention -- i.e. it is not trivial that the induction proof for function symbols of positive arity carries over to nullary function symbols.)

---

So in order to prove a statement $P(t)$ about terms $t$ by induction on the complexity, one needs to verify that each of these constructions is suitably well-behaved with regard to the formation rules.

That is, we need to verify that $P(x), P(c)$ for $x$ a variable, $c$ a constant, and that $P(t_1),\ldots, P(t_n)$ imply $P(f(t_1,\ldots,t_n))$.

Now why would we want to have such statements $P$? Well, a useful example of a statement $P$ about terms could be verifying your initial statement for the case $\varphi = (t_1 = t_2)$!

---

In conclusion, proving something about terms is entirely different from proving something for formulae. Therefore, they call for different approaches, and as such require a different basis for their "structural induction".

Answer 2

Sometimes, when doing induction on the complexity of formulae, you need to do some sort of induction on the complexity of terms first in order to prove your basis cases for the induction on the complexity of formulae. That's what Chang & Keisler, the book you referenced, do. Their theorem has parts (i), (ii), and (iii); part (i) is just a statement about terms, proven by induction on the complexity of terms, and part (ii) is the part you're concerned about, which is proven by induction on the complexity of formulae using part (i) to get the basis case rolling. So you are doing the atomic case first, but it's just that in order to do the atomic case, you need a separate argument, which happens to be an argument via induction on the complexity of terms.