Everyone I have asked so far seem to agree that if a rule in a sequent calculus system permutes down all the other rules of this system, than this rule is invertible, and vice versa. But when I ask for a proof of that, no one knows about it. Is it folklore? Is it so obvious that I cannot see it?
I started writing about this invertibility issue here: https://www.dropbox.com/s/1cby7a3qgraiyyd/invertibility.pdf?dl=0 [1]
If any one out there has more information or ideas, I’d be happy to be informed.
[1] Thanks to Elaine Pimentel, who read and commented on the first draft, and with whom I’ve had many insightful discussions, and to Arnold Beckmann for having pointed out the induction proof of invertibility (and to Norbert Preinning for a lovely workshop).