Return to Answer

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.

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.

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

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

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

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

$$ {P \in \Gamma \over \Gamma \Rightarrow P}{\it init} \qquad {\Gamma, A \Rightarrow B \over \Gamma \Rightarrow A \supset B}{{\supset}R^\alpha} \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} \qquad {(\forall x.A(x)) \in \Gamma \qquad \Gamma, A(t) \Rightarrow C \over \Gamma \Rightarrow C}{{\forall}L} $$

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

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

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