On page 57 of A Short Introduction to Intuitionistic Logic (Mints), the author provides an exercise: prove that the right implication rule is not invertible.
By an invertible rule he means: if the conclusion sequent can be derived, then the premise sequent can be derived.
The right implication rule is as follows (the full rule set is on page 54):
ϕ,Γ ⊢ Δ,ψ
---------
Γ ⊢ Δ,(ϕ→ψ)
My feeling is that the proof has something to do with the fact that the implication in the conclusion of the sequent could be the result of an application of the weaken rule, and that psi does not actually follow from phi. Based on that I'm trying to find a choice of phi,psi,Gamma, and Delta, and so that ϕ,Γ ⊢ Δ,ψ is underivable, but that Γ ⊢ Δ is derivable.
However I'm not sure if I'm on the right track because if Γ ⊢ Δ derivable then we can just weaken on the left and right to obtain ϕ,Γ ⊢ Δ,ψ. So I think my idea won't work. What am I missing here?
Thanks.
Edit: I now realize that I was confused about the right implication rule to point that I wrote it incorrectly here! Sorry about that. This was clearly a large part of my confusion about solving this exercise.
The correct rule is:
ϕ,Γ ⊢ ψ
---------
Γ ⊢ Δ,(ϕ→ψ)
Edit2: After revisiting the problem with respect to the correct implication rule, and the hints, I was able to solve it. Thanks everyone.
Hint: Try when $\Delta$ is not derivable from $\Gamma$, but instead only derivable from $\phi$.
You wish to show that something of the form $\Gamma,\phi\vdash\Delta,\psi$ may be acceptable, but $\Gamma\vdash\Delta,\phi\to\psi$ is not in an intuitionistic framework. Therefore you do not wish to examine cases where $\Gamma\vdash\Delta$.