1. ## pridicate calculus

In a predicate calculus book there is an axiom that states:

$\displaystyle \forall vP\Longrightarrow P(t/v)$ provided P admits t for v

in other words the implication holds if we can substitute v for t.

Can anybody give an explanation ,please, with an example??

Thank you

2. Hi

If it's what I think, $\displaystyle \forall vP\Rightarrow P[t/v]$ is an axiom iff no occurence of $\displaystyle v$ in $\displaystyle P$ lies within the scope of a quantifier binding a variable of $\displaystyle t$ (which is free since it's a term)

This restriction is essential to avoid situations like:

$\displaystyle \forall v\exists x(\neg x=v)\Rightarrow \exists x(\neg x=x)$

which would be an axiom without the restriction, with $\displaystyle P= \exists x(\neg x=v)$ and $\displaystyle t=x$, while you easily see it is wrong whenever you consider a model with at least two elements.

3. THANK you .

I agree with you.

But then how would you explain the following UNIVERSAL ELLIMINATION rule given in another logic book:

From a universally quantified wff (= well formed formula ) $\displaystyle \forall\beta\phi$ we may infer any wff of the form $\displaystyle \phi\alpha/\beta$ which results from replacing each occurrence of the variable β in φ by some name letter α

Ιs it right or wrong??

4. I guess you stay in the same formal system, so you can still use the axiom.

Let $\displaystyle \forall x_n...\forall x_1 F[x_n,...,x_1]$ be a universal formula, i.e. $\displaystyle F$ is quantifier free. We can assume $\displaystyle x_i\neq x_j if i\neq j$.

If $\displaystyle n=1,$ then $\displaystyle x_1$ has only free occurences in $\displaystyle F[x_1],$ therefore you can apply the axiom: $\displaystyle \forall x_1F\Rightarrow F[\beta_1 /x_1].$

Assume $\displaystyle \forall x_{n-1}...\forall x_1F\Rightarrow F[\beta_{n-1}/x_{n-1},...,\beta_1/x_1].$ Since $\displaystyle x_n$ has only free occurences in $\displaystyle \forall x_{n-1}...\forall x_1F,$ we can once again use the axiom, and get what we wanted.

5. Originally Posted by xalk
THANK you .

I agree with you.

But then how would you explain the following UNIVERSAL ELLIMINATION rule given in another logic book:

From a universally quantified wff (= well formed formula ) $\displaystyle \forall\beta\phi$ we may infer any wff of the form $\displaystyle \phi\alpha/\beta$ which results from replacing each occurrence of the variable β in φ by some name letter α

Ιs it right or wrong??
It's somewhat restrictive, but certainly not wrong.
Note, the author refers specifically to "name letter".
By name, she surely means designator. That's a closed term.
The so-called "non-capture" restriction applies only to open terms.

6. The UNIVERSAL ELIMINATION in the 1st book appears as the following theorem :

From $\displaystyle \forall v.P$ we can infer P(t/v) PROVIDED that P admits t for v ,using in the derivation of the theorem :

1) The axiom : $\displaystyle \forall vP\Longrightarrow P(t/v)$,provided P admits t for v.
2) M.Ponens.

The UNIVERSAL ELIMINATION in the 2nd book that appears in the post #3 ,
does not have the restriction that the 1st book has .

That is why i was wondering if the rule is right