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 downarrow comes, as you note in a comment, from Andreoli's notation, but that notation is more common in presentations of sequent calculi for classical logics, at least in my experience. The notation I'll use is the one with $>$ instead of $\downarrow$, which comes from Cervesato and Pfenning's "A Linear Spine Calculus."
Two proof systems
-----------------
So, to restate the goal, we have the following sequent calculus for first-order, minimal logic:
$$
{P \in \Gamma \over \Gamma \Rightarrow P}{\it init}
\qquad
{\Gamma, A \Rightarrow B \over \Gamma \Rightarrow A \supset B}{{\supset}R}
\qquad
{(A \supset B) \in \Gamma \qquad \Gamma \Rightarrow A \qquad \Gamma, B \Rightarrow C \over \Gamma \Rightarrow C}{{\supset}L}
$$
$$
{\Gamma \Rightarrow A(\alpha) \over \Gamma \Rightarrow \forall x.A(x)}{{\forall}R}
\qquad
{(\forall x.A(x)) \in \Gamma \qquad \Gamma, A(t) \Rightarrow C \over \Gamma \Rightarrow C}{{\forall}L}
$$
We want to relate this proof system to the following presentation of "focused" or "uniform" proofs. I would argue that in your presentation above, the description of uniform proofs is missing at least one necessary rule ($\it focus$) and arguably is missing three; I would write the full system of focused (a.k.a. uniform) proofs 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}$$
... where $A$ and $B$ represent arbitrary propositions and $P$ represents an atomic proposition.
Relationship between the proof systems
--------------------------------------
We, roughly speaking, expect the two proof systems to prove the same things. One direction of this is easy:
**Theorem 1 (Soundness of focusing)** - If $\Gamma \vdash A$, then $\Gamma \Rightarrow A$, and if $\Gamma \vdash A > C$, then $\Gamma, A \Rightarrow C$.
*Proof:* Straightforward induction on focused proofs (+ weakening for the unfocused proofs). QED.
The other direction is a bit trickier:
**Theorem 2 (Completeness of focusing)** - If $\Gamma \Rightarrow A$ then
$\Gamma \vdash A$.
Before we discuss Theorem 2, the question is, why do we care about the focused proof system and its correspondence to the unfocused proof system at all? One answer is because it lets us prove the following theorem (restated from the original poster):
**Corollary 1** - If $\Gamma \Rightarrow P$ then there exists $A \in \Gamma$ such that $\Gamma \vdash A > P$.
*Proof:* By Theorem 2 and the premise, $\Gamma \vdash P$. By case analysis, the last rule in this derivation must be $\it focus$, and the result follows immediately from the premises of that rule.
The completeness of focusing
----------------------------
There are a number of ways to prove the completeness of focusing; the approach I describe here is not the oldest and I don't claim it's the best, but it'll do. Variations of this approach can be found:
* *Sadly-uncommented Twelf code:* Robert J. Simmons, <a href="http://twelf.plparty.org/wiki/Weak_focusing">Weak Focusing</a>. The Twelf Wiki.
* *The appendices of:* Jason Reed and Frank Pfenning, Focus-Preserving Embeddings of Substructural Logics in Intuitionistic Logic.
* *In a much more general form:* Robert J. Simmons and Frank Pfenning, <a href="http://www.cs.cmu.edu/~rjsimmon/papers/CMU-CS-10-147.pdf">Weak Focusing for Ordered Linear Logic</a>. CMU Tech Report.
The basic idea is to prove cut admissibility and identity expansion *for the focused system only*, and then use that to "boost" unfocused proofs over to focused ones.
Theorem 3 is standard, and Theorem 4 is an equally important theorem that has been frequently neglected:
**Theorem 3 (Cut admissibility)**
* If $\Gamma \vdash A$ and $\Gamma \vdash A > C$, then $\Gamma \vdash C$.
* If $\Gamma \vdash A$ and $\Gamma, A \vdash C$, then $\Gamma \vdash C$.
* If $\Gamma \vdash A$ and $\Gamma, A \vdash B > C$, then $\Gamma \vdash B > C$.
*Proof:* These three statements are proved simultaneously by lexicographic induction: either the size of the principal formula $A$ gets smaller or the principal formula stays the same size while one of the provided derivations decrease in size (and the other stays the same).
**Theorem 4 (Identity expansion)**
(note: I'm still editing, just wanted to save midway through)
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