Why is there no conditional inference rule in Sequent Calculus of these forms?

79 Views Asked by At

I'm wondering why sequent calculus doesn't have rules like these (at least in the ones I've come across): $$ \Gamma \vdash A \rightarrow B, \Pi \qquad \Delta \vdash A, \Sigma \over \Gamma, \Delta \vdash B, \Pi, \Sigma $$ And $$ \Gamma, A \rightarrow B \vdash \Pi \qquad \Delta, A \vdash \Sigma \over \Gamma, \Delta, A \rightarrow B, A \vdash \Pi \land B, \Sigma $$ Perhaps they are unnecessary because we can derive the same thing using? But I don't see how as we don't have any rules that involve a conditional on the left or right, above the inference line.

I feel like I'm fundamentally misunderstanding sequent calculus, as I still think in terms of natural deduction.

1

There are 1 best solutions below

3
On BEST ANSWER

If a sentence $P$ holds in first-order classical logic, then you can derive $\vdash P$ using the rules present in the usual Gentzen sequent calculus LK. No other rules are necessary. You don't need to add any extra rules, in particular you don't need to add rules like the one you suggest. That should answer your question.

Why does this hold? Well, the proper explanation depends on which sources you're using, and how these define first-order classical logic in the first place. Some works and authors define first-order classical logic as precisely the things you can prove using the rules of the sequent calculus LK, in which case the statement is trivial. Other authors define first-order classical logic using derivability in another formal proof system, such as a Hilbert system or a system of Natural Deduction: in that case, there will be a proof showing that the derivable sentences in LK and the system used to define first-order logic coincide. Yet other works define first-order logic using some kind of semantics (e.g. a Tarskian model-theoretic semantics): in this case, you'd have a theorem showing that LK is sound and complete for the semantics.

This should answer your titular question: we don't have these rules because we don't need them.

In systems where $\rightarrow$ is a basic connective, not defined in terms of others like $\wedge$ amd $\neg$, the usual rules governing it have the form

$$\frac{\Gamma, A \vdash B, \Delta}{\Gamma \vdash A \rightarrow B, \Delta} $$

and

$$\frac{\Gamma, B \vdash \Delta \:\:\: \Gamma \vdash A, \Delta}{\Gamma, A \rightarrow B \vdash \Delta} $$

instead of the ones you suggest. In calculi where $\rightarrow$ is a defined connective, you don't need separate rules for it, you can just replace it with its definition.

Do you have trouble deriving some specific formula involving $\rightarrow$ in the sequent calculus? If so, you can put it into Logitext and click around to see where you get stuck. If that doesn't help, you can always ask a more specific question here (but make sure you explain clearly which particular presentation of sequent calculus you're using, and reference the textbook where you found it!).

I feel like I'm fundamentally misunderstanding sequent calculus, as I still think in terms of natural deduction.

Alas, based on the question, I suspect so too. I'll give you a few pointers here.

We study the sequent calculus because it makes it easy to analyze proofs. This is accomplished by theorems such as cut-elimination and the subformula property, which ensure that when you're searching for a proof, you don't have to make certain types of "clever guesses".

Let's take a simple example.

You might want to prove logic consistent, by showing that $\vdash X$ for an atomic formula $X$ has no derivation.

When you search for a proof in sequent calculus, you go bottom-up. Starting with the desired conclusion, you try to apply the rules to reach axioms $\Gamma, Y \vdash Y, \Delta$ where some formula $Y$ occurs on both the left and the right of the turnstile.

You can easily show that $\vdash X$ has no derivation which doesn't use the cut rule: such a proof would eventually have to conclude with one or more axiom rules $\Gamma, Y \vdash Y, \Delta$. But the only rules you can apply to an atomic $X$ are weakening and contraction, which always yield sequents of the form $\vdash X, X, \dots, X$, and never let you get a formula on the left of the turnstile at all. But to apply the axiom rule, some formula $Y$ would have to occur on both the left and the right of the turnstile. Since this never happens, $\vdash X$ has no proof that doesn't use the cut rule.

It's much harder to show that $\vdash X$ has no derivation using the cut rule. Recall that the cut rule has the form

$$\frac{\Gamma \vdash A, \Sigma \:\:\: \Delta, A \vdash \Pi}{\Gamma, \Delta \vdash \Sigma, \Pi}\text{cut}$$

Having the cut rule comes in handy when we want to combine proofs together, but turns into a major annoyance when we try to prove that something has no derivation. Maybe we can choose a really clever non-atomic formula $A$ and prove both $\vdash A$ and $A \vdash X$! It's only thanks to Gentzen's Hauptsatz (the cut-elimination theorem), a very difficult result, that we know this cannot happen.

Now notice that your first proposed rule would give rise to the same problem as the cut rule: maybe we could guess some very clever $A$, and prove $\vdash A \rightarrow X$ and $\vdash A$. We don't want such non-analytic rules in our sequent system, and if we had it, our utmost priority would be to show that it's never necessary to use this rule.