Clever Substitution Notation for Logic Formulae

Question

Assume I have a first order- ($\mathsf{FO}$-) formula $ \varphi(x)$ with free variable $x$ and bounded variables $x',x''$. Then, $\varphi(x) \in \mathsf{FO}^3$ since it has $3$ distinct variables.

Furthermore, assume there is a situation such that we want to call that formula $\varphi$ with parameter $x'$ instead of $x$. Writing $\varphi(x')$ does not work because there is a name clash between the parameter $x'$ and the bounded variable $x'$. Hence, we have to replace the bounded variable $x'$ with $x$ and then write $\varphi(x')$. Of course we could use another variable like $y$ but we want to use as few variables as possible. How do write something like this?

$$ \varphi(x')[x' \leftarrow x]$$

This does not really make sense since we would replace both the parameter $x$ and the bounded variable $x$. Is there any standard notation for my situation? The idea is really simple and I don't want the notation to be too bloated.

Answer 1

I think that there is no "compact" formalization of the required double substitution.

Assuming that [using $v_0, v_1, v_2$] :

$\varphi (v_1) := \forall v_0 \psi(v_0, v_1)$

we have :

$\forall v_0 \psi(v_0, v_1)[v_0 ← v_2] \equiv \forall v_2 \psi(v_2, v_1)$

with $v_2$ a new variable. This condition licences us to prove the equivalence.

Now we can perform the second substitution :

$\varphi (v_0) := \forall v_2 \psi(v_2, v_1)[v_1 ← v_0]$.

But, in general :

$\varphi(v_1) \nvdash \varphi(v_0)$.

---

We can try with the approach to substitution in John Bell & Moshe Machover, A Course in Mathematical Logic (1977), page 57-on.

The "syntax" for substitution is : $\alpha(x,t)$ and the basic defintion is Definition 3.3 [page 59] :

We shall say that $t$ is free to be substituted for $x$ in $\alpha$ (briefly, free for $x$ in $\alpha$) if no free occurrence of $x$ in $\alpha$ is within a subformula of $\alpha$ having the form $\forall y \beta$ where $y$ occurs in $t$.

If $t$ is free for $x$ in $\alpha$, we shall define $\alpha(x/t)$ as the result of substituting an occurrence of $t$ for each free occurrence of $x$ in $\alpha$.

Definition 3.5 [page 61]. If $z$ is a variable which is not free in $\beta$ but is free for $x$ in $\beta$, we say that $\forall z [\beta(x/z)]$ arises from $\forall x \beta$ by (correct) alphabetic change. (Note that if $z$ does not occur at all in $\beta$, then $z$ certainly satisfies both of the above conditions.)

Thus, considering again the formula :

$\varphi := \forall v_0 \psi(v_0, v_1, v_2)$

we perform an alphabetic change using $v_n$, where $v_n$ is the first variable not occurring in $\varphi$, getting :

$\forall v_n [\psi(v_0/v_n, v_1, v_2)]$

and then the substitution : $v_1 ← v_0$ (now $v_0$ is free for $v_1$ in the formula), to get :

$\forall v_n [\psi(v_0/v_n, v_1/v_0, v_2)]$.

The result will be :

$\varphi' := \forall v_n \psi(v_n, v_0, v_2)$.

Answer 2

We want to call the above mentoided formula $\varphi(x)$ with $x'$. Therefore, we transform it into an equivalent formula $\varphi'$.

$$ \varphi'(x') :=\exists x ( x=x' \land \varphi (x) )$$