1
$\begingroup$

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?

$\endgroup$

2 Answers 2

3
$\begingroup$

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}).$

$\endgroup$
3
  • $\begingroup$ +1. Note to the OP that the crucial fact here is that "$\Gamma\vdash\Delta$" does not mean that every sentence in $\Delta$ is true whenever every sentence in $\Gamma$ is true. This is to be contrasted with "$\Gamma\models\Delta$." $\endgroup$ Mar 22, 2018 at 17:09
  • $\begingroup$ @NoahSchweber thanks for the pointer I was actually wondering about that. is Γ⊨Δ a valid sequent? Also I think I am lost on the definition of I, how do I denote those interpretations? $\endgroup$
    – raam86
    Mar 26, 2018 at 8:40
  • 1
    $\begingroup$ @raam86 - the sequent is $\Gamma \vdash \Delta$ or, better: $\Gamma \Rightarrow \Delta$. Thus, according to the def above, $\vDash \Gamma \Rightarrow \Delta$ stay for "the sequent $\Gamma \Rightarrow \Delta$ is valid. $\endgroup$ Mar 26, 2018 at 13:11
1
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

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