1
$\begingroup$

Is there a standard multiple-conclusion sequent calculus for classical propositional logic in the language $\{\neg, \wedge, \vee, \to, \leftrightarrow\}$?

Usually $\leftrightarrow$ is excluded, and often one of $\to$ or $\neg$ is excluded in favour of being defined in terms of the other connectives. It's straightforward enough to add any of these back to a system that doesn't use them.

It's also standard to include rules for $\top$ and $\bot$; how can these be safely removed or replaced? Maybe with $\frac{}{\Gamma, \, A, \, \neg A \; \vdash \; \Delta}$ and $\frac{}{\Gamma \; \vdash \; \Delta, \, A, \, \neg A}$?

$\endgroup$
3
  • $\begingroup$ The answer is yes; see Gaisi Takeuti, Proof Theory (Dover, 2nd ed. 1987), based on Gentzen's original sequent calculus. The rules for negation are: $\dfrac {\Gamma \to \Delta, A}{\lnot A, \Gamma \to \Delta}$ and $\dfrac {A, \Gamma \to \Delta}{\Gamma \to \Delta, \lnot A}$ respectively. $\endgroup$ Commented Jul 13, 2022 at 14:39
  • $\begingroup$ Yes, with the two rules I proposed in the question, that is? $\endgroup$
    – jdonland
    Commented Jul 13, 2022 at 14:40
  • $\begingroup$ See The system LK. $\endgroup$ Commented Jul 13, 2022 at 14:50

1 Answer 1

1
$\begingroup$

Is there a standard multiple-conclusion sequent calculus for classical propositional logic in the language $\{¬,∧,∨,→,↔\}$?

Yes! As correctly pointed out by @MauroAllegranza in his comment, in the language $\{\lnot, \land, \lor, \to\}$ a standard sequent calculus for classical propositional logic is system LK, presented in the Wikipedia page (without the rules for quantifiers). Note that that presentation do not consider the connective $\leftrightarrow$. But adding $\leftrightarrow$ to LK is easy: the rules for $\leftrightarrow$ are as follows.

$$ \dfrac{\Gamma, A \vdash B, \Delta \qquad \Gamma', B \vdash A, \Delta'}{\Gamma, \Gamma' \vdash A \leftrightarrow B, \Delta, \Delta'}\leftrightarrow_R \\ \\ \dfrac{\Gamma \vdash A, \Delta \qquad \Gamma', B \vdash \Delta'}{\Gamma, \Gamma', A \leftrightarrow B \vdash \Delta, \Delta'}\leftrightarrow_{L_1} \qquad \dfrac{\Gamma \vdash B, \Delta \qquad \Gamma', A \vdash \Delta'}{\Gamma, \Gamma', A \leftrightarrow B \vdash \Delta, \Delta'}\leftrightarrow_{L_2} $$

Why are the rules for $\leftrightarrow$ like this? We now that the formula $A \leftrightarrow B$ is logically equivalent to $(A \to B) \land (B \to A)$. So, if we exclude $\leftrightarrow$ from the language by defining $A \leftrightarrow B$ as a abbreviation for $(A \to B) \land (B \to A)$, it is natural to expect that the rule $\leftrightarrow_R$ can be simulated in LK for $\{\lnot, \land, \lor, \to\}$ by only using the rules $\to_R$ and $\land_R$ (technically, this means that the rule $\leftrightarrow_R$ is derivable from $\to_R$ and $\land_R$). And similarly, it is natural to expect that $\leftrightarrow_L$ can be simulated in LK for $\{\lnot, \land, \lor, \to\}$ by only using the rules $\to_L$ and $\land_L$. Let us see that this is the case for both $\leftrightarrow_R$ and $\leftrightarrow_L$.

  • Derivability of $\leftrightarrow_R$: we show that from the sequents $\Gamma, A \vdash B, \Delta$ and $ \Gamma', B \vdash A, \Delta'$ is it possible to derive the sequent $ \Gamma, \Gamma' \vdash (A \to B) \land (B \to A), \Delta, \Delta'$ by only using the rules $\to_R$ and $\land_R$.

$$ \dfrac{\dfrac{\Gamma, A \vdash B, \Delta}{\Gamma \vdash A \to B, \Delta}\to_R \qquad \dfrac{\Gamma', B \vdash A, \Delta'}{\Gamma' \vdash B \to A, \Delta'}\to_R}{\Gamma, \Gamma' \vdash (A \to B) \land (B \to A), \Delta, \Delta'}\land_R $$

  • Derivability of $\leftrightarrow_{L_1}$: we show that from the sequents $\Gamma \vdash A, \Delta$ and $ \Gamma', B \vdash \Delta'$ is it possible to derive the sequent $ \Gamma, \Gamma', (A \to B) \land (B \to A) \vdash \Delta, \Delta'$ by only using the rules $\to_L$ and $\land_{L_1}$.

$$ \dfrac{\Gamma \vdash A, \Delta \qquad\qquad \Gamma', B \vdash \Delta'}{\dfrac{\Gamma, \Gamma', A \to B \vdash \Delta, \Delta'}{\Gamma, \Gamma', (A \to B) \land (B \to A) \vdash \Delta, \Delta'}\land_{L_1}}\to_L $$

  • Derivability of $\leftrightarrow_{L_2}$: we show that from the sequents $\Gamma, A \vdash \Delta$ and $\Gamma' \vdash B, \Delta'$ is it possible to derive the sequent $ \Gamma, \Gamma', (A \to B) \land (B \to A) \vdash \Delta, \Delta'$ by only using the rules $\to_L$ and $\land_{L_1}$.

$$ \dfrac{\Gamma, A \vdash \Delta \qquad\qquad \Gamma' \vdash B, \Delta'}{\dfrac{\Gamma, \Gamma', B \to A \vdash \Delta, \Delta'}{\Gamma, \Gamma', (A \to B) \land (B \to A) \vdash \Delta, \Delta'}\land_{L_2}}\to_L $$


often one of → or ¬ is excluded in favour of being defined in terms of the other connectives

Right, but pay attention that $\lnot A$ can be defined in terms of the other connectives only if they include $\bot$ (falsehood). The natural way to define $\lnot A$ is $A \to \bot$ (and the rules $\lnot_R$ and $\lnot_L$ are derivable from the rules for $\to$ and $\bot$ in LK, see here), and it can be proved that in the language $\{\land, \lor, \to, \leftrightarrow\}$ the connective $\lnot$ cannot be expressed.


It's also standard to include rules for ⊤ and ⊥; how can these be safely removed or replaced?

On the sequent calculus, the rules for $\bot$ and $\top$ can be formulated as follows.

$$ \dfrac{}{\Gamma, \bot \vdash \Delta}\bot_L \qquad\qquad \dfrac{\Gamma \vdash \Delta}{\Gamma \vdash \bot, \Delta}\bot_R \\ \dfrac{\Gamma \vdash \Delta}{\Gamma, \top \vdash \Delta}\top_L \qquad\qquad \dfrac{}{\Gamma \vdash \top, \Delta}\top_R $$

"Safely removing" and "replacing" $\bot$ and $\top$ means to find a formula logically equivalent to $\bot$ and $\top$, respectively, such that the rules for $\bot$ and $\top$ are derivable in LK for $\{\lnot, \land, \lor, \to\}$.

We can define $\bot$ as the formula $A \land \lnot A$ (for $A$ whatsoever), and $\top$ as the formula $A \lor \lnot A$ (for $A$ whatsoever).

  • Derivability of $\bot_L$: we show that (from no assumption) it is possible to derive the sequent $\Gamma, A \land \lnot A \vdash \Delta$ in LK (restricted to $\{\lnot, \land\}$).

$$ \dfrac{\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{}{A \vdash A}ax}{A, \lnot A \vdash}\lnot_L}{A \land \lnot A, \lnot A \vdash}\land_{L_1}}{A \land \lnot A, A \land \lnot A \vdash}\land_{L_2}}{A \land \lnot A \vdash}ctr_L}{\Gamma, A \land \lnot A \vdash}wk_L}{\Gamma, A \land \lnot A \vdash \Delta}wk_R $$

  • Derivability of $\bot_R$: we show that from the sequent $\Gamma \vdash \Delta$ it is possible to derive the sequent $\Gamma \vdash A \land \lnot A, \Delta$ in LK.

$$ \dfrac{\Gamma \vdash \Delta}{\Gamma \vdash A \land \lnot A, \Delta}ctr_R $$

  • Derivability of $\top_L$: we show that from the sequent $\Gamma \vdash \Delta$ it is possible to derive the sequent $\Gamma, A \lor \lnot A \vdash \Delta$ in LK.

$$ \dfrac{\Gamma \vdash \Delta}{\Gamma, A \lor \lnot A \vdash \Delta}ctr_L $$

  • Derivability of $\top_R$: we show that (from no assumption) it is possible to derive the sequent $\Gamma \vdash A \lor \lnot A, \Delta$ in LK (restricted to $\{\lnot, \lor\}$).

$$ \dfrac{\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{}{A \vdash A}ax}{\vdash A, \lnot A}\lnot_R}{\vdash A \lor \lnot A, \lnot A}\lor_{L_1}}{\vdash A \lor \lnot A, A \lor \lnot A}\lor_{L_2}}{\vdash A \lor \lnot A}ctr_R}{\Gamma \vdash A \lor \lnot A }wk_L}{\Gamma \vdash A \lor \lnot A, \Delta}wk_R $$

$\endgroup$
1
  • $\begingroup$ Comprehensive! Thanks! $\endgroup$
    – jdonland
    Commented Jul 16, 2022 at 2:25

You must log in to answer this question.

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