2
$\begingroup$

There is signature $\sigma = \left \langle P^{2} \right \rangle$ , P - predicate, t - term signature $\sigma$.

I need to prove that the rule $\frac{\Gamma ,\Phi (t))\vdash \Psi }{\Gamma , \forall x \Phi (x))\vdash \Psi }$ is not a valid rule. It means its addition to the predicate calculus can extend the set of provable sequents. Also I understend This rule is not deducible, so we can find a algebraic system of our signature where it doesn't work.

I have some problems, because it doesn't looks like not valid. I qlearly know that there is such rule $ \frac{\Gamma ,\Phi (x)_{t}^{x})\vdash \Psi }{\Gamma , \forall x \Phi (x))\vdash \Psi } $. Also our signature has only one predicate symbol, so t can be only variable. So if $\Phi (x)$ true $\forall x$ then it true for a special one.

$\endgroup$
  • $\begingroup$ If you look closely at the rule you quoted, you'll probably find some restriction intended to prevent variables from becoming accidentally quantified when you substitute $t$ for $x$. (The relevant terminology might be "substitutable" or "free for" or freely substitutable", depending on the author's taste.) Try to concoct a situation where that restriction is violated; see whether you can arrange it so that the resulting rule isn't sound. $\endgroup$ – Andreas Blass Dec 25 '17 at 1:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.