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.

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

${}\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.