Replacement of terms and formulas

Question

I'm trying to study mathematical logic with J.R.Shoenfield's Mathematical Logic.

Section 3.4 starts with the Equivalence Theorem, which states the following ($A, B, ...$ denote formulas of a first order language).

Let $A'$ be obtained from $A$ by replacing some occurrences of $B_1, ..., B_n$ by $B_1', ..., B_n'$ respectively. If $\vdash B_1\leftrightarrow B_1', ..., \vdash B_n\leftrightarrow B_n'$, then $\vdash A\leftrightarrow A'$.

My question is how exactly do we replace $B_1, ..., B_n$ by $B_1', ..., B_n'$? I believe that from the occurrence theorem $B_i$ and $B_j$ are either distinct or one is a part of the other. I'm interested in the latter case. The proof seems to work for any reasonable way of defining the replacement but then the theorem states very different things for each such way; or is that intended?

I have the same question about replacing terms by terms inside of terms and formulas.

Answer 1

I think I see what you mean:

If $A$ is $(\phi_1 \land \phi_2) \to \phi_3$, and we have $\vdash (\phi_1 \land \phi_2) \leftrightarrow \phi_4$ and $\vdash \phi_1 \leftrightarrow \phi_5$, then what is the result of the 'replacing'?

Once we replace $\phi_1 \land \phi_2$ with $\phi_4$, we are left with $\phi_4 \to \phi_3$, and so we can no longer apply the $\vdash \phi_1 \leftrightarrow \phi_5$ equivalence.

On the other hand, if we start with the latter equivalence, we end up with $(\phi_5 \land \phi_2) \to \phi_3$, and now we can't apply the first equivalence. That is, the replacements are 'interfering' with each other.

So, is $A'$ supposed to be $\phi_4 \to \phi_3$ or $(\phi_5 \land \phi_2) \to \phi_3$? It doesn't seem well-defined.

I think the key is that the book says 'some':

Let $A'$ be obtained from $A$ by replacing some occurrences of $B_1, ..., B_n$ by $B_1', ..., B_n'$ respectively. if $\vdash B_1\leftrightarrow B_1', ..., \vdash B_n\leftrightarrow B_n'$, then $\vdash A\leftrightarrow A'$.

That is, the book does not force every replacement to take place, even if more can take place. As such, $A'$ is not the unique result of making any such replacements, but can be one of many. For example, even if $A$ is $(\phi_1 \land \phi_2) \to \phi_1$, and we have $\vdash \phi_1 \leftrightarrow \phi_3$ and $\vdash \phi_2 \leftrightarrow \phi_4$ (so we can apply all equivalences without any 'interference') then $A'$ can still be one of many possible outcomes:

$(\phi_3 \land \phi_4) \to \phi_3$

or

$(\phi_3 \land \phi_2) \to \phi_3$

or

$(\phi_3 \land \phi_4) \to \phi_1$

or

$(\phi_3 \land \phi_2) \to \phi_1$

or

$(\phi_1 \land \phi_4) \to \phi_3$

or

$(\phi_1 \land \phi_2) \to \phi_3$

or

$(\phi_1 \land \phi_4) \to \phi_1$

or even simply the original

$(\phi_1 \land \phi_2) \to \phi_1$

However, whichever one you take, they are all equivalent to the original.

With that, I don't think there is any issue here. But, I will say that the theorem could have avoided any confusion by simply doing:

Let $A'$ be obtained from $A$ by replacing some occurrences of $B$ by $B'$ respectively. if $\vdash B\leftrightarrow B'$, then $\vdash A\leftrightarrow A'$.

This, of course has the same effect, since if you want to apply other equivalences, you can just reapply this theorem.