Natural deduction and sequent calculus - united in a polarized linear framework

In the last post I talked a little bit about what it means to give atomic propositions in a logical framework polarity. The main point I wanted to get around to was that if we have a proposition in the signature of the form P1⁺ ⊃ P2⁺ ⊃ P3⁺, then all the information contained in that rule is captured by this synthetic inference rule:

  Γ, P1+, P2+, P3+ ⊢ Q
  -------------------
  Γ, P1+, P2+ ⊢ Q

On the other hand, if I have a proposition in the signature of the form P1^- ⊃ P2^- ⊃ P3^-, then all the information contained in that rule is captured by this synthetic inference rule:

  Γ ⊢ P1-
  Γ ⊢ P2-
  --------
  Γ ⊢ P3-

By further mixing-and-matching the polarities of atomic propositions, we can get a whole host of synthetic inference rules.

First, a clarification

Before I get started with this post, I want to point out that in the last post I said something imprecise: that the strongest possible form of adequacy is to say that the synthetic inference rules induced by your signature have an exact correspondence with the "on-paper" inference rules. I then gave an example, saying that

  ∨L : (hyp A → conc C)
       → (hyp B → conc C)
       → (hyp (A ∨ B) → conc C)

corresponds to this expected synthetic inference rule

  Γ, hyp (A ∨ B), hyp A ⊢ conc C
  Γ, hyp (A ∨ B), hyp B ⊢ conc C
  -------------------------------- ∨L
  Γ, hyp (A ∨ B) ⊢ conc C

only if (hyp A) has positive polarity. But this isn't quite the right story, because from the definition of ∨L we know nothing about the contents of Γ, and our notion of adequacy with respect to the sequent calculus requires that our judgments take the form Γ ⊢ conc C where Γ contains only atomic propositions hyp A for some propositions A. So, really, this strongest possible notion of adequacy needs one additional puzzle piece, a generalization of what the Twelfers would call regular worlds. We can assume the conclusion of the derived rule is in the image of some "on paper" judgment, but we also need to verify that the premises will always end up similarly in the image of some "on paper" judgment.

Now, with that out of the way...

Representing natural deduction in LLF

The post today starts off working with a subset of the Linear Logical Framework (LLF) designed (in large part) by Cervesato. We can reason about specifications in this framework using Jason Reed's HLF/Twelf implementation. Essentially, we will be using this framework the same way we used it last week: defining a signature and looking at the synthetic inference rules that arise from that signature.

It has recently become common to see presentations of the canonical forms of a simply-typed lambda calculus presented in spine form; doing so removes a major source of unplesentless in the proof of global soundness/hereditary substitution. You do have to pay the piper, though: it is more difficult to handle the proof of global completeness/η-expansion in a spine form calculus. However, a Twelf proof that Frank Pfenning worked out in February '09, which uses something like a third-order premise, can successfully handle the proof of global completeness for a spine-form presentation of canonical forms. One version of this Twelf proof, which can be found here, is presented as a bunch of Twelf code without much commentary, and the current story arose in part due to my attempts to provide some commentary and intuition for this Twelf proof of eta expansion and generalize it to substructural logics.

In the process, I ended up investigating another way of presenting logic that is somewhere between a natural deduction and spine form presentation. A bit of Twelf code describing this presentation can be found here, but the key point is that, when we need to verify an atomic proposition Q, we pick some hypothesis A from the context and show that, from a use of A we can prove that Q can be used. This is basically what happens in spine form, but here the "spiney" things associate the opposite of the way they do in spine form presentations. It looks something like this:

  end : use A A.
  atm : hyp A -> use A (a Q) -> verif (a Q).
  ⊃I  : (hyp A -> verif B) -> verif (A ⊃ B).
  ⊃E  : use A (B1 ⊃ B2) -> verif B1 -> use A B2.

One thing that we've known for a long time is that the atomic proposition (use A B) is an instance of a pattern - it can be thought of as a Twelf representation of the linear funtion use A -o use B, in which case the rule end above is just the identity function λx.x.

But, since we're putting ourself conceptually in the territory of LLF, not the territory of LF/Twelf, we can represent the thing that is morally a linear function as an actual linear function. The main trick is appropriately using unrestricted implication -> versus linear implication -o in such a way that it controls the branch of the subproof that the linear assumption use B winds up in. The resulting signature looks much like a standard natural deduction presentation with a very non-standard transition between uses and verifications (the usual rule is just use (a Q) -> verif (a Q)) and a sprinkling of lollipops where we'd normally see arrows.

  atm : hyp A -> (use A -o use (a Q)) -> verif (a Q).
  ⊃I  : (hyp A1 -> verif A2) -> verif (A1 ⊃ A2).
  ⊃E  : use (A1 ⊃ A2) -o verif A1 -> use A2.
  ∧I  : verif A1 -> verif A2 -> verif (A1 ∧ A2).
  ∧E1 : use (A1 ∧ A2) -o use A1.
  ∧E2 : use (A1 ∧ A2) -o use A2.

We are interested, for the purpose of this presentation, in hypothetical judgments of the form (Γ; · ⊢ hyp A), (Γ; · ⊢ verif A), and (Γ; use A ⊢ use B), where Γ contains unrestricted facts of the form hyp A. In light of this, we can show the synthetic inference rules that result from the above signature.

  ---------------------------- hyp
  Γ, hyp A; · ⊢ hyp A 

  ---------------------------- use
  Γ; use A ⊢ use A 

  Γ; · ⊢ hyp A
  Γ; use A ⊢ use (a Q)
  ---------------------------- atm
  Γ; · ⊢ verif (a Q)

  Γ, hyp A1; · ⊢ verif A2
  ---------------------------- ⊃I
  Γ; · ⊢ verif (A1 ⊃ A2)

  Γ; use B ⊢ use (A1 ⊃ A2)
  Γ; · ⊢ verif A1
  ---------------------------- ⊃E
  Γ; use B ⊢ use A2

  Γ; · ⊢ verif A1
  Γ; · ⊢ verif A2
  ---------------------------- ∧I
  Γ; · ⊢ verif (A1 ∧ A2)

  Γ; use B ⊢ use (A1 ∧ A2)
  ---------------------------- ∧E1
  Γ; use B ⊢ use A1

  Γ; use B ⊢ use (A1 ∧ A2)
  ---------------------------- ∧E2
  Γ; use B ⊢ use A2

There are basically no surprises - the complete HLF/Twelf specification, including global soundness and completeness proofs, is essentially just a repeat of the most closely related related Twelf specification where the elimination rules in the signature look somewhat less unusual.

Switching up the polarity

Now, let us imagine that we add atoms with positive polarity to LLF in a way analagous to their addition in the previous post. Obviously (hyp A) is naturally positive, so we can make that change, but that is not the interesting point. Consider the derived rules if we *also* make (use A) positive and restrict our attention to sequents of the form (Γ; · ⊢ verif A) and (Γ; use A ⊢ use (a Q)).

  ---------------------------- use
  Γ; use (a Q) ⊢ use (a Q)

  Γ, hyp A; use A ⊢ use (a Q)
  ---------------------------- atm
  Γ, hyp A; · ⊢ verif (a Q)

  Γ, hyp A1; · ⊢ verif A2
  ---------------------------- ⊃I
  Γ; · ⊢  verif (A1 ⊃ A2)

  Γ; use A₂ ⊢ use (a Q)
  Γ; · ⊢ verif A1
  ---------------------------- ⊃E
  Γ; use (A₁ ⊃ A₂) ⊢ use (a Q)

  Γ; · ⊢ verif A1
  Γ; · ⊢ verif A2
  ---------------------------- ∧I
  Γ; · ⊢ (verif A1 ∧ verif A2)

  Γ; use A1 ⊢ use (a Q)
  ---------------------------- ∧I1
  Γ; use (A1 ∧ A1) ⊢ use (a Q)

  Γ; use A2 ⊢ use (a Q)
  ---------------------------- ∧I2
  Γ; use (A1 ∧ A1) ⊢ use (a Q)

While our previous formalizaiton was an interesting sort-of modified version of natural deduction, the result when we change the polarity of the atomic proposition (use A) is precisely a focused sequent calculus.

A few related points

There are a lot of other neat explorations to consider in the near vicinity of this topic. Among them are:

• Generalizing to a polarized, weakly-focused logic. I did most of this once, but there were some issues with my original proof.
• What's the precise natural deduction system that the system with weak focusing + inversion on negative propositions corresponds to? Does it correspond exactly to the style of natural deduction used by Howe in "Proof Search in Lax Logic"?
• Generalizing to a fully-focused logic (how close can we get, for instance, to the natural deduction system of Brock-Nannestad and Schürmann ("Focused Natural Deduction," LPAR 2010)?
• Can this generalize to a focused linear sequent calculus, or do I only get to use linearity once per specification? Could the machinery of HLF be used to work around that?
• The global soundness and completeness results that I established in HLF have the least amount of slickness possible - I basically just repeat the proof that I gave for the Twelf formalization without linearity. How close can we get to the intuition that the eta expansion theorem says use A -> verif A for all A?