Revisions - MathOverflow

Return to Answer

The word "boost" there was basically useless.

view source

edited May 26 2011 at 3:03

The basic idea is to prove cut admissibility and identity expansion for the focused system only, and then use that to prove the critical "boost" unfocused proofs admissibility" lemmas, which show that any unfocused inference is valid over to focused onesproofs. 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.

no reason not to tidy up once it's gone community wiki

view source

edited May 25 2011 at 17:09

Rob Simmons
96●3

$${A \in \Gamma \quad qquad \Gamma \vdash A > P \over \Gamma \vdash P}{\it focus}

Proof: Straightforward induction on focused proofs (+ weakening for the unfocused proofs). QED.

put the alpha subscript in the right place(s)

view source

edited May 25 2011 at 16:43

Rob Simmons
96●3

{\Gamma, A \Rightarrow B \over \Gamma \Rightarrow A \supset B}{{\supset}R^\alphaB}{{\supset}R}{\Gamma \Rightarrow A(\alpha) \over \Gamma \Rightarrow \forall x.A(x)}{{\forall}Rx.A(x)}{{\forall}R^\alpha}

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

tidy up \supset R - didn't have a superscript alpha in the unfocused calculus; [made Community Wiki]

view source

edited May 25 2011 at 16:23

Rob Simmons
96●3

expand on proof of Theorem 2

view source

edited May 25 2011 at 16:18

Rob Simmons
96●3

links for everybody

view source

edited May 25 2011 at 15:01

Rob Simmons
96●3

minor typo

view source

edited May 25 2011 at 14:56

Rob Simmons
96●3

tiny typo

view source

edited May 25 2011 at 14:26

Rob Simmons
96●3

fix some typos, respond to a comment

view source

edited May 25 2011 at 14:07

Rob Simmons
96●3

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 "boost" unfocused proofs over to focused ones. 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.

Part 1: Cut admissibility

Part 2: Identity expansion

(note: I'm still editing, just wanted to save midway through)

Assuming this fits with your understanding, then the If there is a proof you describe $$\Gamma \vdash [ A ] > P $$$$\Gamma \vdash P$$that is simpleparametric in $P$, then $\Gamma \vdash A$.

Proof:it is provable simply 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 case analysis $\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 the observation 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$ is the only rule allows us to create a derivation parametric in $Q$ that is applicablehas an open leaf $\Gamma, A \vdash [ A ] > Q$ and that proves $\Gamma, A \vdash Q$. Without By the induction hypothesis, we can conclude $\it focus$ rule\Gamma, A \vdash A$.

These two derivations, the caculus as you describe it cannot possibly be complete together with respect rule ${\supset}L$, allow us to minimal first-order logicconstruct a derivation parametric in $P$ that has an open leaf $\Gamma, A \vdash [ B ] > P$ and that proves $\Gamma, A \vdash P$.

The original reference for what I think you're trying to do here is:

Dale Miller, Gopalan NadathurBy the induction hypothesis, Frank Pfenningwe can conclude $\Gamma, A \vdash B$, and Andre Scedrovby rule ${\supset}R$, we can conclude $A \supset B$. Uniform proofs

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

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

Part 3: Unfocused admissibility

Now we can prove "unfocused admissibility" of Pure 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 Applied Logic$\Gamma, B \vdash C$, 51:125-157then $\Gamma \vdash C$.

If $(\forall x.A(x)) \in \Gamma$ and $\Gamma, A(t) \vdash C$, 1991then $\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, A \supset B \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 (Theorem 2) 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.

partial revision

view source

edited May 25 2011 at 13:21

Rob Simmons
96●3

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 latter downarrow comes, as you note in a comment, from Andreoli's notation, but that notation is closest 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 notation you were usinggoal, we have the following sequent calculus for first-order, minimal logic:

$${P \in \Gamma \over \Gamma \Rightarrow P}{\it init}{\Gamma, A \Rightarrow B \over \Gamma \Rightarrow A \supset B}{{\supset}R}{(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}{(\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.

FirstI would argue that in your presentation above, you're the description of uniform proofs is missing at least one necessary rule , ($\it focus$) and arguably you're is missing three; I would write the full system of focused (a.k.a. uniform) proofs as follows:

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

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. Variations of this approach can be found:

Sadly-uncommented Twelf code: Robert J. Simmons, Weak Focusing. The Twelf Wiki.

The appendices of: Jason Reed and Frank Pfenning, Focus-Preserving Embeddings of Substructural Logics in Intuitionistic Logic.

In a much more general form: Robert J. Simmons and Frank Pfenning, Weak Focusing for Ordered Linear Logic. CMU Tech Report.

The basic idea is to prove cut admissibility and identity expansion for the focused system only, and then use that to "boost" unfocused proofs over to focused ones.

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

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

Theorem 4 (Identity expansion)

(note: I'm still editing, just wanted to save midway through)

explain A, B, P notation.

view source

edited May 24 2011 at 15:27

Rob Simmons
96●3

view source

answered May 24 2011 at 14:32

Rob Simmons
96●3