Why does the inference rule of negation moves a term to the other side of the turnstile

Question

the excellent tutorial http://logitext.mit.edu/tutorial presents the negation inference rule like so:

\begin{align} \frac{\Gamma \vdash A, \Delta}{\Gamma, \lnot A \vdash \Delta} \lnot_L \end{align}

and

\begin{align} \frac{\Gamma, A \vdash \Delta}{\Gamma \vdash \lnot A, \Delta} \lnot_R \end{align}

It's elegant and reminds of algebra but I can't convince myself of the first example truthiness.

The proposition itself seems impossible A and not A implies A? Isn't the above a contradiction?

Answer 1

They must be understood "semantically": intuitively, a sequent $A_1,\ldots,A_m \vdash B_1,\ldots, B_n$ means: if $A_1 \land \ldots \land A_m$, then $B_1 \lor \ldots \lor B_n$.

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 if it is satisfied in every interpretation.

The inference rules must be sound, i.e. they must derive true conclusion from true premises.

Consider now the first rule:

$(\lnot \text{left}) \ \ \ \ \dfrac{\Gamma \vdash \Delta, A}{\lnot A, \Gamma \vdash\Delta};$

forgetting about the contexts ($\Gamma$ and $\Delta$), if the upper sequent is true in $\mathfrak I$, this means that $A$ is true, and thus $\lnot A$ is false.

The same for $(\lnot \text{right}).$

Answer 2

The "design intent" of the classical sequent calculus is that the sequent $$A_1,\ldots,A_m\vdash B_1,\ldots,B_n$$ should be derivable if and only if $$ \neg A_1 \lor \cdots \lor \neg A_m \lor B_1 \lor \cdots \lor B_n $$ is logically valid.

Viewed in this light, passing between $\Gamma,A\vdash \Delta$ and $\Gamma\vdash \neg A,\Delta$ does not change the correctness condition at all, so it is reasonable that they should be derivable from each other.

And passing between $\Gamma\vdash B,\Delta$ and $\Gamma,\neg B\vdash \Delta$ doesn't change the meaning of the correctness criterion, if we accept that $\neg\neg B$ has the same meaning as $B$ itself.