0
$\begingroup$

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
Improve this question
$\endgroup$
2
  • $\begingroup$ what's actually your confusion? Give more explanation with example. Then we are able to help you properly. $\endgroup$
    – user19121278
    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
    Aug 7 at 19:25

2 Answers 2

Reset to default
0
$\begingroup$

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

Improve this answer
$\endgroup$
1
  • 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
    Jul 12, 2022 at 23:48
0
$\begingroup$

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

Improve this answer
$\endgroup$

Your Answer

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

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