Suppose that I have proof tree starting with some statement |- B in a sequent calculus, leading to two premises/leafs |- A. Is it always possible to transform such a proof tree into another proof tree, which only contains one leaf |- A only using standard rules of natural deduction?

More schematically I want to perform the following transformation:

  |- A     |- A                       |- A
------------------    ---->     ---------------
      |- B                            |- B
  • $\begingroup$ what's actually your confusion? Give more explanation with example. Then we are able to help you properly. $\endgroup$
    – A. H.
    Commented Jun 12, 2022 at 10:49
  • $\begingroup$ If I understand your question correctly, it is always possible to apply the trasformation you are point out by virtue of the weaking inference rule of sequent calculus. It states that duplicate consequents or antecedents are immaterial and can consequently by discarded. $\endgroup$
    – Chaos
    Commented Aug 7, 2023 at 19:25

2 Answers 2


"All $A$ are $B$" and "All $B$ are $C$" then "All $A$ are $C$", it is called deductive reasoning.

If two premises are identical then you don't get actually the deduction, you get only the implication.

For example "All $A$ are $B$" then you get the implication "some $A$ are $B.$" "No $A$ are $B$" you get the implication "some $A$ are not $B.$"

  • 1
    $\begingroup$ I'm not familiar with the formalism used in the question (I don't know what sequent calculus is), but $\forall a \in A, a \in B$ does not imply $\exists a \in A, a \in B$. Also, $\not\exists a \in A, a \in B$ does not imply $\exists a \in A, a \not\in B$. $\endgroup$
    – Steven
    Commented Jul 12, 2022 at 23:48

If I understand your question, I do not think so. That is, maybe the premise $\mathscr{A}$ is used for multiple things in the proof. Consider the following proof of $\mathscr{B}=(A\rightarrow (B\rightarrow C))\rightarrow (A\wedge B \rightarrow C)$:

$$\rightarrow I_2\cfrac{\rightarrow E\cfrac{\rightarrow E \cfrac{\wedge E \cfrac{[ A\wedge B]^1}{A} \quad [A\rightarrow (B\rightarrow C]^2}{B\rightarrow C} \quad \wedge E \cfrac{[A\wedge B]^1}{B}}{\rightarrow I_1\cfrac{C}{A\wedge B \rightarrow C}}}{(A\rightarrow (B\rightarrow C))\rightarrow ((A\wedge B)\rightarrow C)}$$

As you can see in the above proof we have the formula $\mathscr{A} = A\wedge B$ which is used two times. Though both are omitted by using the rule $\rightarrow I_1$, they really need to be used more than once (One time for deduction of $A$ and one time for deduction of $B$).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.