A sequent calculus proof Consider the sequent calculus (with multiplicative contexts) defined by the following rules (without contraction and weakening). The sequent calculus is taken from p.23 here: http://users.ox.ac.uk/~cpgl0036/pdf/asudeh-giorgolo-perspectives.pdf):
$$ \frac{\qquad }{A \vdash A} \,{Id} $$ 
$$ \frac{\Gamma\vdash B \qquad B, \Delta\vdash C}{\Gamma, \Delta \vdash C} \,{Cut} $$
$$ \frac{\Delta\vdash A \qquad \Gamma, B\vdash C}{\Gamma, \Delta,  A \rightarrow B \vdash C} \,{\rightarrow L} $$
$$ \frac{\Gamma, A \vdash B}{\Gamma \vdash A \rightarrow B} \,{\rightarrow R} $$
$$ \frac{\Gamma \vdash A}{\Gamma \vdash \bigcirc A} \,{\bigcirc R} $$
$$ \frac{\Gamma, A \vdash \bigcirc B \qquad }{\Gamma, \bigcirc A \vdash \bigcirc B} \,{\bigcirc L} $$
I can prove $\bigcirc (A \rightarrow B) \vdash \bigcirc A \rightarrow \bigcirc B$ in this calculus, but not the converse $\bigcirc A \rightarrow \bigcirc B \vdash \bigcirc (A \rightarrow B)$. Is the converse provable? I cannot find a proof of it.
 A: The general recipe for answering such questions is based on a cut-elimination theorem. The authors state in footnote 28 that the $Cut$ rule is "admissible" for this calculus, which is another way to say that it can be eliminated.[*] To decide whether $\bigcirc A \to \bigcirc B \vdash \bigcirc (A \to B)$ is provable, it therefore suffices to ask, "Does it have a cut-free proof?"
Now, any cut-free proof of $\bigcirc A \to \bigcirc B \vdash \bigcirc (A \to B)$ must necessarily end in either ${\to}L$ or ${\bigcirc}R$, as in one of the following proof attempts:
$$
 \frac{\vdash \bigcirc A \qquad \bigcirc B \vdash \bigcirc (A \to B)}{\bigcirc A \to \bigcirc B \vdash \bigcirc (A \to B)} {\to}L
\qquad
 \frac{\bigcirc A \to \bigcirc B \vdash A \to B}{\bigcirc A \to \bigcirc B \vdash \bigcirc (A \to B)} {\bigcirc}R
$$
The first possibility can be immediately eliminated because it is not possible to prove $\vdash \bigcirc A$ for arbitrary $A$ (take $A$ to be any atomic formula). The second possibility can likewise be eliminated through a bit more case analysis of cut-free proofs: eventually we would be required to prove $\bigcirc B \vdash B$, but this is not possible for general $B$.
Therefore, $\bigcirc A \to \bigcirc B \vdash \bigcirc (A \to B)$ is not provable for general $A$ and $B$.
[*] technically, a rule is admissible for a sequent calculus if given derivations of the premises, we can construct a derivation of the conclusion without using the rule itself. In particular, the $Cut$ rule is admissible if given cut-free derivations of $\Gamma \vdash B$ and $B, \Delta \vdash C$, we can always construct a cut-free derivation of $\Gamma,\Delta \vdash C$.

Edit: Of course, the extra bit of reasoning which is missing from this argument is the proof of cut-elimination itself which the authors claim in the footnote. That is usually done on a case-by-case basis for a particular sequent calculus, and is a good exercise (you can find an example for another sequent calculus in these lecture notes by Frank Pfenning).
