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.



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


1 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.

  • $\begingroup$ Hi - thanks. Using your suggestion, I solved it with De-Morgan's law. Posted in OP. Does this look correct? $\endgroup$
    – user644059
    Commented May 7, 2019 at 1:42
  • $\begingroup$ @Nick I don't quite understand what you did in your steps 3. and 4.; is should be $p \lor \neg p \lor \neg q \lor r \Rightarrow \neg p \lor \neg \q \lor p \lor r \Rightarrow p, q \vdash p, r$. But be aware that these transformations are just transformations on the meta language level that give another idea of what is going on in the sequents; DeMorgan etc. are not rules that directly underlie the sequent calculus. $\endgroup$ Commented May 7, 2019 at 10:45
  • $\begingroup$ I read your explanation in detail and it is clear in regards to the logic, negative disjunction on the left and positive disjunction on the right and moving (not p) as a positive p to the right. I'm still confused how (not p), p, which are two contradictory premises result in a conclusion where one of them may be asserted out of necessity. Is this a case of law of contradiction? Thanks $\endgroup$
    – user644059
    Commented May 10, 2019 at 5:15
  • $\begingroup$ Because when taking sequents as large disjunctions, $\neg p, p$ are $\lor$-ed, not $\land$-ed. They are not both premises, but $p$ is the premise and $p$ the conclusion, so when writing it as a disjunction, we get $\neg p \lor p$. $\neg p \lor p$, also known as the law of excluded middle, is a tautology in classical logic. That's why it's used as one of the axioms. $\endgroup$ Commented May 10, 2019 at 10:29
  • $\begingroup$ Thanks! Got the last step. (not(p) or not(q) or p or r) -> (not(p or q) or p or r) -> (p and q) -> p or r. $\endgroup$
    – user644059
    Commented May 11, 2019 at 1:46

You must log in to answer this question.