simrob posed a neat puzzle over dinner: show that the linear exponential ! is not definable using any of the other linear connectives, including unrestricted implication. I think I have a proof now, after one wrong attempt. It goes like this. Suppose we have a propositional expression ψ(A) (not mentioning !) such that ψ(A) |- !A and !A |- ψ(A) for all A. Consider the case where A is an atomic proposition, and look at the proof of ψ(A) |- !A.We claim that it will never involve the ! right rule. Why? Because the proof will never toss anything into the unrestricted context in any branch where !A is still the goal, so using !-right will always leave us with |- A, which is unprovable. For an illustrative almost-counterexample, ψ(A) might be something like (D ⊃ B) ⊃ C so that after applying ⊃L and the ⊃R we wind up with (among other goals) the goal D; . |- C, but notice that in order to get D in the unrestricted context we had to clobber !A with C. This sequent has no banged subformulae at all, so we certainly can't use !-right.
Now since the proof never decomposes !A on the right at all — indeed the only way it can finish, if you think about it, is by liberal use of the 0-left rule — there is a proof of precisely the same structure that establishes ψ(A) |- 0. By cut admissibility, using the assumption that !A |- ψ(A), we obtain !A |- 0, which quickly leads to a contradiction by inversion on the !-left and (lack of) 0-right rules.
