Stack Exchange: writing inference rules and proofs

gistfile1.txt

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:

* *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, <a href="http://www.cs.cmu.edu/~fp/papers/substruct10.pdf">Focus-Preserving Embeddings of Substructural Logics in Intuitionistic Logic</a>.
* *Mostly just hinted at:* Frank Pfenning and Robert J. Simmons, <a href="http://www.cs.cmu.edu/~fp/papers/lics09.pdf">Substructural Operational Semantics as Ordered Logic Programming</a>. LICS 2009.
* *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 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:

### Part 1: Cut admissibility

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

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

### Part 3: Unfocused admissibility

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

**Theorem 5 (Unfocused admissibility)** 

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