0
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ $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 $\endgroup$
    – Ten O'Four
    Nov 19, 2021 at 5:37

1 Answer 1

3
$\begingroup$

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.

$\endgroup$
6
  • 1
    $\begingroup$ @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)"? $\endgroup$
    – joseville
    Nov 19, 2021 at 14:28
  • 1
    $\begingroup$ @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) $\endgroup$
    – Z. A. K.
    Nov 19, 2021 at 14:31
  • 1
    $\begingroup$ 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 $\endgroup$
    – joseville
    Nov 19, 2021 at 14:38
  • 1
    $\begingroup$ That is correct. $\endgroup$
    – Z. A. K.
    Nov 19, 2021 at 14:41
  • 1
    $\begingroup$ 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. $\endgroup$
    – Z. A. K.
    Nov 19, 2021 at 16:59

You must log in to answer this question.

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