3
$\begingroup$

I am having difficulty with the concept of $LK-\Phi$ proofs, here is a question I have been working on:

Let $\Phi = \{Pafa\}$, where $P$ is a binary predicate symbol and $f$ is a unary function symbol. Give an $LK-\Phi$ proof of $\exists y Pby$. You do not need to show exchanges and weakenings.

My intution for these questions is very little unless it is blatantly obvious over what to do, but I do know that in the system $LK$ we have a $LK-\Phi$ proof if we have $A\to A$ or $\to A$ where $A\in\Phi$. So in this situation I think I set this up as the following:

$$\to \exists y Pby$$and then I would have a sequent above it where I would apply the $\exists R$ rule, which would create the sequent above as: $$\to Pba$$ but from here I am not sure at all what to do whether I need to rely on some sort of trick or anything? Any help would be greatly greatly appreciated, this is for an exam I am studying.

$\endgroup$
  • $\begingroup$ What are $a,b$? Free variables? Atoms? $\endgroup$ – Yuval Filmus Apr 24 '14 at 13:59
  • $\begingroup$ I am going to assume free variables. $\endgroup$ – InsigMath Apr 24 '14 at 14:06
3
$\begingroup$

First of all, let me recommend then you use parentheses. So $\Phi = \{P(a,f(a))\}$, and you're trying to derive $\exists y P(b,y)$ from this.

If it were $\exists y P(a,y)$ instead, the proof would be very simple. You start by using the $\Phi$-rule to deduce $\vdash P(a,f(a))$, and then using the $\exists R$ rule you deduce $\vdash \exists y P(a,y)$.

As it stands, you cannot deduce $\exists y P(b,y)$ from $\Phi$ since $\exists y P(b,y)$ is not logically entailed from $\Phi$. For example, consider the interpretation in which $f$ is the identity and $P(x,y)$ is true only if $x=y=a$. Then $\Phi$ holds but $\exists y P(b,y)$ is false. Since LK-$\Phi$ is sound, you cannot deduce $\exists y P(b,y)$ from $\Phi$.

$\endgroup$
  • $\begingroup$ I might be a little slow ... are you saying that this question is impossible? $\endgroup$ – InsigMath Apr 24 '14 at 14:06
  • 1
    $\begingroup$ That's right. Assuming LK-$\Phi$ is sound, you can only prove valid statements, and what you are trying to prove isn't valid. It's probably a typo. $\endgroup$ – Yuval Filmus Apr 24 '14 at 15:26

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.