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

I've read the following:

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?

## 1 Answer

I enjoyed reading the paper you linked, but I can only offer a tentative response, since I have only a passing acquaintance with the subject matter.

The internal logic of a proof system is concerned with whether a given conclusion is the consequence of the premises, while the external logic is concerned with whether the conclusion, considered as a theorem, follows from the premises, also considered as theorems. (Pp. 1070-71) Internal logic is concerned with inferences, external logic with metainferences.

The distinction between internal and external logic relates to proof systems, rather than to a logic itself. A given logic may have several distinct proof systems, and the consequence relation for the external logics of those proof systems may differ. The authors give as an example that LK and LK- are both proof systems for classical logic, but their external consequence relations differ. (P. 1072)

For some logics, including classical logic, there exists some proof system such that the external logic contains the internal logic, i.e. for every inference that is provable in the internal, the corresponding external metainference is also provable. For other logics this does not hold. (P. 1073)

The significance of this in the context of the paper is that the authors are arguing against a paper by Barrio, et al, who claim that two logics LP+ and ST+ are effectively equivalent because LP+ is the external logic of ST+. The authors counter this by pointing out firstly that one cannot speak of the external logic of ST+ but only of the external logic of some proof system for it, and secondly that ST+ has no proof system such that its internal and external logics agree. (Pp. 1073-75) Hence in effect the logic ST+ is quite distinct from any external logic of any proof system for it, and so any such external logic should be regarded as a different logic. This allows room for ST+ to be understood as a logic that is intermediate between classical logic and the paraconsistent logic LP+.