This post is a change of scene for those of you that have come to expect gentle meditations on matters personal.

I’m going to experiment with posting some of my work scribblings as an irregular record of thoughts I’m having while working on sabbatical. It may well confirm the impression that you might have that I’m crazy, but hey, I have tenure, so I won’t worry about that too much.

Over the last couple of days I’ve been thinking about cut elimination arguments, and in particular, the general cut elimination argument that you can find in my book (look around here).

It struck me last night – as I was trying to find the right mix of generality and clarity – that there’s nothing in Gentzen’s original argument that *requires* that formulas have just two distinct positions in a sequent (the traditional two positions are *antecedent* and *consequent*, or *left* and *right*, or if you like, *premise* and *conclusion* or *input* and *output*). Every presentation of cut elimination that I’m aware of (even for single sided systems which don’t have an explicit left or right to a sequent) has two “positions” in which a formula can reside. (In single sided systems this is represented by the dualising map on formulas). The point is seen in the structure of the identity rule (an instance of the formula on each position, left and right, is what gives you an *identity*) and the cut rule (take two sequents, one with the formula in *antecedent* position, the other with it in *consequent* position – the *cut* rule tells you how to combine them).

Well, as I was saying, it struck me last night (at approximately 1:30am – I indulge myself by working late when my spouse is out of town) that the form of the traditional cut-elimination argument – when you look at it in the right way, at least – in no way requires that there are just two positions in a sequent. You could have *four* if you like. Or maybe *three*. Or soemthing else entirely. All you need is for identity and cut to interact in the right kind of way (cuts composed with identities disappear), for the rules to commute with cuts in parametric positions, and for cuts on principal formulas to be eliminable. It works quite generally, which is very pretty. (I have an example scrawled on pages of my notebook as I was taking a coffee after lunch this afternoon of a cut elimination theorem for a sequent system in which sequents have *four* different slots. You can visualise proofs in this system as having input and output going from top to bottom on the page *and* different inputs and outputs going left-to-right. In this picture, there are two kinds of cut: *horizontal* and *vertical*.)

Now, the question for you, gentle reader (if you have read this far, as you seem to have): Can you think of any reason why we would *want* such a thing, beyond the insane desire to generalise well-known theorems and constructions? Can you think of any applications in which you might want proof-like-objects to go in “more than one direction” in this sense, or analogously, in which you might have attitudes of more than just assertion and denial to propositional content and more importantly, have vocabulary that is sensitive to these different features? I can think of one possibility.

← Reflections on Iona, part 2 | News Archive | Week 1 →

I’m *Greg Restall*, and this is my personal website. ¶ From August 2021, I will be the Shelby Cullom Davis Professor of Philosophy at the University of St Andrews.

- greg@consequently.org
- keybase.io/consequently, to sign or encrypt a message to send to me privately.
- @consequently on Twitter.
- @consequently on Instagram.
- @consequently on GitHub.

To receive updates from this site, you can subscribe to the RSS feed of all updates to the site in an RSS feed reader, or follow me on Twitter at @consequently, where I’ll update you if anything is posted.