Negation Inference with Gentzen Natural Deduction and Sequents?

Question

I'm trying to understand the negation rules of this system.

Wiki's page on Sequent Calculus claims that from:

${\displaystyle \lnot p,p,q\vdash r}$

the following is inferred:

${\displaystyle p,q\vdash p,r}$

Can anyone explain how this rule works?

Being confused how the contradictory conditional premises $p$ and $\neg p$ result in this form, I consulted Investigations in Logical Deduction by Gentzen 1935.

Here are the relevant definitions of the rules by Gentzen:

Gentzen Negation (I)introduction (E)limination

Gentzen Description of 'V '^ symbols for negation

Gentzen Full Inference Skhemata

I understand all the other rules in Gentzen's Inference Skhemata, with the exception of negation.

Appreciate anyone's guidance on interpreting how the negation rules work and why Wiki was able to infer above formulas.

Thanks

UPDATE: SOLUTION:

$\lnot p,p,q\vdash r$

reduces to: $(\lnot p \cap p \cap q) \implies r$

$\lnot (p \cap p \cap q) \cup r$

$p \cup \lnot p \cup \lnot q \cup r$

$\lnot p \cup \lnot q \cup p \cup r$

$\lnot (p \cap q) \cup p \cup r$

$(p \cap q) \implies (p \cup r)$

$p,q \vdash p,r$

Answer 1

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:

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

$\neg(A_1 \land \ldots \land A_n) \lor B_1 \lor \ldots \lor B_m$

And this is equivalent to

$\neg A_1 \lor \ldots \lor \neg A_n \lor B1 \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 $p$: Moving $p$ from the (negative) LHS of the sequent to the (positive) RHS gives you $\neg p$, while moving $p$ from the (positive) RHS to the (negative) LHS gives you $\neg p$; and likewise, moving $\neg p$ from the (negative) LHS of the sequent to the (positive) RHS gives you $p$, while moving $\neg p$ from the (positive) RHS to the (negative) LHS gives you $p$.

If this is not convincing yet, consider the limit cases:

• If $A$ is empty, then $B$ is a tautology: $B$ is follows without any premises; the sequent $\vdash B_1, \ldots, B_m$ asserts the validity of the disjunction $B_1 \lor \ldots \lor B_m$.
• If $A$ is empty and $B$ is a singleton $B_1$, then the sequent $\vdash B_1$ asserts the validity of the formula $B_1$.
• If $B$ is empty, then we only have a negation of the premises: From $A_1 \land \ldots \land A_n$ follows "nothing", or more precisely a contradiction (see also below), hence the sequent $A_1, \ldots, A_n \vdash$ asserts the invalidity of the conjunction $A_1 \land \ldots \land A_n$, or equivalently, the validity of $\neg A_1 \lor \ldots \lor \neg A_n$.
• If $B$ is empty, and $A$ is a singleton $A_1$, then the sequents $A_1 \vdash $ asserts the invalidity of the formula $A_1$.
• If both $A$ and $B$ are empty, then the sequent $\vdash$ amounts to an empty disjunction, which is unsatisfiable. (A disjunction of $n$ formulas is true iff at least one out of the $n$ formulas is true - but if there are 0 formulas disjuncted over, then there is none which can make the disjunction true.) Hence, $\vdash$ asserts $\bot$.
• Lastly, the axiom $A \vdash A$ can be thought of as expressing the tautology $\neg A \lor A$, or $A\to A$: If $A$ then $A$; either $\neg A$ or $A$.

So the sequent $\vdash p$ amounts to stating that $p$ is valid, and $p \vdash$ amounts to stating that $p$ is invalid and $\neg p$ is valid. This will again give you the intuition that the left-hand side of a sequent is, in some way, "negative" while the right-hand side of a sequent is "positive". Switching sides therefore amounts to adding or removing a negation.