Is cut rule an instance of left implication?

252 Views Asked by At

I'm working with a sequent caluculus system where cut-rule is defined as follows:

$$\begin{array}{lcr} \Gamma \Rightarrow \varphi, \Delta & & \Gamma, \varphi \Rightarrow \Delta \\ \hline & \Gamma \Rightarrow \Delta \\ \end{array} $$

And left implication as follows:

$$\begin{array}{lcr} \Gamma \Rightarrow \beta_1, \Delta & & \Gamma, \beta_2\Rightarrow \Delta \\ \hline & \Gamma, \beta_1\rightarrow\beta_2 \Rightarrow \Delta \\ \end{array} $$

So, by applying left implication to the two sequents $\Gamma \Rightarrow \varphi, \Delta$ and $\Gamma, \varphi \Rightarrow \Delta$ we then get $\Gamma, \varphi\rightarrow\varphi\Rightarrow \Delta$. Now, since $\varphi\rightarrow\varphi$ is clearly a tautology, it shouldn't really matter if it belongs or not to our set of premises. (Am I right on this? My intuition is that by adding some tautology in the left side of a sequent we are not adding any useful information that could be used in a deduction)

I was thus wondering whether one can consider the cut rule as a way of getting rid of these tautologies in the set of premisses, and whether the cut-elimination results can be somehow considered as reducing cut to left implication.

1

There are 1 best solutions below

0
On BEST ANSWER

Tautology is usually used for a semantic notion, but we need to show that the proof system corresponds to the semantics. It is a meta-logical result that $\Gamma,\varphi\Rightarrow\Delta$ and $\Gamma\Rightarrow\Delta$ are inter-derivable when $\varphi$ is a tautology, but the proof of this is to show that there is a derivation from the first to the second (and the other way, but that's just left weakening). If we identify tautologies with formulas $\varphi$ for which we can derive $\cdot\Rightarrow\varphi$ (which is something that would need to be proven, unless this is what you intended "tautology" to mean), then the instance of cut (plus some weakening1), $$\cfrac{\cdot\Rightarrow\varphi\qquad\Gamma,\varphi\Rightarrow\Delta}{\Gamma\Rightarrow\Delta}$$ lets us remove tautologies from the premises. So you are correct that cut is what lets us "get rid of the tautologies in the premises".

I'm not sure what you mean by "reducing cut to left implication". Cut is a structural rule and is arguably more "fundamental" than left implication, so it's not clear why we would want to "reduce" it to that. The idea that cut captures is that we can reuse results that we've already proven. Cut-elimination is the process of inlining the proof of a result everywhere it is referenced. This doesn't have much to do with the $\to$ connective.

1 Often cut is formulated as $$\cfrac{\Gamma\Rightarrow\varphi,\Delta\qquad\Gamma',\varphi\Rightarrow\Delta'}{\Gamma,\Gamma'\Rightarrow\Delta,\Delta'}$$ which avoids the need for extra weakening to make the contexts line up.