*polarity*. The main point I wanted to get around to was that if we have a proposition in the signature of the form

`P1`, then all the information contained in that rule is captured by this synthetic inference rule:

^{+}⊃ P2^{+}⊃ P3^{+}Γ, P1On the other hand, if I have a proposition in the signature of the form^{+}, P2^{+}, P3^{+}⊢ Q

-------------------

Γ, P1^{+}, P2^{+}⊢ Q

`P1`, then all the information contained in that rule is captured by this synthetic inference rule:

^{-}⊃ P2^{-}⊃ P3^{-}Γ ⊢ P1By further mixing-and-matching the polarities of atomic propositions, we can get a whole host of synthetic inference rules.^{-}

Γ ⊢ P2^{-}

--------

Γ ⊢ P3^{-}

### 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)corresponds to this expected synthetic inference rule

→ (hyp B → conc C)

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

Γ, hyp (A ∨ B), hyp A ⊢ conc Conly if (

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

-------------------------------- ∨L

Γ, hyp (A ∨ B) ⊢ conc C

`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.One thing that we've known for a long time is that the atomic proposition (

atm : hyp A -> use A (a Q) -> verif (a Q).

⊃I : (hyp A -> verif B) -> verif (A ⊃ B).

⊃E : use A (B_{1}⊃ B_{2}) -> verif B_{1}-> use A B_{2}.

`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).We are interested, for the purpose of this presentation, in hypothetical judgments of the form (

⊃I : (hyp A_{1}-> verif A_{2}) -> verif (A_{1}⊃ A_{2}).

⊃E : use (A_{1}⊃ A_{2}) -o verif A_{1}-> use A_{2}.

∧I : verif A_{1}-> verif A_{2}-> verif (A_{1}∧ A_{2}).

∧E_{1}: use (A_{1}∧ A_{2}) -o use A_{1}.

∧E_{2}: use (A_{1}∧ A_{2}) -o use A_{2}.

`Γ; · ⊢ 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.

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

Γ, hyp A; · ⊢ hyp A

---------------------------- use

Γ; use A ⊢ use A

Γ; · ⊢ hyp A

Γ; use A ⊢ use (a Q)

---------------------------- atm

Γ; · ⊢ verif (a Q)

Γ, hyp A_{1}; · ⊢ verif A_{2}

---------------------------- ⊃I

Γ; · ⊢ verif (A_{1}⊃ A_{2})

Γ; use B ⊢ use (A_{1}⊃ A_{2})

Γ; · ⊢ verif A_{1}

---------------------------- ⊃E

Γ; use B ⊢ use A_{2}

Γ; · ⊢ verif A_{1}

Γ; · ⊢ verif A_{2}

---------------------------- ∧I

Γ; · ⊢ verif (A_{1}∧ A_{2})

Γ; use B ⊢ use (A_{1}∧ A_{2})

---------------------------- ∧E_{1}

Γ; use B ⊢ use A_{1}

Γ; use B ⊢ use (A_{1}∧ A_{2})

---------------------------- ∧E_{2}

Γ; use B ⊢ use A_{2}

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

---------------------------- useWhile 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 Q) ⊢ use (a Q)

Γ, hyp A; use A ⊢ use (a Q)

---------------------------- atm

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

Γ, hyp A_{1}; · ⊢ verif A_{2}

---------------------------- ⊃I

Γ; · ⊢ verif (A_{1}⊃ A_{2})

Γ; use A₂ ⊢ use (a Q)

Γ; · ⊢ verif A_{1}

---------------------------- ⊃E

Γ; use (A₁ ⊃ A₂) ⊢ use (a Q)

Γ; · ⊢ verif A_{1}

Γ; · ⊢ verif A_{2}

---------------------------- ∧I

Γ; · ⊢ (verif A_{1}∧ verif A_{2})

Γ; use A_{1}⊢ use (a Q)

---------------------------- ∧I_{1}

Γ; use (A_{1}∧ A_{1}) ⊢ use (a Q)

Γ; use A_{2}⊢ use (a Q)

---------------------------- ∧I_{2}

Γ; use (A_{1}∧ A_{1}) ⊢ use (a Q)

`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`?

## No comments:

## Post a Comment