false introduction sequent calculus?

Question

I'm proving the following proposition using sequent calculus. I got stuck at the very top line. My thought is that if the both hypothesis inside the curly bracket are true, then it's false. So I think the top line just end there, i.e., no more proof needed.
Is that how the top line works?

$$\dfrac{\dfrac{\{\neg A \vee \neg B , A \wedge B \} \vdash False}{\{ \neg A \vee \neg B\} \vdash \neg (A \wedge B)}}{ \{ \} \vdash (\neg A \vee \neg B) \Rightarrow \neg(A \wedge B)} $$

Answer 1

It's hard to say whether this is a valid proof without knowing the specific proof system you are using. "Sequent calculus" is strictly speaking a style of proof system rather than a particular proof system. That said I would guess that you're most likely using a close relative of Gentzen's original LK system. In this system there is only axiom schema $A\vdash A$ and so only sequents of this form (i.e. sequents where the antecedent and succedent are an identical formula) can appear at the top of a proof. It appears you are also using a false constant so you likely also have a axiom/axiom schema governing this e.g. $\bot \vdash $, but the point is only axioms can go at the start of formal proofs, so you have to look and see what the axioms are in your system.

Your reasoning about the top line is what we call a semantic argument. You're reasoning in terms of truth and falsity and the meanings of the formulas. However a formal proof, in sequent calculus or any other system, is purely syntactic, it's solely about whether at each step the inferences you are making follow the formal rules of the system you are using.

EDIT: Just noticed the title of your question. Note that classical natural deduction systems do not have an introduction rule for $\bot$ (FALSE) since it can never be true. Similarly sequent calculus systems do not have a right intoduction rule for it.

Answer 2

You are trying to prove: $\lnot A \lor \lnot B \vdash \lnot (A \land B)$, which is indeed provable, being valid (it is one of so-called De Morgan's laws).

I think the top line just end there, i.e., no more proof needed.

This is not correct.

A Sequent Calculus proof must start from axioms: $\varphi \vdash \varphi$, and thus - working bottom-up - the proof will end when you reach the axioms:

1. $(\lnot A \lor \lnot B), (A \land B) \vdash$

and then:

2. $(\lnot A \lor \lnot B), A, B \vdash$

Now we unpack the formula $(\lnot A \lor \lnot B)$, generating two upper sequents:

3. $\lnot A, A,B \vdash$ and $\lnot B,A,B \vdash$

from which we get the axioms (using Weakening):

4. $A \vdash A$ and $B \vdash B$.

Now the derivation is complete.

---

You have to note that in Sequent Calculus the empty sequent "means" (its sematic value is): $\bot$.

There is no introduction rule for $\bot$: the calculus is consistent.

You can use the defintion of $\lnot A$ as $A \to \bot$ to derive e.g.

$\dfrac {\Gamma , A \vdash \bot}{\Gamma \vdash \lnot A}$

using the rule for $\to$.