{'fraction_non_alphanumeric': 0.03940554619273786, 'fraction_numerical': 0.009284510494867474, 'mean_word_length': 4.129027188433129, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
The naturality of natural deduction (II). Some remarks on atomic polymorphism

In this paper (which is a prosecution of"The naturality of natural deduction", Studia Logica 2019) we investigate the exact relationship between the Russell-Prawitz translation of intuitionistic propositional logic into intuitionistc second-order propositional logic (System F), and its variant proposed by Fernando Ferreira and Gilda Ferreira into the atomic fragment of System F (System Fat). In the previous paper we investigated the Russell-Prawitz translation via an extended equational theory for System F arising from its categorical semantics. The main result of this paper is that the Russell-Prawitz translation and Ferreira and Ferreira's translation are equivalent modulo this extended equational theory. This result highlights a close connection between our previous work and that of Ferreira and Ferreira. We argue however that the approach obtained by coupling the original Russell-Prawitz translation with our extended equational theory is more satisfactory for the study of proof identity than the one based on System Fat.


Introduction
In (proof-theoretic) semantics investigations of natural deduction, it is common to take the conversions defining normalization as inducing an equivalence relation on derivations.
The equivalence relation induced by these conversions plays an essential role in the categorical semantics of NI, as equivalent derivations are interpreted by the same entity, namely a morphism in a bi-cartesian closed category. For this reason this equivalence relation is sometimes referred to as identity of proofs [3].
Since Russell it is well-known that propositional connectives like conjunction and disjunction can be defined using only implication and propositional quantification. In natural deduction, the derivability-preserving mapping from NI into System F (also referred to as NI 2 , e.g. [17]) is usually called the Russell-Prawitz translation (henceforth RP-translation).
When not only derivability but also the proof identity is considered, the RP-translation is not fully satisfactory. Although the RP-translation preserves the equivalence generated by β-conversions, it fails to preserve both the one generated by η-and γ-conversions. In categorical terms, the interpretation of conjunction and disjunction via the RPtranslation does not satisfy all the laws of the product and coproduct in a bi-cartesian closed category (but only "weak" versions of some of them). We will refer to this fact as the equivalence-preservation problem of the RP-translation.
In a previous paper we discussed a solution to the equivalence-preservation problem obtained by introducing an extended equational theory of NI 2 . 1 Our starting point was the categorical semantics of System F ( [1], [9]), in which derivations in NI 2 are interpreted as natural transformations. We first gave a syntactic formulation of the naturality condition satisfied by these transformations in the form of a particular class of equations (called ε-equations) among derivations of NI 2 . Then we showed that, when the equivalence on NI 2 -derivation is extended with the ε-equations, the RP-translation does preserve the equivalence of NI-derivations.
In a recent series of papers, Ferreira and Ferreira [4,6] proposed to modify the RPtranslation to map NI onto System F at or atomic System F . The latter (to which we will refer to, for uniformity, as NI 2 at ) is the predicative fragment of NI 2 obtained by requiring in each application of the quantifier elimination rule: @XA @E A B{X the formula B (called the witness of the rule application) to be an atomic formula.
The starting point of Ferreira and Ferreira's proposal is the discovery that for some quantified formulas @XA, in particular for those that are the RP-translation of some propositional formula, the unrestricted elimination rule is derivable in NI 2 at . That is, for every formula B of the language of System F , A B{X is derivable in NI 2 at from @XA. The formulas of the form @XA for which this holds are said to enjoy the property of instantiation overflow.
The translation proposed by Ferreira and Ferreira (henceforth FF-translation) does preserve the equivalence generated by η-and γ-conversion ( [5]) for disjunction, without the need of resorting to the admittedly complicated ε-equations.
There are however several aspects of Ferreira and Ferreira's approach that stand in need of clarification. In the present paper, we spell out the exact relationship between the RP-and FF-translation using the notion of equivalence arising from the ε-equations we introduced in our previous paper.
In particular, using the framework developed in our previous work we define an alternative translation of NI into NI 2 at . We then show that given a derivation D in NI, its FF-translation and the alternative translation we propose are β-equivalent derivations in NI 2 at . Moreover, the RP-translation of D and the alternative translation we propose are ηε-equivalent derivations in NI 2 . Thus the RP-and the FF-translation are βηε-equivalent derivations in NI 2 .
In spite of the close connection between our work and Ferreira and Ferreira's, in the conclusive section of the paper we discuss two distinct reasons for claiming that the latter cannot be seen as providing a solution to the equivalence-preservation problem. First, altough it does preserve the equivalence induced by γ-conversions it does not preserve the one induced by the generalization of γ-conversions needed to interpret disjunction as a categorical coproduct. Second, whereas every formula is interderivable with its RPtranslation in the extension of NI 2 with primitive propositional connectives, an anologous result fails for NI 2 at . In Section 2, we introduce the languages and systems we will be concerned with, we recall some notions from our previous paper, and we introduce some notational conventions. In Section 3 we first present Ferreira and Ferriera's translation as well as a variant theoreof suggested by our previous work; then we show that that the our variant of the FF-translation is β-equivalent to the original FF-translation. In Section 4 we show that our modified FF-translation is ηǫ-equivalent to the original RP-translation, and thus that the FF-translation is βηε-equivalent to the RP-translation. In Section 5 we discuss the two reasons for denying that the FF-translation can be taken as a solution to the equivalence preservation problem. In Section 6 we summarize the results of the paper, we draw some connections with related works, and we suggest further directions of investigations.

Preliminaries
As this article is a prosecution of [22], we refer to that article for a fully detailed treatment of the technical notions here employed. To make the present paper as self-contained as possible, definitions of these notions are given in Appendix A-E. In this section we brifely recall these notions, as well as other ones that are well-known from the literature, and we introduce some notational conventions.

Languages and systems
We will be mainly concerned with three natural deduction systems based on three different languages and some restrictions thereof. Given a set of propositional variables V, to be indicated with X, Y , Z, . . . these are defined as: The systems NI 2 at and NI 2_ at are obtained by replacing the rule @E with the following: in which the witness must be an atomic formula. We indicate derivability in NI, NI 2 , . . . with $ NI , $ NI 2 , . . .. Remark 2.1. As in [22], we do not consider^and K, but unless otherwise specified the results presented in the paper apply as well if one takes L and L 2_ to be the full intuitionistic propositional language and its second order extension.

Weak expansion of a formula
The general form of a formula A P L 2 is the following: where @Y i (for 1 ď i ď n`1) denote finite (possibly empty) sequences of quantifiers.
Definition 2.1. Given a formula A as above, the weak expansion of A is the derivation that one obtains by repeatedly applying η-expansions to the derivation consisting only of the assumption of A until the minimal formula of the main branch is atomic, i.e.: indicate (possibly empty) sequences of applications of @E and @I.
We will indicate with E A and I A the two halves of such a derivation consisting of elimination rules and introduction rules respectively, so we will abbreviate the above derivation in the following way: where m " m 1 , . . . , m n in E m A indicates that the conclusion X depends, in addition to the assumption A, on the undischarged assumptions

Sp-X formulas and C-expansion
We recall that Definition 2.2. A formula F P L 2p_q is strictly positive in X (short sp-X) when all free occurrences of the variable X in F are in strictly positive position (i.e. do not appear to the left of any occurrence of Ą).
We will make essential use of the notion of C-expansion of a derivation D defined for sp-X formulas C [see 22, sec. 3.2]. 2 When C is sp-X and D is a derivation of B from assumptions A, ∆ (where A is freely chosen among the undischarged assumptions of D), the C-expansion of a derivation D (relative to X on main assumption A), that we indicate with C D thereby leaving both X and ∆ implicit, is a particular derivation of C B{X from C A{X , ∆. For the exact definition of C-expansion see Appendix C.
With the alternative notation for substitution introduced in [22, sec. 3.2], we write C B{X and C A{X as C B and C A (thus leaving again X implicit), so that: 2 Actually, in [22] we defined the notion of C-expansion for the more general class of formulas, called pn-X formulas, but these will play no role in the present paper.
which we sometimes shorten further to: Remark 2.4. In the present paper, we will only be concerned with the C-expansion of derivations E m A (i.e. the elimination part of the weak expansion of some formula A, see Definition 2.1 above) relative to X on main assumption A.
Observe that, by the definition of C-expansion, the undischarged assumptions of C E m A besides C A are the same as the undischarged assumptions of E m A besides A, namely (see Section 2.1 above)

RP-translation and RP-derivations
The details of the RP-translation p¨q˚are recalled in Appendix D.
For readability, we will abbreviate pA Ą Xq Ą ppB Ą Xq Ą Xq with A B (and thus pA _ Bq˚with @XpA˚ B˚q).
Some results below will hold for a particular class of derivations in the second-order systems NI 2 , NI 2_ , NI 2 at and NI 2_ at (we abbreviate them with NI 2p_q patq ): patqderivation in which the premises of all applications of @E have the form @XpA Bq.
Remark 2.6. If D is an NI-derivation, then its RP-trasnlation D˚is an RP-NI 2 derivation. (Note however that not every RP-NI 2 -derivation is the image of some NI-derivation under the RP-translation).

ε-equations and main previous result
In order to solve the equivalence-preservation problem of the RP-translation, in [22] we introduced an equational theory " ε generated by all instances of the equation ε (see Appendix E). This equation expresses a generalized naturality condition for NI 2 -derivations and the equivalence relation induced by β-, η-, and ε-equations strictly extends the one induced by β-and η-equations only.
The main result of this previous work was that the adoption of " ε offers a solution to the equivalence-preservation problem in the following sense: 3 Two translations of NI into NI 2 at As we recalled in the introduction, Ferreira and Ferreira [4,5,6,8], developed an alternative translation of NI-derivations into NI 2 that we propose to call the FF-translation. The FF-translation agrees with the RP-translation on how to translate formulas, but not on how to translate derivations. In particular, the FF-translation does not use the full power of the @E rule of NI 2 , but rather it maps derivations in NI into derivations in NI 2 at , the fragment of NI 2 obtained by restricting the witnesses of the rule @E to atomic formulas: The FF-translation exploits the property of instantiation overflow : This property is enjoyed by a class of formulas (see [11] for an exact characterization) among which there are all formulas of the form @XA that are the RP-translation of some formula in L.
To better focus on (the internal structure) of derivations rather than on derivability, we slightly reformulate Ferreira and Ferreira's insight, by defining a mapping from NIderivations to NI 2 at -derivations.

Definition 3.2 (@E-atomization, FF-translation).
If D is an RP-NI 2 -derivation, the @Eatomization (or simply atomization) of D, which we indicate as D Ó , is the NI 2 at -derivation defined by induction on D as follows. We only consider the case in which the last rule D is @E since all other rules are translated in a trivial way. In this case observe that D "  Proof. The proposition follows from the fact that for all C P L 2 Remark 3.1. Ferreira and Ferreira present their result in a slightly different way, by using the inductive clauses of Definition 3.2 to give a direct proof of Proposition 3.1, and they refer to what we here called the FF-translation of D as to "the canonical translation of D in F at provided by instatiation overflow" [8]. This minor difference in presentation is however inessential for the results presented here.
As shown by Ferreira and Ferreira, the FF-translation preserves both η-and γequivalence of NI-derivations: Remark 3.2. The analogy between Ferreira and Ferreira's Theorem 3.2 and our Theorem 2.1 may suggest that the FF-translation delivers a solution to the equivalencepreservation problem. This is however not the case, as Ferreira and Ferreira's Theorem 3.2 applies only to disjunction and fails for conjunction, and moreover it cannot be extended to the generalization of γ-conversion needed for interpreting NI as a bicartesian closed category. For more details, see below Sec. 5.
As the next definition shows, using the notion of C-expansion it is possible to define an alternative atomization procedure and thus an alternative translation of NI into NI 2 at in a more compact way: The definition differs from the previous one in the following respect: In case where F is not atomic and Z is the variable in rightmost position in F , using the notation introduced in Section 2.2-2.3 (see in particular Remark 2.4), we define: The relationship between the original and the alternative atomizations (and thus between the original and alternative FF-translations) is very tight: the alternative FF εtranslation is just the derivation that results from Ferriera and Ferreira's original FFtranslation by eliminating some of the β-redexes introduced by their atomization process: Proof. The proof is by induction on D. If D ends with an application of either ĄI, ĄE, or @I, or @E with an atomic witness then it is enough to apply the induction hypothesis to the immediate sub-derivations of D.
If D ends with an application of @E with a non-atomic witness F we reason by induction on F : if F " C Ą D, we assume that Z is the rightmost atomic formula in F . The lengthy computation is postponed to Appendix F; if F " @ZD the case is similar to the previous one.
This proposition together with Ferreira and Ferreira's Theorem 3.2 yields the following corollary: That is, like the FF-translation and unlike the RP-translation, the FF ε -translation preserves the equivalence induced by γ-and η-conversion (but Remark 3.2 applies to the FF ε -translation as well).

The relation between RP-and FF pεq -translations
What is the exact relationship between the original RP-translation on the one hand and the FF-and the FF ε -translation on the other hand?
In this section we give a precise answer to this question by showing that the RPtranslation and the FF ε -translation are equivalent NI 2 -derivations modulo the equivalence " ηε . In particular, we show that the RP-translation of an NI-derivation D can be transformed into the FF ε -translation of D by applying a series of η-expansions and of the conversions arising by orienting the ε-equation from left to right.
Together with Theorem 3.3 of last section, this shows that the RP-translation and the Ferreira and Ferreira's FF-translation are βηε-equivalent derivations in NI 2 . Proof. The proof is by induction on D. If D ends with an application of either ĄI, ĄE, @I, or @E with an atomic withness then it is enough to apply the induction hypothesis to the the immediate sub-derivations of D.
If D ends with an application of @E, then D " Let Z be the atomic formula occurring in rightmost position in F , we have that: The left-to right orientation of the ε-equations can thus be viewed as a sort of permutation that together with η-expansion allows to atomize the application of @E, provided the premise of the rule application is the RP-translation of a propositional formula. Conversely, the FF ε -translation of an NI-derivation D can be viewed as consisting of a (huge) series of η-expansions followed by ε-permutations applied to the RP-translation of D.
As to the relation of the RP-translation and the original FF-translation, by combining Theorem 4.1 and Theorem 3.3 we obtain the following:

RP-translation and " βηǫ vs FF-translation and " βη
Given the results of the previous section, one may be tempted to say there is a trade-off between the solution to the preservation problem we proposed and the work of Ferreira and Ferreira: either one adopts the straightforward RP-translation but one needs a more involved equational theory on NI 2 -derivation; or one adopts the standard βη-equational theory for NI 2 but one needs the more involved FF-translation mapping NI on NI 2 at . Results from further work by the authors seems however to suggest that the adoption of the ε-equation has considerable advantages over the FF-translation. In this section we briefly summarize these results.

FF-translation and generalized permutations
First, and most importantly, although the FF-translation preserves the equivalences induced by η-and γ-conversions, it does not preserves all equivalences one would like to consider on NI 2 -derivations.
As is well known, in order to obtain a perfect match between the syntax of NI and the free bicartesian closed category, it is necessary to consider the following generalized permutative conversions in which every chunk of derivation (and not just those consisting of applications of elimination rules) is permuted-up across an application of disjunction elimination: 3 Consider the instance of this schema in which A, B, C and D are atoms, D (respectively D 1 , D 2 ) consists only of the assumptions of A _ B (resp. C), and D 3 is the derivation C Ą D C ĄE D . As the reader can easily check, the FF-translations of the left and right-hand side of this instance of pγ g q, just like their RP-translations, are not βη-equivalent. On the other hand, they are βηε-equivalent NI 2 at -derivations, (this follows from the fact that Theorem 2.1 keeps on holding if one replaces γ with γ g , see [22], and of Corollary 4.2).
Moreover, as Ferreira and Ferreira observed in [8], Theorem 3.2 fails if NI is extended to include also conjunction. On the other hand, our Theorem 2.1 keeps on holding. This weakness of the FF-translation can be shown to hinge upon a generalization of permutative conversions as well. Once the two Gentzen-Prawitz elimination rules for conjunction are replaced with the elimination rule in general form: A^B rAsrBs C C one can extend Theorem 3.2 to the equivalence relation induced by the β-, η-and γ-conversions of the modified system, but not to the equivalence induced by the γ gconversions for the generalized elimination rule for conjunction (thus showing that the latter is implicit in the η-conversion for the conjunction with the Gentzen-Prawitz rule).
Extending NI 2 and NI 2 at with primitive disjunction Secondly, in the extension of NI 2 with a primitive disjunction connective governed by the disjunction rules of NI (we call this system NI 2_ , see Appedix A), the following holds: Proposition 5.1. For all A P L: A %$ NI 2_ AP roof. By induction on A. The only non trivial case is A " B _ C. In this case we have that: hat is, as soon as one extends NI 2 with a primitive disjunction operator, one can show in the extended system NI 2_ that A _ B and its RP -translation are interderivable. Actually, A and its RP-translation are not just interderivable, but isomorphic modulo " βηγε (see for details [12]).
In contrast to what happens in NI 2_ , a propositional formula A and its RP-translation A˚may fail to be intederivable in the extesion of NI 2 at with a primitive disjunction sign (and thus, a fortiori, they are not isomorphic either). By inspecting one direction of the proof of proposition 5.1 it is clear that A $ NI 2_ at A˚. However, the inspection of the other direction clearly suggests that, at least for some formulas A P L 2_ , in order to establish that A $ NI 2_ at A˚it is essential to apply @E with a non-atomic witness. In particular, at the RP-translation of Y _Z is thus strictly weaker than Y _Z. In the terminology of Prawitz [13, p. 58], it thus follows that pA _ Bq˚weakly defines A _ B in NI 2 at , but it does not strongly define it (and it is plausible to conjecture that no other formula of L 2 does).
Another way of making this clear is by observing that, whereas the disjunction elimination rule warrants that for all A, B, C in L 2_ , A _ B $ NI 2_ at pA Ą Cq Ą pB Ą Cq Ą C, we have that: If there were an NI 2_ at -derivation D of pY Zq Y _ Z{X from @XpY Zq, then one could derive Y _ Z from pY _ Zq˚by using D in place of the application of @E in the first derivation of the proof of proposition 5.1, thereby contradicting Proposition 5.2.
That is, in contrast to what happens in NI 2 at (see Proposition 3.1), the instantiation overflow property fails for @XpA Bq in NI 2_ at .

Concluding remarks
In this paper we have shown how the category-theory-inspired notions introduced in our previous paper can be used to clarify the exact relationship between the alternative translation proposed by Ferreira and Ferreira and the original Russell-Prawitz translation.
In particular, we showed how the notion of C-expansion allows one to define in a straightforward manner an alternative mapping from NI-to NI 2 at -derivations, the FF εtranslation. The FF ε -translation of an NI-derivation D can be seen as the result of applying some steps of β-reduction to the FF-translation of D. On the other hand, it can also be seen as the result of repeteadly applying first several η-expansions and then one application of the ε-conversion to the RP-translation of D.
Finally, we stressed two differences between NI 2 equipped with the equivalence induced by β-, η-and ε-equations on the one hand and NI 2 at equipped with the equivalence induced by β-and η-equations only on the other hand.
First, both the RP-translation and the FF-translation map derivations that are equivalent modulo generalized commutative conversions onto derivations which are not βηequivalent, but only βηε-equivalent. The adoption of the equational theory induced by ε-equation seems thus unavoidable if one wishes to investigate the equational theory of NI arising from its categorical interpretation using second-order propositional logic.
Second, whereas by extending NI 2 with a primitive disjunction operator one can show inside the extended system the interderivability of any formula with its RP-translation (what Prawitz called the strong definability of disjunction in NI 2 ), an analogous result does not hold for NI 2 at . Thus, in a sense, whereas the analysis of propositional connectives in NI 2 delivered by the RP-translation can be "internalized" in the extension of NI 2 with primitive propositional connectives, the analysis in NI 2 at delivered by the F F pεqtranslation remains an analysis "from the outside" (in Prawitz terminology, disjunction is only implicitly definable in NI 2 at ). We conclude with three final remarks: 1. As we stressed in the introduction, the results here presented extend straightforwardly to all other propositional connectives definable in System F (in particular to^, K, J). More precisely, it covers all those connectives whose introductions and elimination rules satisfy the inversion principle first formulated by [15] and refined in the setting of the calculus of higher-level rule by [16] (see [22, sec 4.3]).
The RP-translation of these connectives is given by formulas of the form where all F i are sp-X formulas and we call the formulas belonging to a slight generalization of this class nested sp-X. This suggests to consider another subsystem of System F (called F poly in [12]) in which the rule @E is restricted so that its premise has to be a nested sp-X formula for some variable X. In [12] we show that the atomization procedure introduced in this paper can be generalized to an embedding of F poly into NI 2 at , and that the ε-equations characterize the maximum consistent equational theory of F poly .
2. The tight connection between the ε-equation and the phenomenon of instantiation overflow underlying the present paper seems to be limited to the class of nested sp-X formulas. In [22] the ε-equations was defined for a broader class of formulas, that of nested p-X formulas. Although all these formulas do enjoy the instantiation overflow property as well, it does not seem possible to define a uniform @-atomization procedure in the style of our @-atomization ε for the NI 2 -derivations in which the premises of all applications of @E are nested p-X formulas.
In [2] and [11] it is shown that the instantiation overflow phenomenon is not restricted to nested p-X formulas. In the second paper a class of formulas called generalized Russell-Prawitz formulas (GRP ) is introduced and it is proved that a formula of the form @XA, where A is quantifier-free, enjoys instantiation overflow if and only if it is equivalent, in F at , to a GRP formula. GRP formulas include all nested p-X formula, but the converse is not true. For instance the formula @XppppA Ą B Ą Xq Ą Xq Ą Y q Ą Zq is GRP , hence satisfies instantiation overflow, but is not nested p-X.
3. Finally, we observed that, as we already briefly mentioned, in the extension of System F with primitive propositional connectives, not only every propositional and its Russell-Prawitz translation are interderivable, but they are actually isomorphic (modulo the equivalence relation induced by β-, η-, γ-, and ε-equations). From a categorical perspective, such isomorphisms belong to a more general class of isomorphisms which are induced by a proof-theoretic formulation of the Yoneda lemma. This and further categorical aspects underlying the present work have been spelled out in a fully fledged way in [12].
A The systems NI, NI 2 and NI 2_ The system NI 2 The system NI The system NI 2_ p˚q Proviso: X does not occur free in the undischarged assumptions.

B The standard equivalence on derivations
Remark B.1. As usual we refer to the left-to-right and right-to-left orientations of β-and η-equations as reductions and expansions respectively, and to the left-to-right orientations of γ-equation as permutations. We use conversion to cover any of reduction, expansion, and permutation.

C The notion of C-expansion
Definition C.1 (C-expansion of D relative to X on main assumption A). If C is sp-X and D is a derivation of B from undischarged assumptions A, ∆ (where A is freely chosen among the undischarged assumptions of ∆), we call the C-expansion of D relative to X on main assumption A, notation C D , the derivation of CvB{Xw from CvA{Xw, ∆ defined as follows: A. If X does not occur in C, then C D just consists of the assumption of C.
B. Otherwise C D is defined by induction on C: 1. If C " X then C D " D; 2. If C " @ZF then, as C is sp-X, F is sp-X as well, and we define (where the substitution p@ZF q A{X " @Z 1 pF 1 A{X q might require a renaming of the bound variables of F ).
3. If C " F Ą G then, F does not contain X at all and G is sp-X, so we can define Remark C.1. We observe that the C-expansion (relative to X) of a derivation consisting of the assumption of the variable X is exactly the weak expansion of C.
X˚" X pA Ą Bq˚" A˚Ą B@ XA˘˚" @XAp A _ Bq˚" @XppA˚Ą Xq Ą pB˚Ą Xq Ą Xq Definition D.2 (˚: NI 2_ Þ Ñ NI 2 ). The RP-translation D˚of an NI 2_ -derivation D is by induction on D as follows:´n E The ε-equation Table 1: ε-conversion In [22] we defined the ε-equation for the more general case in which the conclusion of D 1 is a nested p-X formula, where a formulas is nested p-X if it is of the following form: @ Y 1 pF 1 Ą @ Y 2 pF 2 Ą¨¨¨Ą @ Y n pF n Ą @ Y n`1 pGqq . . . qq (the @Y i represent possibly empty lists of quantifiers) and where @Y 1 F 1 , . . . , @Y 1 . . . @Y n F n are formula in which X-occurs only positively.
In the present paper we will only use the restricted form given in Table 1.
G Proof of Proposition 5.2 As usual, we say that an (intuitionistic) frame is a pair F " xW, ďy with ď a partial order on the set (of worlds) W . An (intuitionistic) model is a pair M " xxW, ďy, vy, where xW, ďy is a frame and v : V Þ Ñ PpW q is a function (called valuation) assigning sets of worlds to propositional variables such that if w P vpXq and w ď w 1 then w 1 P vpXq.
As in Tarski's truth definition for a first-order language, we first define the notion of satisfaction of a formula A P L 2_ (at a world w P W in a model M " xxW, ďy, vy) relative to an assignment σ (notation w, σ M A), where an assignment is a function mapping variables on variables. An X-variant of σ is any assignment σ 1 such that for all Y ‰ X, σpY q " σ 1 pY q and we indicate with σrX Þ Ñ Zs the X-variant σ 1 of σ such that σ 1 pXq " Z.
Satisfaction is defined as follows (here and below the indication of the model is omitted if clear from the context; we use w 1 ě w for w ď w 1 ): • w, σ X iff w P vpσpXqq • w, σ A Ą B iff forall w 1 ě w, if w 1 , σ A then w 1 , σ B • w, σ A _ B iff w, σ A or w, σ B • w, σ @XA iff forall w 1 ě w and all atomic formulas Y , w 1 , σrX Þ Ñ Y s A.
When Γ " A 1 , . . . A n we write w, σ Γ for w, σ A 1 , . . . , w, σ A n . We say that Γ A iff for any model M " xxW, ďy, vy, for any assignment σ and any world w P W , If w, σ M Γ then w, σ M A It is easy to see that the rules of NI 2_ at are sound w.r.t. this semantic notion of consequence: Proposition G.1 (Soundness). If Γ $ NI 2_ at A then Γ A. To establish this proposition we need the following lemmata: Lemma G.2. If w, σ B and w ď w 1 then w 1 , σ B. Lemma G.3. If Y R F V pBq and w, σ B then w, σrY Þ Ñ Zs B.
Lemma G.4. If w, σrY Þ Ñ Zs B then w, σ B Z{Y Proof. All three lemmata can be proven by a straightforward induction on B. (The only non trivial cases are those of a formula of the form @XA, which however present no difficulty).
Proof of Proposition G.1. If Γ $ NI 2_ at A then there is an NI 2_ at -derivation D with undischarged assumptions Γ 1 Ď Γ and conclusion A. We reason by induction on D. If D is an assumption or D ends with either ĄI, ĄE, _I, _E the proposition is established in the same way as the soundness of NI w.r.t. its standard Kripke semantics (as σ plays no role).
If D ends with an application of @I (i.e. A " @Y B, and Y does not occur free in Γ 1 ) we have that (for any σ, in all worlds w of all frames, and for all models) that is w, σ M Γ 1 ñ w, σ M @Y B so we can conclude Γ 1 @Y B.
If D ends with an application of @E at then A " B Z{Y (thus @Y B is the premise of the last application of @E in D). We can apply the induction hypothesis to the immediate subderivation of D, from which it follows that (for any σ, in all worlds w of all frames, and for all models) Remark G.1. In [7] Ferreira and Ferreira prove the soundness of NI 2 at with respect to a semantics with a stronger clause for @XA, namely the following: w @XA iff w A B{X for all quantifier-free formulas B P L 2 .
The system NI 2 at is clearly incomplete w.r.t. this semantics as the semantics validates another restriction of the rule @E of NI 2 , namely that obtained by restricting the witnesses to quantifier-free formulas (this fragment of System F , known as the system of predicative polymorphism, see [10], is strictly stronger than F at ).
It is on the other hand plausible to conjecture that NI 2 at is not only sound but also complete w.r.t. the semantics we propose (see also [19] for a more general investigation of Kripke-style semantics of subsystems of NI 2 ).
Let Y ‰ Z. We establish the non derivability of Y _ Z from @XpY Zq by semantic means: Proposition G.5. @XpY Zq NI 2_ at Y _ Z