Sequent calculus: What does it mean to say “choose the sequents from which we can derive some other sequent via the right conjunction rule”

formal-proofslogicpropositional-calculussequent-calculus

My question is probably quite silly really, but I am puzzled what this exercise is asking:

Excercise. Choose all sequents from which we can derive some other sequent via the right-side conjunction rule.

  1. $\color{green}{\lnot (A\land B), \lnot A \vdash A\land B}$ (correct)
  2. $\lnot (A\land B), A \vdash A\land B$
  3. $\color{green}{\lnot (A\land B), \lnot A \vdash \lnot A \land \lnot B}$ (correct)
  4. $\lnot (A\land B), B \vdash \lnot A \land \lnot B$
  5. $\lnot (A\land B), \lnot B \vdash A\land B$

(Source: homework excerise in since-discontinued course, translated)

The correct answers are marked green.

Here is the referenced

Right-side conjunction rule:
$$\cfrac{\Gamma \vdash \mathcal{F}\quad \Gamma \vdash \mathcal{G}}{\Gamma\vdash \mathcal{F}\land \mathcal{G}}$$
where $\mathcal{F}, \mathcal{G}$ are zeroth order formulae, and $\Gamma$ is a list of zeroth order formulae or is empty.

I believe I do understand the basics of Gentzen's sequent calculus. I am aware of the axioms and rules for allowed derivations, including the right-side conjunction rule; the intuition behind the formalisation is also clear. I have derived dozens upon dozens of formulae in sequent calculus (as trees), and proved, for example, the correctness and completeness of sequent calculus wrt tautologies in propositional calculus.

With this in mind,

  • the problem is not how to solve the excercise. Rather, my problem is in understanding what is even being asked in the first place. So: What exactly is the excercise after?

Even with the “correct” answers known, I am admittedly confused. Firstly, the multiple choices are all of the form $\Omega \vdash \mathcal{F} \land \mathcal{G}$ (with varying $\Omega, \mathcal{F}, \mathcal{G}$). One usually uses the right-side conjunction rule to derive sequents of the form $\Omega \vdash \mathcal{F} \land \mathcal{G}$, not use them as “sequents from which” to derive other sequents. Secondly, what are the “some other sequents” which I should check? Others from the multiple-choice list? Other sequents in general?

Perhaps the phrasing of the exercise is a bit off from what is common… Is this a common type of exercise, maybe you can recognize the intended idea behind it? To reiterate, what is the exercise asking for?

EDIT

Here is another exercise of the same type. I also know the “correct” answer(s) to the test excercise but I will omit this information at first. That way I have an elementary check if an answer has the intended interpretation.

Test excercise.
Choose all sequents from which we can derive some other sequent via the left-side conjunction rule.

  1. $\vdash (X \lor \lnot X) \land (Y \lor \lnot Y)$
  2. $Z, X \land Y \vdash \lnot X \lor \lnot Y \lor \lnot Z$
  3. $X \land (Y \lor Z), Y \land (X \lor Z) \vdash X \land Y \land Z$
  4. $\lnot Z \land \lnot X \vdash (Y \lor \lnot Z) \land (\lnot Y \lor \lnot X)$
  5. $X\land Y \vdash X\lor Y$

(Source: homework excerise in since-discontinued course, translated)

Left-side conjunction rule:
$$\cfrac{\Gamma, \mathcal{F}, \mathcal{G} \vdash \mathcal{H}}{\Gamma, \mathcal{F} \land \mathcal{G} \vdash \mathcal{H}}$$
where $\mathcal{F}, \mathcal{G}$ are zeroth order formulae, and $\Gamma$ is a list of zeroth order formulae or is empty.

The correct answers were indeed (spoiler)

2 and 3.

Best Answer

Having the answer, I think I can figure out what the question was intended to be. An application of the right-$\land$ rule needs two premises, and those two premises must have the same set $\Gamma$ of formulas to the left of $\vdash$. The two green sequents have the same formulas to the left of $\vdash$, and no two others on your list of five options do that. So the two green sequents, and only those two, can serve as the two premises in an application of right-$\land$.

Related Question