LK-$\phi$ proof of $\exists y Pby$

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.

• What are $a,b$? Free variables? Atoms? Apr 24, 2014 at 13:59
• I am going to assume free variables. Apr 24, 2014 at 14:06

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$.
• 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. Apr 24, 2014 at 15:26