Jason (jcreed) wrote,

Here's a nice rehash of an old idea. simrob informs me below that this has been known for about 10 years already.

Now there are a bunch of papers exploring how to do proof term assignment for sequent calculi. That is, making a sequent calculus appear as a special case of natural deduction.

I believe this is totally backwards. Sequent calculi are obviously the one true truth and light and etc. and natural deduction systems ought to be special cases of them.

Fortunately, this is the case. What you should do is invent sequent calculi, for there is a nice recipe for extracting the corresponding natural deduction system from it. The punchline is:

Normal natural deduction proofs are in exact correspondence to sequent calculus proofs that are "a little bit" focused

How much focused? You want "concentration" on negative propositions, (that is, forcible decomposition of them on the left, where they're synchronous) and just one step of forced inversion on the positive proposition that occurs at the end of one of these concentration phases --- as if there was just a little irresistible momentum left.

I first came to believe this fact in a gradlounge whiteboard conversation with Dan Licata some time ago --- he may have coined the word "concentration" then, too. But I never had a really nice proof of it until now. The completeness (of normal natural deduction) proof was easy, but the soundness proof was elusive.

Say Γ |- A means A is derivable in a sequent calculus, and Γ [A] |- C indicates left focus on A while proving C. We're allowed to "focus" in this way on positive props, too. It just forces us to do that one step of inversion alluded to above, and then we give up focus. I'll write normal and atomic natural deductions like Γ ⇐ A and Γ ⇒ A.

The completeness theorem is

1. If Γ |- A, then Γ ⇐ A
2. If Γ [A] |- C, then there is a derivation from Γ ⇒ A to Γ ⇐ C.

Having the conclusion be a derivation-with-hole like this is a clever trick I learned from Frank's proof of the identity property in focusing logics. The proof basically proves itself once you've got this induction invariant.

And so I puzzled over how to characterize the derivations from Γ ⇒ A to Γ ⇐ C that were in the image of this translation, supposing maybe I had to consider linear occurrences of the hypothesized derivation of Γ ⇒ A, or something... and it never worked out very nicely. Turns out all I needed to do was choose a less blatantly symmetric (and perhaps more *subtly* symmetric) way of stating the converse: the soundness theorem that's easy to prove is

1. If Γ ⇐ A, then Γ |- A.
2. If Γ ⇒ A, then for all C there is a derivation from Γ [A] |- C to Γ |- C.

It's really just hitting it with the same "conclude a hypothetical derivation" hammer, only with the forms of the derivations swapped around! The two "2."s taken together look kinda like cut principles, only with different conclusions.

Anyway, it turned out to be very easy to twelf up, so here it is, for a STLC with implication, disjunction, and base types:

% Propositions

o : type.
a : o. % Base type
=> : o -> o -> o. %infix right 3 =>.
v : o -> o -> o. %infix right 2 v.
% LC+1 Sequent Calculus

conc : o -> type.
hyp : o -> type.
fconc : o -> o -> type.

var : fconc a a.
foc : (hyp A -> conc C) <- fconc A C.

=>R : conc (A => B) <- (hyp A -> conc B).
=>L : fconc (A => B) C 
       <- conc A
       <- fconc B C.
vL : fconc (A v B) C
      <- (hyp A -> conc C)
      <- (hyp B -> conc C).
vR1 : conc A -> conc (A v B).
vR2 : conc B -> conc (A v B).

% Normal Natural Deduction

nrm : o -> type.
syn : o -> type.

coe : syn a -> nrm a.
lam : (syn A -> nrm B) -> nrm (A => B).
app : syn (A => B) -> nrm A -> syn B.
case : syn (A v B) -> (syn A -> nrm C) -> (syn B -> nrm C) -> nrm C.
inl : nrm A -> nrm (A v B).
inr : nrm B -> nrm (A v B).

% Completeness of NND wrt LC+1
% i.e. (LC+1 |- A) ---> (NND |- A)

complete1 : conc A -> nrm A -> type.
complete2 : fconc A C -> (syn A -> nrm C) -> type.
cvt : hyp A -> syn A -> type.

complete1/foc : complete1 (foc FCONC HYP) (NRM SYN)
                 <- complete2 FCONC NRM
                 <- cvt HYP SYN.
complete1/=>R : complete1 (=>R CONC) (lam NRM)
                 <- ({x : hyp A} {y : syn A} cvt x y
                       -> complete1 (CONC x) (NRM y)).

complete2/var : complete2 var coe.
complete2/=>L : complete2 (=>L FCONC CONC) ([s] K (app s ARG))
                 <- complete2 FCONC K
                 <- complete1 CONC ARG.
complete2/vL : complete2 (vL Br2 Br1) ([s] case s NRM1 NRM2)
                <- ({x:hyp A}{y:syn A} cvt x y -> complete1 (Br1 x) (NRM1 y))
                <- ({x:hyp B}{y:syn B} cvt x y -> complete1 (Br2 x) (NRM2 y)).
complete1/vR1 : complete1 (vR1 CONC) (inl NRM) <- complete1 CONC NRM.
complete1/vR2 : complete1 (vR2 CONC) (inr NRM) <- complete1 CONC NRM.

(complete1 +CONC -NRM)
(complete2 +FCONC -NRM)
(cvt +HYP -SYN).
%block b : some {A:o} block {x:hyp A}{y:syn A}{d:cvt x y}.
%worlds (b) (complete1 _ _) (complete2 _ _) (cvt _ _).
%total (CONC FCONC HYP) (complete1 CONC _) (complete2 FCONC _) (cvt HYP _).

% Soundness of NND wrt LC+1
% i.e. (NND |- A) ---> (LC+1 |- A)

sound1 : nrm A -> conc A -> type.
sound2 : syn A -> ({C:o} fconc A C -> conc C) -> type.

sound1/coe : sound1 (coe SYN) (CONC a var)
   <- sound2 SYN CONC.
sound1/lam : sound1 (lam NRM) (=>R CONC)
              <- ({x : syn A} {y : hyp A} sound2 x ([c] [fc] foc fc y) 
                    -> sound1 (NRM x) (CONC y)).
sound1/case : sound1 (case SYN Br1 Br2) (X _ (vL CONC2 CONC1))
               <- ({x:syn A}{y:hyp A} sound2 x ([c][fc] foc fc y) -> sound1 (Br1 x) (CONC1 y))
               <- ({x:syn B}{y:hyp B} sound2 x ([c][fc] foc fc y) -> sound1 (Br2 x) (CONC2 y))
               <- sound2 SYN X.

sound2/app : sound2 (app F ARG) ([c] [fc] CF c (=>L fc CARG))
   <- sound2 F CF
   <- sound1 ARG CARG.
sound1/inl : sound1 (inl NRM) (vR1 CONC) <- sound1 NRM CONC.
sound1/inr : sound1 (inr NRM) (vR2 CONC) <- sound1 NRM CONC.

(sound1 +NRM -CONC)
(sound2 +SYN -CONC).
%block b : some {A:o} block {x:syn A}{y:hyp A}{d:sound2 x ([c][fc] foc fc y)}.
%worlds (b) (sound1 _ _) (sound2 _ _).
%total (NRM SYN) (sound1 NRM _) (sound2 SYN _).

% To actually show that these compose to the identity:

eqsc1 : sound1 N C -> complete1 C N -> type.
eqcs1 : complete1 C N -> sound1 N C -> type.
eqsc2 : sound2 E E' -> complete2 D D' -> sound1 (D' E) (E' _ D) -> type.
eqcs2 : sound2 E E' -> complete2 D D' -> complete1 (E' _ D) (D' E) -> type.

Also every time I talked to Frank about this he kept mentioning some paper that basically proved this for just negatives, or maybe even just for implication --- and I always forget who it was. Anyway, I think the larger focusing story deserves to be told.
Tags: logic, twelf

  • (no subject)

    After getting home from work immediately appeared to be a traintastrophe in the making, went to see Esther Schor talk about her book "Bridge of…

  • (no subject)

    Went to a series of maker-y talks hosted by Pivotal. The last one, by the woman who runs Genspace, "New York City's Community Biolab" was pretty…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded