Exercise 5.4.7 on page 127 of Chiswell and Hodges "Mathematical Logic" is:
Let $\sigma$ be a signature, $r$ a term of qf LR($\sigma$), $y$ a variable and $\phi$ a formula of qf LR($\sigma$). Let $D$ be a qf $\sigma$-derivation, and write $D^{\prime}$ for the diagram got from $D$ by replacing each occurrence of the formula $\phi$ in $D$ by $\phi[r/y]$. Show that $D^{\prime}$ is also a qf $\sigma$-derivation.
The book defines LR as a "language of relations". A formula of qf LR($\sigma$) is a formula in which quantifier symbols do not appear ("quantifier free"). A $\sigma$-derivation is defined as a tree structure that satisfies the logic rules for LR($\sigma$) (definion 5.4.5 on page 125).
I interpret the question above as follows. We "fix" the signature $\sigma$, term $r$, variable $y$, and formula $\phi$ first. Then, we are given a $\sigma$-derivation $D$. For each node in $D$, we replace occurrences of the formula $\phi$ that appear as sub-formula within the left label of the node (the left label of a derivation node is a formula, the right label is the name of the rule used to derive the formula in the left label) with the formula $\phi[r/y]$. We want to show that the tree that results from this process is a qf $\sigma$-derivation.
After struggling to prove the result, I looked at the solution on page 239-240. The solution only describes the proof for one part of the $\sigma$-derivation (the $\sigma$-derivation requirements of a node that has two daughters and right label "=E"), but it appears to be describing a proof for a problem where the formula $\phi$ is not fixed. For clarity, this is the proposition that I think the solution is proving:
Let $\sigma$ be a signature, $r$ a term of qf LR($\sigma$), $y$ a variable. Let $D$ be a qf $\sigma$-derivation, and write $D^{\prime}$ for the diagram got from $D$ by substituting the term $r$ for the variable $y$ in the formula of each left label in $D$ (i.e. for each formula $\phi$ that appears as a left label in a node of $D$, replace the left label with $\phi[r/y]$). Show that $D^{\prime}$ is also a qf $\sigma$-derivation.
I concluded this because the solution proves that, given some node $\nu$ with formula $\psi$ as its left label, the formula $\psi[r/y]$ satisfies the requirements for that type of node (a "=E" node). It doesn't delve into any reasoning about whether some pre-existing formula $\phi$ is equal to $\psi$, not equal to $\psi$, or is a sub-formula of $\psi$, which I expect would be required if $\phi$ were fixed before the derivation $D$ was considered. (Note: my description of the solution is a rough summary based on my understanding of it, refer to page 239 of the book for the details.)
My questions:
Is the wording of this exercise clear?
Is there a better wording that might help me understand it better?
If you are familiar with the book, does it appear that the solution is proving something that is not the same as the problem defined in the exercise? Or, if the wording of the exercise is fine, and the solution is correct, can you help me understand why the solution only deals with substituting $r$ for $y$ and doesn't deal with contents of the formula $\phi$?
EDIT: response to Mauro's question (What do you mean with "the contents of the formula $\phi$ ?):
I don't understand how the proof for case (=E) could be correct: to quote from the solution,
The formulas at the corresponding nodes in $D^{\prime}$ are $\phi[t/x]^{\prime}$ at $\nu$ and $\phi[s/x]^{\prime}$ and $(s = t)^{\prime}$ at its daughters.
where the solution defines the prime notation by stating
we write $t^{\prime}$ for $t[r/y]$ and $\phi^{\prime}$ for $\phi[r/y]$.
This is my confusion with the solution: the corresponding nodes of $D^{\prime}$ should only be modified ($r$ substituted for $y$) at places where the formula $\phi$ (fixed before we modified a derivation D) occurs in the left label. So why does the solution assume that the left label of BOTH $\nu$ AND its daughters are modified such that $r$ is substituted for $y$? Shouldn't the "contents"/"form"/"parse tree" of the $\phi$ have to match the left label of a node for the formula to be modified?
Maybe I understand it now...
Your concern is right: what the exercise proves is something like:
i.e. every occurrence of formulae $\phi$ must be replaced with $\phi[r/y]$.
At node $\nu$ of the corresponding tree, we have the left leaf $ϕ[t/x]$ and we have to replace it with $ϕ[t/x]′$. But it may be the case that $y$ occurr also inside $t$, and thus the replacement acts also on the "part" of $ϕ[t/x]$ where that occurrence of $y$ is "imported" by $t$. This is way we have to consider also $(s=t)′$.
Consider this silly derivation $D$ in the qf language of arithmetic:
1) $z=y$ --- is: $s=t$
2) $z=S(0)$ --- is: $\phi[s/x]$, where $\phi$ is: $x=S(0)$
3) $y=S(0)$ --- is: $\phi[t/x]$; from 1) and 2) by (=E).
Now we want to build $D'$ with $S(x)$ as $r$, replacing each occurrence of the formula $y$ in $D$ by $r$.
The "receipe" is:
Thus, working upside-down, we have the new tree:
3') $S(x)=S(0)$ --- this is: $ϕ[t/x]′$
2') $z=S(0)$ --- this is: $ϕ[s/x]′$
1') $z=S(x)$ --- this is: $(s=t)′=(s'=t')$.
If, as you noted, we do not apply the substitution of $r$ in place of $y$ to the leaf $(s=t)$, what we get is a wrong derivation:
3'') $S(x)=S(0)$ --- this is: $ϕ[t/x]′$
2') $z=S(0)$ --- this is: $ϕ[s/x]′$
1') $z=y$ --- this is: $(s=t)$.