How establish conversion of cut-free proof into uniform proof?

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

-
I don’t understand the question. What is $A\downarrow P$, and what are uniform proofs? – Emil Jeřábek May 23 '11 at 18:31
Like Emil, I don't understand the question. You refer to "the following helper derivation" but what follows looks like a deductive system, not a derivation. This deductive system has the property that every derivable sequent has an occurrence of $\downarrow$ on the right, yet the lemma you want has a hypothesis $\Gamma\vdash P$ with no $\downarrow$. – Andreas Blass May 24 '11 at 0:36

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^\alpha} \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 \qquad \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).

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; I'd welcome anyone else that wanted to elaborate other, possibly simpler, versions of this proof. Variations of this approach can be found in the following places:

The basic idea is to prove cut admissibility and identity expansion for the focused system only, and then use that to prove the critical "unfocused admissibility" lemmas, which show that any unfocused inference is valid over focused proofs. One reason that I like this presentation is that it shows how the completeness of focusing is a straightforward consequence of cut admissibility and identity expansion for the focused sequent calculus.

Theorem 3 is standard, and Theorem 4 is an equally important theorem that has been frequently neglected:

• 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).

Part 2: Identity expansion

Theorem 4 (Identity expansion) If there is a proof $$\Gamma \vdash A > P$$ $$\vdots$$ $$\Gamma \vdash P$$ that is parametric in $P$, then $\Gamma \vdash A$.

Proof: By induction on the structure of $A$.

Case $A = P'$. We are given a derivation parametric in $P$ that has an open leaf $\Gamma \vdash P' > P$ and that proves $\Gamma \vdash P$. By letting $P = P'$, we can show $\Gamma \vdash P' > P'$ by $\it init$, which gives us $\Gamma \vdash P'$, exactly what we needed to show.

Case $A = A \supset B$. We are given a derivation parametric in $P$ that has an open leaf $\Gamma \vdash A \supset B > P$ and that proves $\Gamma \vdash P$.

First, note that we can weaken this derivation to a derivation parametric in $P$ that has an open leaf $\Gamma, A \vdash A \supset B > P$ and that proves $\Gamma, A \vdash P$.

Second, note that the rule $\it focus$ allows us to create a derivation parametric in $Q$ that has an open leaf $\Gamma, A \vdash A > Q$ and that proves $\Gamma, A \vdash Q$. By the induction hypothesis, we can conclude $\Gamma, A \vdash A$.

These two derivations, together with rule ${\supset}L$, allow us to construct a derivation parametric in $P$ that has an open leaf $\Gamma, A \vdash B > P$ and that proves $\Gamma, A \vdash P$. By the induction hypothesis, we can conclude $\Gamma, A \vdash B$, and by rule ${\supset}R$, we can conclude $\Gamma \vdash A \supset B$.

Case $A = \forall x. A(x)$. (Omitted.)

This completes the identity expansion lemma which has, as a simple corollary, the identity theorem that for all $A$, $\Gamma, A \vdash A$ (we actually used this corollary in the second case).

Now we can prove "unfocused admissibility" of all of the left rules:

• If $P \in \Gamma$, then $\Gamma \vdash P$.
• If $(A \supset B) \in \Gamma$, $\Gamma \vdash A$, and $\Gamma, B \vdash C$, then $\Gamma \vdash C$.
• If $(\forall x.A(x)) \in \Gamma$ and $\Gamma, A(t) \vdash C$, then $\Gamma \vdash C$.

The first statement we can prove immediately by ${\it init}$ followed by ${\it focus}$.

For the second statement, we use identity expansion to prove that $\Gamma, A \vdash A$. From this fact, the given fact that $A \supset B \in \Gamma$, and the ${\it focus}$ and ${{\supset}L}$ rules, it is possible to construct a derivation parametric in $P$ that has an open leaf $\Gamma, A \vdash B > P$ and that proves $\Gamma, A \vdash P$. Therefore, by identity expansion, $\Gamma, A \vdash B$. We were given that $\Gamma \vdash A$, so by cut admissibility, $\Gamma \vdash B$. We were also given that $\Gamma, B \vdash C$, so by cut admissibility, $\Gamma \vdash C$.

I'll omit again the proof of the third statement.

Part 4: Proving Theorem 2 by straightforward induction

Now that I have the unfocused admissibility theorems, proving the completeness of focusing is just a matter of straightforward induction over the unfocused derivations. Whenever we encounter a right rule we can use the induction hypothesis along with the corresponding rule in the focused sequent calculus. Whenever we encounter another rule we use the appropriate unfocused admissibility theorem.

Theorem 2 (Completeness of focusing) - If $\Gamma \Rightarrow A$ then $\Gamma \vdash A$.

Proof - By induction on the derivation $\Gamma \Rightarrow A$.

Case 1: $\mathcal D = {P \in \Gamma \over \Gamma \Rightarrow P}{\small \it init}$.

To show: $\Gamma \vdash P$.

Immediate from the assumption $P \in \Gamma$ (premise of ${\it init}$ and unfocused admissibility (part 1).

Case 2: $\mathcal D = {\Gamma, A \Rightarrow B \over \Gamma \Rightarrow A \supset B}{\small {\supset} R}$

To show: $\Gamma \vdash A \supset B$.

By the induction hypothesis, we have $\Gamma, A \vdash B$. Then, by rule ${\supset}R$, we have $\Gamma \vdash A \supset B$, which is what we needed to show.

Case 3: $\mathcal D = {(A \supset B) \in \Gamma \quad \Gamma \Rightarrow A \quad \Gamma, B \Rightarrow C \over \Gamma \Rightarrow C} {\small {\supset} L}$

To show: $\Gamma \vdash C$.

By the induction hypothesis, we have $\Gamma \vdash A$ and $\Gamma, B \vdash C$. Then the result follows from the fact that $(A \supset B) \in \Gamma$ and the unfocused admissibility lemma.

Case 4: (${\forall}R^\alpha$, omitted)

Case 5: (${\forall}L$, omitted)

-
@Rob: Will Theorem 4 (Identity expansion) still hold if A is of positive polarity? Or do we need to state another version if positive propositions are added to the language? – Ali Lahijani Oct 30 '11 at 10:43
Beautiful question! Yes, you need to generalize the identity expansion property in an interesting and non-obvious way to handle positive propositions. Luckily, I have a paper on arXiv that describes how, which I plan to submit to a journal after a bit more revision: arxiv.org/abs/1109.6273 – Rob Simmons Oct 30 '11 at 15:54
Now I am studying your paper and its Twelf companion. It seems interesting. Thanks for the link. – Ali Lahijani Oct 31 '11 at 16:26