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.
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$.