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}{(Id\downarrow)}$$

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

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

I am stuck with the following lemma, which establishes some preliminary relationship between cut-free proofs and uniform proofs. P denotes a prime formula:

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

Best Regards

(*)
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