0
$\begingroup$

The sequent proof systems I learned only allowed one formula on the right hand side of the sequent, and $\phi_1, \ldots, \phi_n \Rightarrow \psi$ (or ... $\vdash \psi$) is understood as saying that $\psi$ is a logical consequence of (or provable from) $\phi_1, \ldots, \phi_n$.

Now I'm seeing sequent calculus systems with right weakening:

$$\frac{\Gamma\vdash \Delta}{\Gamma\vdash \Delta,A} \text {RW}$$

So I guess $\Gamma\vdash \Delta,A$ has to be saying that at least one of $\Delta,A$ is provable from $\Gamma$ and not that both are. Why is this used?

I assume the notation has some payoff I'm missing, since it seems like sequences of wffs have different meanings based on whether they're in the antecedent or succedent.

$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

The sequent calculus is based on the notation $\Gamma \Rightarrow \Delta$ (or $\Gamma \vdash \Delta$), with $\Gamma, \Delta$ finite (possibly empty) sequences of formulas, called a sequent.

The intuitionistic sequent calculus is obtained with the restriction that $\Delta$ consists of at most one formula.

For the semantics for sequents, see Gaisi Takeuti, Proof Theory (2nd ed - 1987), page 9:

intuitively a sequent $\gamma_1, \ldots, \gamma_m \vdash \delta_1, \ldots, \delta_n$ means :

"if $\gamma_1 \land \ldots \land \gamma_m$, then $\delta_1 \lor \ldots \lor \delta_n$".

Then we have [page 41] :

A sequent $\Gamma \vdash \Delta$ is satisfied [in an interpretation $\mathfrak I$] if either some formula in $\Gamma$ is not satisfied by $\mathfrak I$, or some formula in $\Delta$ is satisfied by $\mathfrak I$. A sequent is valid it it satisfied in every interpretation.

$\endgroup$
3
  • $\begingroup$ I thought that any sequent proof system was considered a sequent calculus, but now I'm thinking that's wrong and is the source of my confusion. I've used a classical sequent proof system that only allowed one formula on the right hand side, and an intuitionistic sequent proof system that also only allowed one formula on the right hand side but had different rules. Are you saying that you get an intuitionistic sequent calculus by just adding the restriction that $\Delta$ consists of at most one formula and not changing the rules beyond that? $\endgroup$
    – Hungry
    Commented Apr 30, 2016 at 21:26
  • 1
    $\begingroup$ @Hungry - yes; the original Gentzen's formulation of sequent calculus derive the intuitionistic version from the classical one only with that restriction. See Takeuti's book for a detailed exposition. There are now many "variants"; see S.Negri & J.von Plato, Structural Proof Theory. $\endgroup$
    – Mauro ALLEGRANZA
    Commented May 1, 2016 at 8:12
  • $\begingroup$ An old post you made about Getzen sequent calculus rules being "upside down" tableaux rules was ENORMOUSLY helpful to me. Funny how tableaux rules seem so natural and Getzen rules seemed bewildering. When I returned to the book I learned tableaux from (Bostock's Intermediate Logic) I realized it actually explicitly goes through the conversion later in the book. And nicely answers my question re: the benefits of allowing multiple formulae on the right—all the combos of rules for signs are complete for all sequents containing only those signs. Otherwise would need neg rules! $\endgroup$
    – Hungry
    Commented May 1, 2016 at 22:42

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .