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.


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).

  • $\begingroup$ Thanks. You can actually prove $\bigcirc A$ for arbitrary A, given that the sequent is as the $\bigcirc R$ rule describes. That is, from $A \vdash A$, we can move to $A \vdash \bigcirc A$. However, that move wouldn't work for your first proof attempt, since the "A" would have to then be present in the lower sequent. In fact, though, I've found that, although we don't have $B \vdash B$ for all formulas, for some we do; in fact, we have $\bigcirc (A \rightarrow \bigcirc B) \equiv A \rightarrow \bigcirc B). $\endgroup$ – user65526 Aug 16 '17 at 16:29
  • $\begingroup$ What I was also trying to find out was whether we have $\bigcirc (M \land N) \vdash \bigcirc M \land \bigcirc N$, when we add a multiplicative conjunction to the language with the rules $$ \frac{\Gamma\vdash A \qquad \Delta\vdash B}{\Gamma, \Delta \vdash A \land B} \,{\land R} $$ and $$ \frac{\Gamma, A, B \vdash C \qquad}{\Gamma, A \land B \vdash C} \,{\land L} $$. We seem to have the converse. $\endgroup$ – user65526 Aug 16 '17 at 16:33
  • $\begingroup$ Also, if we are working in intuitionistic logic with the modality $\bigcirc$ we seem to have $\bigcirc (A \rightarrow B) \equiv \bigcirc A \rightarrow \bigcirc B$, so adding contraction and weakening to the rules above must mean that at least one of your two proof attempts can be mended in an intuitionistic setting. $\endgroup$ – user65526 Aug 16 '17 at 16:36
  • $\begingroup$ When I say that it is not possible to prove $\vdash \bigcirc A$ for arbitrary $A$, I mean with an empty left-hand side, as required to invoke the ${\to}L$ here. It is true that $\bigcirc B \vdash B$ (I think that's what you meant to write, rather than $B \vdash B$) holds for some $B$, though, in particular for any $B$ of the form $B = \bigcirc C$. $\endgroup$ – Noam Zeilberger Aug 16 '17 at 16:38
  • 2
    $\begingroup$ By the way, if this answers your original question, please don't forget to accept the answer :-) $\endgroup$ – Noam Zeilberger Aug 16 '17 at 23:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.