lucidity vs ludicity, and translating one esoteric language into a slightly less esoteric one

One of the things I often wonder about is how to say things that are intelligible. Too frequently, I lapse into jargon─sometimes even on-the-spot-invented jargon─and only realize this after the damage has been done. An example: the previous blog post, which was probably incomprehensible to all but...well, probably to all. I promise I will try hard to avoid doing this in the future.

But on the topic of making things less inscrutable─and not on the topic of Girard!, though keep your eyes on the Girard Reading Group Wiki─another thing I've been thinking about is how to translate Martin-Löf's "judgment vs proposition" distinction (as spelled out in the Siena Lectures) into the language of category theory. At first, the judgment vs proposition distinction may seem pedantic: okay, one can distinguish between a well-formed proposition "A" and the assertion that it is true "A true"...but so what? Well, the distinction helps get dependent type theory off the ground, since well-formedness is defined mutually with truth (the dependent quantifier ∏x:A.B is a well-formed proposition if and only if A is well-formed and B is well-formed under the assumption x:A). More mundanely, it is obvious that a separate notion of judgment is useful if we want to refute propositions as well as assert them, using the judgment "A false" in addition to "A true".

Well, this is actually not quite so obvious. Why not just assert ¬A? For a philosophical explanation of why not, Greg Restall's essay "Multiple Conclusions" is a nice read. From a proof/type-theoretic perspective, the reason why not to identify "A false" with "¬A " is that we need the separate judgment in order to obtain "good compositionality" principles─this is an informal but very general law gleaned by Frank Pfenning and collaborators over years of refining the "judgmental method", to which the paper "A judgmental reconstruction of modal logic" probably serves as the most complete introduction. Unfortunately, though, my impression is that these principles are still not very widely accepted or understood.

I think part of the problem is the seemingly obscure philosophical origins of the judgmental method (although its application is practically motivated), and so what I would like is a translation guide into the language of category theory (an order of magnitude less obscure, though granted still sometimes considered esoteric) . I think there must be such a translation, since the whole point of the judgmental method (at least in my mind) is obtaining compositionality principles.

Does anyone know if the judgment vs proposition distinction has been explored before in category theory? As a simple example of a system with two judgments that should be possible to explain categorically, I propose the bidirectional lambda calculus with implication and conjunction (described in Section 3.1 here).

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