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.
Best Answer
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.
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.
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.