- (red) The rule makes sense to me for ND but not for SC. In SC it says "if $\Gamma,\varphi$ proves $\Delta$ then $\neg\varphi,\Delta$".
So I guess the comma on the right of $\vdash$ must be read as an OR.
(And comma on the left means AND?)
Yes, that's correct. From the post linked in the comments:
The naive interpretation of a sequent $A_1, \ldots, A_n \vdash B_1, \ldots, B_m$ is that the conjunction of the $A$'s implies the disjunction of the $B$'s:
$\vdash A_1 \land \ldots \land A_n \rightarrow B_1 \lor \ldots \lor B_m$
Using the fact that $A \to B$ is equivalent to $\neg A \lor B$, we can re-write this as:
$\vdash \neg(A_1 \land \ldots \land A_n) \lor B_1 \lor \ldots \lor B_m$
And this is equivalent to
$\vdash \neg A_1 \lor \ldots \lor \neg A_n \lor B_1 \lor \ldots \lor B_m$
All these derivability claims are equivalent in the strong sense that any one derivation can be tarnsformed into one of the others, that is, we have the so-called deduction theorem
$$A_1, \ldots, A_n \vdash B_1, \ldots, B_m \iff \vdash \neg A_1 \lor \ldots \lor \neg A_n \lor B_1 \lor \ldots \lor B_m$$
So a sequent can be thought of as a large disjunction, where the premise formulas are negated and the conclusion formulas are positive.
If a formula occurs on the left-hand side of the sequent, it can be thought of as negated (in the disjunction), and if it occurs on the right-hand side of the sequent, it can be thought of as positive (in the disjunction).
So by switching sides, you effectively negate and unnegate the formula $\phi$: Moving $\phi$ from the (negative) LHS of the sequent to the (positive) RHS gives you $\neg \phi$. Together with the fact that an empty RHS corresponds to an empty disjunction, and the observation that an empty disjunction behaves like a contradiction ($\bot$), this motivates the rule in question.
- (orange) Aff stands for affaiblissement = weakening. So if the R.H.S comma is an OR then I guess there is no problem: "if $\Gamma$
proves $\Delta$ then $\Gamma$ proves $\varphi$ or $\Delta$"
Exactly.
- (yellow) I realize now that this is also OK, since $\varphi$ or $\Delta$ is true and $\neg\varphi$ is in the hypothesis, $\Delta$ must
be true
Yes, see above.
- (blue) In general, SC rules often seem to be the same as ND rules but with $,\Delta$ on the right. Why is that?
That's because sequent calculus, unlike ND, allows for more than one conclusion formula. In general, we can have arbitrarily many formulas $B$ on the right-hand side of our sequent, while rules only manipulate one. To account for the fact that before and after the rule application there might still be other formulas on the RHS of the sequent, we summarize these formulas by $\Delta$. Note that $\Gamma$ and $\Delta$ can be empty.
- SC $\textit{Aff}_g$: I assume that the L.H.S. comma in SC means AND so why from $\Gamma\vdash\Delta$ can we deduce $(\Gamma$ and
$\varphi)\vdash\Delta$? I guess if we know that $\Gamma$ by itself
proves $\Delta$ then knowing $\Gamma$ and $\varphi$ doesn't hurt. It's
just weird because I know that in ND,
$\Gamma,\varphi=\Gamma\cup\{\varphi\}$ (and a L.H.S comma is also
AND). This makes sense but is weird because I'm used to treat the
union of objects as OR (from probability courses)...
Your intuition is right. This property is called monotonicity: If from a set of premises $\Gamma$ we can infer $\Delta$, then adding more knowledge to the premises doesn't destroy that previous knowledge. If from "If I drop my pencil, it will hit the ground" and "I dropped my pencil" I can infer "My pencil hit the ground", then I shouldn't lose that inference just because I additionally know that "Unicorns like asparagus", and neither if I know that "Unicorns don't like asparagus". The apparent contradiction with unions usually being read as disjunctive is hopefully resolved by the fact the formulas on the (negative) LHS of the sequent can be read as a disjunction of negations.
What are the roles of SC and ND in minimal, intuitionistic and
classical logic? As I understand it, min, int, cl. logics use ND. So
what's the point of SC?
And why do we need ND and SC?
These are quite broad question that can't be comprehensively answered within an SE post, so let me just say this much:
Minimal and intuitionistic logic certainly do know sequent calculus; it's just a matter of modfifying the permitted sequents and rules: Sequent calculus for intuitionistic and minimal logic can be obtained by simply restricting oneself to sequents with at most one and, respectively, exactly one formula on the right-hand side, and modifying the rules accordingly.
And while one doesn't "need" more than one syntactic calculus in the sense of guaranteeing the existence of a derivation for any semantic tautology (given that ND and SC for classical logic are equilvalent in this respect by completeness), different calculi have different proof-theoretic properties, and SC has some interesting features about the way derivations are built up and things one can "see" in a proof that ND lacks and vice versa. ND more closely resembles the way mathematicians would argue naturally (hence the name); SC is nice because assumptions are kept locally inside a sequent rather than scattered over leaves in a derivation tree.
A discussion of both can be found in the book linked by Mauro Allegranza in the comments.
The Wikipedia article on sequent calculus also gives a good overview.
Best Answer
What you did so far goes in the right direction. Now, how to prove the sequent $\lnot A \lor \lnot B, \, A \land B \vdash \bot $ where you get stuck?
Let us first consider the problem from an informal point of view. Proving the sequent $\lnot A \lor \lnot B, \, A \land B \vdash \bot $ intuitively means that a contradiction must emerge from the assumptions $\lnot A \lor \lnot B$ and $A \land B$, using the inference rules of natural deduction listed here (pp. 7-8). This is where the rule $\lor_\mathrm{elim}$ plays a crucial role. From the assumption $\lnot A \lor \lnot B$, it follows that there are two cases:
either $\lnot A$ holds, but this is in contradiction with the fact $A$ holds ($A$ is derived from the assumption $A \land B$),
or $\lnot B$ holds, but this is in contradiction with the fact $B$ holds (again, $B$ is derived from the assumption $A \land B$).
In both cases, we have the contradiction we are looking for.
Formally, a rigorous derivation in natural deduction using the inference rules listed here (pp. 7-8) is below. For the sake of readability, I split the derivation in three parts. The first one below is the "bottom" part of the derivation. You have to imagine that the derivation $\Pi_A$ is above the sequent $\lnot A \lor \lnot B, \, A \land B, \, \lnot A \vdash \bot$, and that the derivation $\Pi_B$ is above the sequent $\lnot A \lor \lnot B, \, A \land B, \, \lnot B \vdash \bot$.
\begin{align} \dfrac {\overline{\lnot A \!\lor\! \lnot B, A \!\land\! B \vdash \lnot A \!\lor\! \lnot B}^\mathrm{hyp} \ \overset{\Pi_A}{\lnot A \!\lor\! \lnot B, A \!\land\! B, \lnot A \vdash \!\bot} \ \ \ \overset{\Pi_B}{\lnot A \!\lor\! \lnot B, A \!\land\! B, \lnot B \vdash \!\bot}} {\dfrac {\lnot A \lor \lnot B, \, A \land B \vdash \bot} {\dfrac {\lnot A \lor \lnot B \vdash \lnot (A \land B)} {\vdash (\lnot A \lor \lnot B) \to \lnot (A \land B)} \to_\mathrm{intro} } \lnot_\mathrm{intro} }\! \lor_\mathrm{elim} \end{align} where \begin{align} \Pi_A = \ \dfrac {\dfrac{}{\lnot A \lor \lnot B, \, A \land B, \, \lnot A \vdash \lnot A}^\mathrm{hyp} \quad \dfrac {\overline{\lnot A \lor \lnot B, \, A \land B, \, \lnot A \vdash A \land B}^\mathrm{hyp}} {\lnot A \lor \lnot B, \, A \land B, \, \lnot A \vdash A} \land_\mathrm{elim} } {\lnot A \lor \lnot B, \, A \land B, \, \lnot A \vdash \bot} \lnot_\mathrm{elim} \end{align} and \begin{align} \Pi_B = \ \dfrac {\dfrac{}{\lnot A \lor \lnot B, \, A \land B, \, \lnot B \vdash \lnot B}^\mathrm{hyp} \quad \dfrac {\overline{\lnot A \lor \lnot B, \, A \land B, \, \lnot B \vdash A \land B}^\mathrm{hyp}} {\lnot A \lor \lnot B, \, A \land B, \, \lnot B \vdash B} \land_\mathrm{elim} } {\lnot A \lor \lnot B, \, A \land B, \, \lnot B \vdash \bot}~\lnot_\mathrm{elim} \end{align}