A sequent calculus proof

608 Views Asked by At

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.

1

There are 1 best solutions below

9
On BEST ANSWER

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