Dear All

Gentzen (*) claimed that through cut-elimination, he can normalize proofs. It is well known that cut-eliminated proofs might still contain some unnecessary noise. I am trying to show that cut-eliminated proofs can be further converted into so called uniform proofs. Uniform proofs are not only cut-eliminated, but also focused. 

Focused proofs are currently actively researched. Chaudhuri (**) shows for example some good behaviour in planning problems formulated with linear logic.

I am currently working with minimal logic and horn clauses. I am using the following helper derivation, which should model the clause picking and makes up the focusing:

${}\over{\vdash P \downarrow P}$

${\Gamma \vdash A[x/t] \downarrow P}
\over
{\Gamma \vdash \forall x A \downarrow P}$

${\Gamma \vdash A\quad \quad\Delta \vdash B \downarrow P}
\over
{\Gamma, \Delta \vdash A \rightarrow B \downarrow P}$

I am stuck with the following lemma:

> If $\Gamma \vdash P$ then $\Gamma' \vdash A \downarrow P$ for some $A$ in $\Gamma$ and some $\Gamma'$ subset $\Gamma$

Best Regards

P.S.: I guess I could do the following detour: Define some calculus that does extract proof objects. And then look at the proof objects, and further normalize them. But let's assume that we don't invoke the device of proof objects.

(*)
Gerhard Genzen, "Untersuchungen über das logische Schließen. I". Mathematische Zeitschrift 39 (2): 176–210. 1934. http://gdz.sub.uni-goettingen.de/dms/resolveppn/?PPN=GDZPPN002375508.

(**)
Kaustuv Chaudhuri, "The Focused Inverse Method for Linear Logic", Thesis, Carnegie Mellon University Pittsburgh, 2006. http://reports-archive.adm.cs.cmu.edu/anon/2006/CMU-CS-06-162.pdf