# How does one write a sequent calculus sequent with an empty cedent?

How does one write $$P \land Q$$ in sequent calculus? This would require an empty succedent/consequent?

$$P, Q \vdash$$

or

$$P, Q \vdash \bot$$

?

An empty consequent represents the disjunction ($$\lor$$) of zero items, which I take to be false ($$\bot$$)? Is this correct?

What about, how does one write $$\lnot P \lor \lnot Q$$? This would require an empty antecedent?

$$\vdash \lnot P, \lnot Q$$

or

$$\bot \vdash \lnot P, \lnot Q$$

?

An empty antecedent represents the conjunction ($$\land$$) of zero items, which I take to be false ($$\bot$$). Is this correct?

Since $$P \land Q \equiv \lnot(\lnot P \lor \lnot Q$$) via DeMorgan's Law, it should be possible to convert the sequent of $$P \land Q$$ into the sequent of $$\lnot(\lnot P \lor \lnot Q)$$, and vice-versa.

I'm using the following terminology:

• antecedent is what's to the left of the turnstile ($$\vdash$$)
• consequent/succedent is what's to the right of turnstile ($$\vdash$$)
• cedent refers to either an antecedent or a consequent
• sequent refers to the "antecedent $$\vdash$$ consequent" as a whole

My goal: to prove DeMorgan's Law using sequent calculus.

EDITED: I had written de Morgan's law incorrectly. Thanks for the corrections.

• $P\land Q\equiv\lnot(\lnot P\lor \lnot Q)$, and, with hypothesis introduction, $P, Q\vdash$ can't occur (i.e., $P\vdash P, Q\vdash Q, P, Q\vdash P\land Q$, and so on Nov 19, 2021 at 5:37

An empty consequent represents the disjunction (∨) of zero items, which I take to be false (⊥)? Is this correct?

The empty disjunction is indeed false, so the sequent $$P,Q \vdash$$ has the same intuitive meaning as $$P, Q \vdash \bot$$ (namely that it is not the case that both $$P$$ and $$Q$$ hold). However, the sequents $$P,Q \vdash$$ and $$P,Q \vdash \bot$$ are not the same sequents.

Why? First of all, not all variants of sequent calculus permit the use of the constants $$\top$$ and $$\bot$$. You can use them only if your sequent calculus actually has rules for these constants (such as $$\bot L$$, the left rule for $$\bot$$). Even if your particular sequent calculus supports these constants, the sequents $$P,Q \vdash$$ and $$P,Q \vdash \bot$$ are still not the same. The right-hand side of the first sequent is empty, while the right-hand side of the second sequent contains the formula $$\bot$$. This means that these two sequents support different reasoning rules. If your rules say that you should get the sequent $$P,Q \vdash$$, then you cannot assume that you have $$P, Q \vdash \bot$$ instead - and vice versa.

An empty antecedent represents the conjunction (∧) of zero items, which I take to be false (⊥). Is this correct?

This is not correct at all. The empty conjunction is true, i.e. $$\top$$ (see this related question or this quora post). Again, the sequents $$\top \vdash P, Q$$ and $$\vdash P, Q$$ have the same intuitive meaning, but different form. If your rules say that you should get the sequent $$\vdash P, Q$$, you cannot assume that you have $$\top \vdash P,Q$$ instead.

Since P∧Q≡¬P∨¬Q, via DeMorgan's Law, it should be possible to convert the sequent of P∧Q into the sequent of ¬P∨¬Q, and vice-versa.

This is very, very wrong. Intuitively, $$P \wedge Q$$ says that both $$P$$ and $$Q$$ hold, while $$\neg P \vee \neg Q$$ says that at least one of $$P$$ or $$Q$$ fails. They are clearly not the same thing, and de Morgan's law certainly does not say that they are the same thing.

As for the "actual" de Morgan's laws, $$\vdash (P \wedge Q) \leftrightarrow \neg (\neg P \vee \neg Q)$$ and $$\vdash (P \vee Q) \leftrightarrow \neg (\neg P \wedge \neg Q)$$, you can prove these straightforwardly in the sequent calculus. If you have left and right rules for $$\neg, \vee, \wedge, \rightarrow$$, then you will never need to use $$\bot$$ or $$\top$$ in these derivations.

Once you get to the cut-elimination theorem, you'll be able to use it to convert between derivations of sequents containing $$P \wedge Q$$ and derivations of sequents containing $$\neg (\neg P \vee \neg Q)$$. Similarly, you'll be able to convert between proofs of $$P \wedge Q \vdash \bot$$ and $$P \wedge Q \vdash$$. Starting from a proof of $$P \wedge Q \vdash \bot$$, you'll be able to cut against a trivial proof of $$\bot \vdash$$ to obtain a proof of $$P \wedge Q \vdash$$. Starting from a proof of $$P \wedge Q \vdash$$, you'll be able to write a proof of $$P \wedge Q \vdash \bot$$ by using the weakening rule on the right.

• @thanks for the detailed answer and the correction. re: "𝑃,𝑄⊢ has the same intuitive meaning as 𝑃,𝑄⊢⊥ (namely that 𝑃 and 𝑄 are both false)" I take that to mean $(P \land Q) \rightarrow \bot$ which in order to be true, requires $P \land Q$ to be false, i.e. $\lnot(P \and Q) \equiv \lnot Q \lor \lnot P$. So wouldn't it be more like (namely that at least one of $P$ or $Q$ is false)"? Nov 19, 2021 at 14:28
• @joseville Thanks for catching that, that was very misleading wording on my part! Indeed, as you wrote, the intuitive meaning is of course "it is not the case that both P and Q are true", rather than "both P and Q are not true". Will fix (now done) Nov 19, 2021 at 14:31
• no problem. Another clarification. re: $$\vdash (P \wedge Q) \leftrightarrow \neg (\neg P \vee \neg Q)$$. I'm newish to using $\vdash$ so just want to confirm that that should be parsed as $$\vdash ((P \wedge Q) \leftrightarrow \neg (\neg P \vee \neg Q))$$, right? i.e. $\vdash$ has the highest precedence? en.wikipedia.org/wiki/Logical_connective#Order_of_precedence Nov 19, 2021 at 14:38
• That is correct. Nov 19, 2021 at 14:41
• Alas, I don't know any good free online resources. You may find the relevant chapters of the freely available textbook Proofs and Types useful, combined with other resources you find online, but I don't think the book is a suitable introduction in itself. Nov 19, 2021 at 16:59