# Sequent calculus for classical propositional logic without ⊤ and ⊥

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}$$?

• 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. Jul 13, 2022 at 14:39
• Yes, with the two rules I proposed in the question, that is? Jul 13, 2022 at 14:40
• See The system LK. Jul 13, 2022 at 14:50

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$$

• Comprehensive! Thanks! Jul 16, 2022 at 2:25