Location: PHI Bar

(Only the location matters.)

Today we had the second (or really 1.5th) meeting of the Girard Reading Group, a.k.a. the Locus Solum Drinking Group. Many more people than I expected! It seems that obscure proof theory is a sexy topic. We're trying to go through Locus Solum systematically, although it's hard because the writing style makes digression so tempting. Fortunately, it's a diverse enough group of people that we better stay disciplined or else anarchy will ensue (as in the first meeting). Rob put up a wiki for us to pool whatever nuggets/maggots of wisdom we manage to extract. Stay tuned there for updates! Here I'll talk about a few of today's punchlines (these will probably go on the wiki soon).

I think it was a pretty productive day. We made it through the basics of designs-dessins, and started to talk about designs-desseins (what's the differance between them?). Basically, designs-dessins are focused sequent calculus proofs in affine, polarized linear logic, where formulas have been replaced by loci. I still don't have a good sense of the motivation for locativity, but the definition is very concrete: a locus ξ is just a finite sequence of natural numbers. Appending a number ("bias") i corresponds to taking an immediate subformula (ξ*i is an "immediate sublocus" of ξ). There are two kinds of sequents ("pitchforks"): ⊢ Λ (positive pitchfork) and ξ ⊢ Λ (negative pitchfork). Here Λ is a finite set of loci.

Now, Girard doesn't much intuition for what these judgments mean, but my running interpretation is as follows: a positive pitchfork asserts that all of the the loci in Λ can't be false, i.e. that if all the loci in Λ are false we have a contradiction; a negative pitchfork asserts that if all the loci in Λ are false, then ξ is also false. (I'm not really sure what it means for a locus to be false, as opposed to a formula, but let's run with it...) Observe this is just an inversion of the usual interpretation of intuitionistic sequents Γ ⊢ A and Γ ⊢∙. However, the system is not really "dual intuitionistic", because the notions "false" and "contradiction" used here are intuitionistic, and really there is a hidden notion of "direct truth" buried within the rules for proving pitchforks.

Let's take Girard's example "pre-located" formula A = (P^⊥⊕ Q^⊥) ⊗ R^⊥. There are two proper positive rules (right-rules) for A:

    
  P ⊢ Γ      R ⊢ Δ            Q ⊢ Γ      R ⊢ Δ
—————————————————————      ——————————————————————
     ⊢ Γ, Δ, A                    ⊢ Γ, Δ, A

Under our interpretation, to prove ⊢ Γ, Δ, A we must show that all of the formulas in Γ, Δ, A can't be false. These rules attempt to do this by focusing on A, i.e. they try to show that A in particular is true (still under the assumption that Γ and Δ are false). To prove A, we must prove both P^⊥⊕ Q^⊥ and R^⊥. To prove a disjunction we must prove either of the disjuncts, while proving the negation of a formula is the same as refuting it. Hence to prove A (under falsehood assumptions Γ, Δ), we must either refute P and refute R (with an arbitrary splitting of the assumptions), or else refute Q and refute R. This is exactly how we read the premises of the two rules. On the other hand, see how in one step we are able to go all the way from "show Γ, Δ, A can't all be false" to "show A is true if Γ, Δ are false" to "show either (P is false if Γ is false and R is false if Δ is false) or (Q is false if Γ is false and R is false if Δ is false)"? This is the focalization property, and it's why we didn't explicitly have to mention "truth" when we glossed the two kinds of sequents. (Editorial remark: if the truth judgment is hidden in there, though, why not show it? I.e., use a third kind of pitchfork "⊢ Λ; ξ", where ξ is already in focus. This is what I do in my paper.)

Designs-dessins are not a perfect notation for proofs, however. The problem is that not all of the loci in a pitchfork will ever be placed in focus. These loci can be split up arbitrarily among the different premises of a derivation---so we can have two dessins which apply essentially the same rules, but just differ in how they throw away these unused loci. The situation here is more or less as it is for ordinary intuitionistic logic. For any sequent calculus proof of Γ ⊢ A, we can get a "new" proof by weakening the derivation to Γ, Δ ⊢ A. However, the sequence of rules applied in both proofs is the same. Natural deduction/simply-typed lambda calculus get rid of these artificial distinctions between proofs: we can give one lambda term corresponding to both sequent calculus proofs (it simply won't mention the extra hypotheses in Δ). So designs-desseins are something like a lambda calculus for focused proofs. Yes, we should expect them to look something like spine form and pattern-matching...but we might have to squint pretty hard...