# Some minimal insightful example for the distinction between internal vs external logic of a Gentzen system?

Definition (Internal logic) An argument from premises to conclusions is valid in the internal logic of a sequent system iff the sequent G ⇒ D is derivable in that system.

Definition (External logic) An argument from premises to conclusions is valid in the external logic of a sequent system iff the sequent ⇒ D is derivable in the new sequent system arrived at by adding initial sequents ⇒ γ for every γ ∈ G to the original system.

But it's rather unclear to me why this distinction matters, especially why one would want to consider the latter definition. Apparently these concepts were introduced in the context of linear logic, but can someone give a less complicated but still insightful example why the distinction matters (and is desirable to consider the latter "external" notion as well)?

In the external logic it looks like an "extra / external" deduction-theorem equivalent is being added. Is this what's happening?