0
$\begingroup$

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.

enter image description 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.

$\endgroup$
15
  • 1
    $\begingroup$ @MauroALLEGRANZA I don't think it's a misprint; rather it's an infelicitous choice of words. What Shoenfield really means is that $e_1$ and $e_2$ are compatible if and only if there exist expressions $e_3$ and $e_4$ such that $e_1e_3$ is the same as $e_2e_4$. $\endgroup$ – Fabio Somenzi Jan 19 '17 at 7:20
  • 1
    $\begingroup$ The proof is a double induction : on $n$ and "inside" it on the index $k$ of each designator. $\endgroup$ – Mauro ALLEGRANZA Jan 19 '17 at 7:27
  • 1
    $\begingroup$ Maybe try "unique readability" as a search term. $\endgroup$ – bof Jan 19 '17 at 7:28
  • 1
    $\begingroup$ You can see into Heinz-Dieter Ebbinghaus & Jörg Flum & Wolfgang Thomas, Mathematical logic (2nd ed 1994) the "calculus of terms", Lemma 4.2 and Lemma 4.3, page 21. $\endgroup$ – Mauro ALLEGRANZA Jan 19 '17 at 7:34
  • 1
    $\begingroup$ In a nutshell, it is a "convoluted" version of the unique readibility property: if you start from $u_1$ and $u'_1$ (outer induction on $n$) and you consider their lenght $k$ (inner induction) for $k=1$ then they must be variables. To say that they are compatible means that they are both one-character expressions such that one can be obtained from the other adding some expression to the right: this can be only the empty string, and thus the two variables must be the same. $\endgroup$ – Mauro ALLEGRANZA Jan 19 '17 at 7:49
3
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Your "preoccupied" remark made me laugh. I think there is pedagogical value in establishing unique readability, but I prefer an algorithmic proof with a top-down structural induction. =) $\endgroup$ – user21820 Jan 20 '17 at 16:41
  • 1
    $\begingroup$ Yes, there is pedagogical value, as in writing an actual program for a Turing machine. I'd also go for structural induction. It's perhaps a sign of the times that Shoenfield explicitly comments on the simplicity of induction on the length of the expression. Finally, I'm glad I put a smile on your face. $\endgroup$ – Fabio Somenzi Jan 20 '17 at 17:53

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.