Locus Solum: From the rules of logic to the logic of rules

Locus Solum: From the rules of logic to the logic of rules by Jean-Yves Girard, 2000.
The monograph below has been conceived as the project of giving reasonable foundations to logic, on the largest possible grounds, but not with the notorious reductionist connotation usually attached to "foundations". Locus Solum would like to be the common playground of logic, independent of systems, syntaxes, not to speak of ideologies. But wideness of scope is nothing here but the reward of sharpness of concern : I investigate the multiple aspects of a single artifact, the design. Designs are not that kind of syntax-versus-semantics whores that one can reshape according to the humour of the day : one cannot tamper with them, period. But what one can achieve with them, once their main properties —separation, associativity, stability— have been understood, is out of proportion with their seemingly banal definition.
Sounds rather controversial, but can make an interesting reading if you believe logic is related to programming (your last name doesn't have to be either Curry or Howard).

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Sounds very interesting.

Sounds very interesting. Since I am buried with work, it would be nice if someone manages to give a summary, so I know what I'm missing...

A Riddle

I started to read this paper and was given the idea of a riddle:

Q: What do you do when you are a great man in your field, you've made major contributions and you are not content to rest on your laurels?

A: Redefine your field from the ground up using a completely new terminology, notation and metaphors.

I'm starting to think the pickings are getting slim in the field of proof theory...

(On a smaller note, his choice of the term "spiritual" to describe non-ludic logic is a particularly jarring case of "faux amis" mental translation.)


Ludics is tremendously interesting from a proof theoretic point of view. I don't understand more than the first chunk of it yet, and that part is still full of wonderfully productive and useful ideas. It is evidence that there's a whole lot more yet to be done in proof theory.

A single example: the daimon. The core idea is really simple -- if you look at a logic as an algebraic structure, then you'll notice that it lacks certain completeness properties (in order to maintain the consistency of the logic). So, you can introduce rules (the daimon) that make the logic-as-structure complete, but which make it inconsistent as a logic. Now, you can prove theorems which do structural manipulations on proofs, which rely on the completeness properties for their correctness. Then, at the end of the day you throw out any proofs that used the bad rules.

This takes the core insight of structural proof theory -- that proofs are just another kind of mathematical object, like groups or lattices -- and takes it really seriously.


This takes the core insight of structural proof theory -- that proofs are just another kind of mathematical object, like groups or lattices -- and takes it really seriously.

I take it as a given that we ALREADY take this idea really seriously, even before we go "ludic". (You know, proof = program)

I'm not sure why the next step can't be taken incrementally, though, rather than starting over with a whole new set of terminology. The first few pages of the paper look to me like a bunch of familiar ideas renamed to emphasize some new direction.

This approach is great when you want to appear revolutionary, but terrible when you want to be evolutionary and build on previously developed knowledge.

Could this be the beginning of another category theory / set theory type split in the community? I certainly hope not.

(I'm also starting to guess what pressures in the field brought about the new "dialogue semantics" sections in Lectures on the Curry-Howard Isomorphism...)

Reworking old results in a new formalism is great for keeping PhD candidates busy (and for allowing established scholars to make their mark), but it isn't necessarily great for advancing the state of human knowledge.

Do you have any examples of new results (rather than re-interpreted ideas) that have resulted from this new approach Neel?


...I hope to be submitting one pretty soon. I'll toss a link here when the draft is written. :)

Anyway, what Girard is doing bridges the gap between two different strands of research. There's the denotational game semantics kind of stuff, and there's the operational focalization stuff, which he's integrating together. I only really have a firm grasp on the second half, and I'm excited precisely because ludics gives me an angle on understanding the first half and why it's important and enlightening. This isn't the first time he's done it, too -- linear logic was born when Girard started looking for a proof theory corresponding to a denotational doohickey (coherence spaces) that he had cooked up.

It's true that in Locus Solum he's making us jump through hoops for the treat, but he has a track record that makes me confident that it'll be tasty. So hop hop hop for me. :)

Raymond Roussel

Just to think of the connection makes my head go dizzy... Locus Solus is a tour de force in nonsense made clear by dint of rational explanation; one of the founding works of surrealism.


I've only skimmed it so far, but it does remind me of Bjarne Stroustrop's famous paper on whitespace-overloading!

"New Impressions of Africa"

"New Impressions of Africa" by Roussel made me comfortable with Scheme!!

The basic construction of each of the work's four cantos is the same: a brief "impression of Africa" is interrupted midway by a parenthesis; this new passage is then interrupted by a further parenthesis and so on until a maximum number of five parentheses is reached and they begin to close again.

"an imagination that joins the mathematicians’ delirium to the poets’ logic"