I am trying to understand the following proof intuitively which I am providing from Joseph R. Shoenfield’s Mathematical Logic, page 15,verbatim. If you wish to consult the book there is an link here.
There are two criteria in the definition of compatibility:
$(i)$ If uv and u'v' are compatible, then u and u' are compatible.
$(ii)$ If uv and uv' are compatible, then v and v' are compatible.
Here is what I was thinking so far:
For example, let $\mathbf u_1$ be $fx_1 , ... ,x_n$, $\mathbf u_2$ be $\mathbf 0$, $\mathbf u_3$ be + , ..., and $\mathbf u_n$ is $\mathbf <$.
We rewrite $\mathbf u_1$ as the function $fx_1 , ... ,x_n$, but the second sentence in the proof says $\mathbf u'_1$ begins with $f$ as well (or as in the proof above with $\mathbf v$) but why is this so?
Is this the repeated use of criterion $(i)$? That is, using criterion $(i)$ repeatedly we show $\mathbf u'_{1}$ is compatible with $\mathbf u_1$ when we remove designators, $\mathbf u_j$ and $\mathbf u'_j$ (starting from the end) from $\mathbf{u_1,...,u_n}$ and $\mathbf{u'_1,...,u'_n}$ respectively. And we then do the same for the terms(components) in each $\mathbf u_1$ and $\mathbf u'_1$ i.e. in our example each $x_i$ is compatible with $x'_i$ of $f$. But what if each $x_i$ and $x'_i$ are dependent on further terms? Wouldn't we need to use criteria $(i)$ on $x_i$ and $x'_i$ until our terms are just individual variables?
The proof in the book seems to assume that the desginators $\mathbf {v_1,...,v_k}$ are not be further dependent on other terms. Or am I completely misunderstanding this??
Thanks in advance!! I really appreciate this site.
Let's first of all set some context. Shoenfield is preoccupied with establishing unique parsing (or readability, as aptly pointed out by @bof) of first-order languages. He uses Polish (prefix) notation for both terms and formulae, which allows him to give a unified treatment. (Unlike, for instance, Enderton, who is another author preoccupied with unique parsing.)
So, designator is the term that may refer indifferently to a term or a formula. If we have a sequence of designators, we want to show that there is no ambiguity in their parsing, even though there is no syntactical demarcation of where one ends and the next begins.
Designators, however, are "complete" entities. A designator cannot be just $+$, if indeed $+$ is a binary function symbol. Instead, $+xy$ is a valid designator, if $x$ and $y$ are variables. In general, if $f$ is a symbol of arity $k$ that starts a designator, it must be followed by $k$ designators. As another example, $>fxfy$ is a designator if $>$ is a binary relation symbol, $f$ is a unary function symbol, and $x$ and $y$ are variables.
Now Lemma 1 shows that two (syntactically correct) sequences of designators that result in the same sequence of symbols can only be obtained by concatenating the same designators in the same order.
As a preliminary to the actual proof, observe that two designators that start with different symbols are definitely incompatible. If one starts with $f$ and the other starts with $g$, there's nothing we can append to make the two designators the same.
This simple observation allows us to apply induction, because we are given that $u_1 = vv_1\cdots v_k$ and $u_1' = vv_1'\cdots v_k'$ are compatible and besides $v_1\cdots v_k$ is shorter than $u_1$. (Why are $u_1$ and $u_1'$ compatible? Because their extensions $u_1\cdots u_n$ and $u_1'\cdots u_n'$ are. Why are the $v_i$ and the $v_i'$ in the same number? Because $k$ is the arity of $v$ which is common to $u_1$ and $u_1'$.)
So, we apply the inductive hypothesis to $v_1\cdots v_k$ and $v_1'\cdots v_k'$ to prove that $u_1$ is parsed the same as $u_1'$. This means, thanks to the second property of compatibility, that $u_2\cdots u_n$ is compatible to $u_2'\cdots u_n'$. Both are shorter than the two original sequences, which allows us to again invoke the inductive hypothesis to argue that they have a unique parsing and thus finish the proof.