I think some of the commenters were confused by the notation $\Gamma \vdash A \downarrow B$, which I have only seen written as $\Gamma [ A ] \vdash B$ or $\Gamma \vdash A > B$. The latter is closest to the notation you were using.
First, you're missing at least one necessary rule, and arguably you're missing three; I would write the full system as follows:
$${A \in \Gamma \quad \Gamma \vdash A > P \over \Gamma \vdash P}{\it focus} \qquad {{} \over \Gamma \vdash P > P}{\it init}$$
$${\Gamma, A \vdash B \over \Gamma \vdash A \supset B}{{\supset}R} \qquad {\Gamma \vdash A \qquad \Gamma \vdash B > P \over \Gamma \vdash A \supset B > P}{{\supset}L}$$
$${\Gamma \vdash A(\alpha) \over \Gamma \vdash \forall x.A(x)}{{\forall}R^\alpha} \qquad {\Gamma \vdash A(t) > P \over \Gamma \vdash \forall x. A (x) > P}{{\forall}L}$$
Assuming this fits with your understanding, then the proof you describe is simple: it is provable simply by case analysis and the observation that the rule $\it focus$ is the only rule that is applicable. Without the $\it focus$ rule, the caculus as you describe it cannot possibly be complete with respect to minimal first-order logic.
The original reference for what I think you're trying to do here is:
Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125-157, 1991