Sequent calculus LEFT rule for a implies b

Question

Two of us encountered two different solutions for Sequent calculus LEFT rule for a implies b as following:

1. Split( {} |- a, b |- {} )
2. Split( {} |- a, {} |- b )

#2 is in out Exercise solution.

#1 is used by few students who passed VRS (also got a decent grade).

Now I am confused which one is correct. Can you please confirm?

UPDATE

Professor confirmed: #1 is correct

Answer 1

I am afraid that the former VRS students are not right, the correct rule is number 2. You can see that also with the following sequent calculus proof trees generated by the tool, and you can verify them also by proving the following formula valid:

    ((φ → ψ) ∧ Γ → ∆) ↔ ((Γ → φ ∨ ∆) ∧ (ψ ∧ Γ → ∆))

Comments

Professor: one question, you said #2 is valid, but the formula you gave above and the tool output aren't proposing #1 is valid?

---

No, it is number 2. It is the third proof tree from the left where we have a->b on the left side, and this branches into |-a and b|- which is rule #2 you had in question, right?

---

#2 is |-a and |-b, both on right side
#1 is |-a and b|-, a on right side, bon left side

---

Ah, got it. Then it is indeed #1, and the exercise solution is wrong.