Elimination of duplicate premise

Question

Suppose that I have a proof tree starting with some statement |- B in a sequent calculus, leading to two premises/leaves |- 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

• user150715: what's actually your confusion? Give more explanation with example. Then we are able to help you properly.
• Chaos: 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.

Answer 1

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$).

Answer 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.$"

• Steven: 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$.