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

Question

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.

Answer 1

We have that $LK_Φ$ is the system obtained from $LK$ by adding $→A$ as initial sequents, for all $A \in Φ$.

Let $Φ = \{ Pafa \}$.

We have to start with the sequent :

$→P(a,fa)$ (with $\Gamma = \Delta = \emptyset$)

and then apply ∃-right (with $fa$ as the term $t$ of the rule) to obtain the sequent :

$→∃yP(a,y)$.

Then we apply the Substitution lemma [see Sara Negri & Jan von Plato, Structural Proof Theory (2001), page 68] :

if $\Gamma \rightarrow C$ is derivable and $t$ is free for $x$ in $\Gamma, C$, then $\Gamma[t/x] \rightarrow C[t/x]$ is derivable.

We apply it to the end-sequent above, with $\Gamma = \emptyset$, $b$ as $t$ and $∃yP(a,y)$ as $C$; thus $C[t/x]$ is $∃yP(a,y)[b/a]=∃yP(b,y)$ to conclude :

$→∃yP(b,y)$.