0
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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)$.

| cite | improve this answer | |
$\endgroup$
0
$\begingroup$

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) )$$

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Well done ! If, for example : $\varphi(x) := \exists x'(x = x'+x')$ [which means : $even(x)$], then $\varphi'(x') := ∃x(x=x′∧ \exists x'(x = x'+x'))$. But, frankly speaking, I do not see the gain ... $\endgroup$ – Mauro ALLEGRANZA Jul 28 '14 at 7:14

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.