1
$\begingroup$

In Gentzen system, there is an inference rule such that one can deduce $\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B}$ from $\Gamma, \mathfrak{A} \to \Delta, \mathfrak{B}$.

Can we, in reverse way, deduce $\Gamma, \mathfrak{A} \to \Delta, \mathfrak{B}$ from $\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B}$? More precisely,

  1. In Gentzen sequent calculus, is there an inference rule of the form below? \begin{align} \frac{\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B}}{\Gamma, \mathfrak{A} \to \Delta, \mathfrak{B}}* \end{align}

  2. In Gentzen sequent calculus, is there a derivation of $\Gamma,𝔄 \to \Delta,𝔅$ from the assumption $\Gamma \to \Delta,𝔄 \supset 𝔅$? In other words, is the rule ($*$) derivable in Genztzen sequent calculus?

$\endgroup$
1
$\begingroup$

Mauro Allegranza's reply correctly answers Point 1 of the question. But the answer to Point 2 of the question is positive. Indeed, the rule $\supset$-right is reversible, which means that the inference rule \begin{align} \frac{\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B}}{\Gamma, \mathfrak{A} \to \Delta, \mathfrak{B}}* \end{align} (i.e. the bottom-up version of the rule $\supset$-right) is derivable in Gentzen sequent calculus: ($*$) is not an inference rule of original Gentzen sequent calculus but it can be "simulated" in Gentzen sequent calculus, i.e. there exists a derivation of $\Gamma, \mathfrak{A} \to \Delta, \mathfrak{B}$ from the assumption $\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B}$, for instance the following \begin{align}\tag{1} \dfrac{\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B} \qquad \dfrac{\dfrac{}{\mathfrak{A} \to \mathfrak{A}}\text{ax} \qquad \dfrac{}{\mathfrak{B} \to \mathfrak{B}}\text{ax}}{\mathfrak{A},\mathfrak{A} \supset \mathfrak{B} \to \mathfrak{B}}\supset\!\!\text{-right} }{\Gamma, \mathfrak{A \to \Delta, \mathfrak{B}}}\text{cut} \end{align}

This entails that if the sequent $\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B}$ is derivable, then $\Gamma, \mathfrak{A} \to \Delta, \mathfrak{B}$ is derivable: given a derivation $\pi$ of $\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B}$, the composition of $\pi$ with the derivation $(1)$ yields a derivation of $\Gamma, \mathfrak{A} \to \Delta, \mathfrak{B}$.

$\endgroup$
2
$\begingroup$

No; in Sequent Calculus you do not "unpack" complex formulae but always build them up from their "components".

The rules for the conditional connective $\supset$ are:

\begin{align} {\cfrac{C, \Gamma \to \Delta, D}{\Gamma \to \Delta, C \supset D} \supset \text {-right}} \end{align}

\begin{align} {\cfrac{\Gamma \to \Delta, C \ \ \ \ \ \ \ D, \Pi \to \Lambda}{C \supset D, \Gamma, \Pi \to \Delta, \Lambda} \supset \text {-left}} \end{align}


An important feature of Sequent Calculus is that the rules are invertible, i.e. we can use them "bottom-up" in a proof-search procedure. In this case, what you are asking is nothing else than $\supset \text {-right}$ read bottom-up.

$\endgroup$
  • $\begingroup$ Thanks! ... Sequent calculus always confuses me... $\endgroup$ – Bram28 Apr 12 '17 at 13:29
  • 1
    $\begingroup$ I think the question in the OP has two possible interpretations. I made them more explicit in my edit. Of course, your answer is correct for question 1. But for question 2. the answer is positive, and I think this was the sense of the OP. I suggest to reopen the question. $\endgroup$ – Taroccoesbrocco Apr 1 '18 at 10:50

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.