$v_2$ is not substitutable for $v_1$ in $\forall \,v_1\,\forall\,v_2\,Bv_1v_2\to\forall v_2 Bv_2v_2$

65 Views Asked by At

Definitions: Let $\alpha$ be a formula, $x$ be a variable and $t$ be a term. We say that $t$ is substitutable for $x$ in $\alpha$ as follows:

$(1)$ For atomic $\alpha, t$ is always substitutable for $x$ in $\alpha.$

$(2)$ $t$ is substitutable for $x$ in $(\neg \alpha)$ iff $t$ is substitutable for $x$ in $\alpha.$

$t$ is substitutable for $x$ in $(\alpha\to\beta)$ iff $t$ is substitutable for $x$ in both $\alpha$ and $\beta.$

$t$ is substitutable for $x$ in $\forall y\,\alpha$ if and only if either

(a) $x$ does not occur free in $\forall y\,\alpha,$ or

(b) $y$ does not occur in $t$ and $t$ is substitutable for $x$ in $\alpha.$

We say that $x$ occurs free in $\forall v_i\,\alpha$ if and only if $x$ occurs free in $\alpha$ and $x\neq v_i.$

Axiom group $2$ contains formula of the form $$\forall x\,\alpha\to\alpha^x_t$$ where $t$ is substitutable for $x$ in $\alpha.$

I am reading Enderton's logic book and have reached substitutability. The author stated the following:

$$\forall \,v_1\,\forall\,v_2\,Bv_1v_2\to\forall v_2 Bv_2v_2$$ is not in axiom group $2,$ since $v_2$ is not substitutable for $v_1$ in $\forall\, v_2 Bv_1v_2.$

However, I could not reach the same conclusion as the author. The following is my verification.

We let $$x=v_1, \alpha=\forall v_2\,Bv_1v_2, t=v_2.$$

$v_1$ does not occur free in $\forall v_1\,\alpha$ since $v_1$ has a quantifier attached to it. So $v_2$ is substitutable for $v_1$ in $$\forall \,v_1\,\forall\,v_2\,Bv_1v_2\to\forall v_2 Bv_2v_2.$$

What's wrong with my verification?

1

There are 1 best solutions below

2
On

In your example let $\alpha=Bv_1v_2$, $t=v_2$ and $x=v_1$ and apply your definition.
$t$ is not sustitutable for $x$ in $\forall t Bxt$ because of part $a)$ of your definition, i.e $x$ is free in $\forall t Bxt$

EDIT: let now $$x=v_1, \alpha=\forall v_2\,Bv_1v_2, t=v_2.$$ as you did before. Whe're trying to prove that $t$ is sustitutable for $x$ in $\alpha$.

Condition $a)$ is satisfied as you verified, but condition $b)$ is not because of the first part of this post, i.e $v_2$ is not sustitutable for $v_1$ in $\forall v_2\,Bv_1v_2$