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