Core Type Theory

Bulletin of the Section of Logic Volume 52/2 (2023), pp. 145–186 https://doi.org/10.18778/0138-0680.2023.19 Emma van Dijk David Ripley Julian Gutierrez CORE TYPE THEORY Abstract Neil Tennant’s core logic is a type of bilateralist natural deduction system based on proofs and refutations. We present a proof system for propositional core logic, explain its connections to bilateralism, and explore the possibility of using it as a type theory, in the same kind of way intuitionistic logic is often used as a type theory. Our proof system is not Tennant’s own, but it is very closely related. The difference matters for our purposes, and we discuss this. We then turn to the question of strong normalization, showing that although Tennant’s proof system for core logic is not strongly normalizing, our modified system is. Keywords: core logic, type theory, strong normalization. 2020 Mathematical Subject Classification: 03A05, 03B38, 03B47, 03F05. 1. Introduction Neil Tennant’s core logic is a type of bilateralist natural deduction system based on proofs and refutations. We present a proof system for propositional core logic, explain its connections to bilateralism, and explore the possibility of using it as a type theory, in the same kind of way intuitionistic logic is often used as a type theory. Our proof system is not Tennant’s own, but it is very closely related. The difference matters for our purposes, and we discuss this. We then turn to the question of strong normalization, showing that although Tennant’s proof system for core logic is not strongly normalizing, our modified system is. Presented by: Sara Ayhan Received: August 29, 2022 Published online: August 9, 2023 c Copyright by Author(s), L´od´z 2023 c Copyright for this edition by the University of Lodz, L´od´z 2023 146 Emma van Dijk, David Ripley, Julian Gutierrez 2. Core logic We open by presenting a natural deduction system for core logic. This is not Tennant’s own system, although it is closely related. (As the paper progresses, we’ll get more and more perspective on the differences; we discuss them in Sections 2.4,3.5 and 5.1.) The language is an ordinary propositional language with connectives ∧,∨,→,¬of arities 2, 2, 2, 1, respectively. We use p, q, r, . . . for atomic formulas and ϕ, ψ, θ, . . . for arbitrary formulas. We suppress parentheses according to the following conventions: the connectives ∧and ∨bind more tightly than →, and ¬more tightly still; and → associates to the right. Thus ¬p∧q→r∨s→tis ((¬p)∧q)→((r∨s)→t). 2.1. Natural deduction We first present core logic via a natural deduction system, following presentations such as [15,21,22]. This proceeds in the style of [5,12], with an important modification: not every node in a derivation needs to be a formula. There is one additional symbol /that can also occupy nodes in a derivation. It is important to keep in mind, though, that /is not a formula, and does not enter into formula construction. As a result, things like ‘¬/’ and ‘/∧p’ make no sense.1 We will call the things that can stand at nodes of a derivation hats (for reasons that will emerge). That is, a hat is either a formula or else /. Recall that we use ϕ, ψ, θ, . . . for arbitrary formulas; for arbitrary hats, we use C,D. There is an important partial order on hats: C≤Diff either Cis /or C=D. That is, any two distinct formulas are ≤-incomparable, and /is ≤-below all formulas. We will also use the maximum max(C,D) of two hats C,Daccording to this order; note that this is only defined when either C=Dor one of C,Dis /. A sequent, as we use the term, is a set of premise formulas and a conclusion hat; we write ΓCfor the sequent with premises Γ and conclusion C. We draw a distinction between sequents and arguments: an argument is a sequent with a formula as its conclusion. The role of /in these systems is not to carry content, the way a formula might. Rather, when it occurs in a derivation, it should be seen as part of the structure of that derivation, the surrounds that the content-bearing 1Tennant uses the symbol ⊥for this purpose; we use /instead because ⊥is in common use in other work as a formula. To reduce potential confusion, we’ve chosen a symbol that is not usually used as a formula. Core Type Theory 147 formulas fit into. It plays, then, the same kind of role in a derivation as the horizontal bar separating nodes from each other, or the rule labels decorating such bars, or markers of which assumptions are discharged; it indicates (in concert with other such apparatus) relations between the formulas in play. Assumptions work as usual in these natural deduction systems, and in particular only formulas may be assumed. Any derivation, then, has a set Γ of open assumptions, all of which are formulas, and it has a conclusion node, which is a hat C. We refer to Γ Cas the sequent of the derivation, and the derivation as a derivation of its sequent. What we understand a derivation as telling us depends on whether the derivation’s sequent is an argument or not. A derivation with sequent Γ ϕshould be understood as a proof of ϕfrom the assumptions Γ, or, as we will also say, a proof of the argument Γϕ. On the other hand, a derivation with sequent Γ/should be understood as a refutation of the set Γ. It is very much not a proof of /—that wouldn’t make sense, as /does not carry content. We have here two fundamentally different roles for a derivation to play: a proof of an argument, or a refutation of a set of formulas. This is the bilateralism in core logic: a bilateralism of proofs and refutations. In this setting, it would not be right to understand either proofs or refutations as a special kind of the other. The rules of derivation allow us to build proofs and refutations both, from components that themselves may be proofs and refutations both. In this sense, then, core logic derivations are bilateralist: based on two core notions, one positive and one negative, neither of which should be understood as a special case of the other. In this regard, the bilateralism in core logic is like the bilateralisms explored in [1,23,24,25]. Tennant’s discussion of these issues in [19] is useful here. To forestall any misunderstandings, however, we note that core logic is not at all symmetrical in the way that many bilateralist theories are. Proofs and refutations in these systems are not at all each other’s mirror image. Even before we present the rules, we can see this already, as they apply to different things. A proof is a proof of an argument: a pair of a set of premises and a single conclusion; while a refutation is a refutation of just a set of formulas. Both are species of derivation, to be sure, but neither is reducible to the other. 148 Emma van Dijk, David Ripley, Julian Gutierrez 2.2. Rules for core logic With that understood, derivations are otherwise relatively standard. What makes core logic distinctive, other than some care about the difference between formulas and hats, is its use of mostly general eliminations (see for example [17] or [10, Ch. 8]), and a bit of fuss around discharge policies. Derivations begin, as usual, from assumptions. Any formula may be assumed; recall that /, which is not a formula, may not be assumed. An assumption of ϕcounts as a proof of ϕϕ: a proof of ϕfrom the open assumption ϕ. 2.2.1. Conjunction From here, rules proceed connective by connective, with introduction and elimination rules for each connective. Each elimination rule has a major premise, which will be indicated as we proceed. Many of these rules have particular restrictions against certain kinds of vacuous discharge, which we will describe as we go. ϕ ψ ∧Iϕ∧ψ ϕ∧ψ [ϕ, ψ]n . . . C ∧En C Discharged assumptions are marked with [square brackets]; other assumptions, including other occurrences of these discharged formulas, may also occur as assumptions.2We use numeral annotations (here schematized as n) to indicate which rule discharges which discharged assumption: in any derivation, we assume that each occurrence of each discharging rule wears a distinct discharge numeral, and that each discharged assumption wears the numeral corresponding to the rule occurrence that discharged it. Discharge restriction: in ∧E, the discharge [ϕ, ψ] may not be completely vacuous. That is, it must discharge at least one occurence of ϕor at least one occurrence of ψ. The major premise of ∧E is ϕ∧ψ. 2See Section 2.4 for discussion. Core Type Theory 149 2.2.2. Disjunction ϕ ∨Ilϕ∨ψ ψ ∨Irϕ∨ψ ϕ∨ψ [ϕ]n . . . C [ψ]n . . . D ∨En max(C,D) Discharge restriction: in ∨E, neither discharge [ϕ] nor [ψ] may be vacuous. Recall as well that max(C,D) is only defined when either C=Dor at least one of C,Dis /; in other cases the rule ∨E is not applicable. The major premise of ∨E is ϕ∨ψ. 2.2.3. Implication [ϕ]n . . . C →In ϕ→ψ ϕ→ψ ϕ [ψ]n . . . C →En C In the rule →I, we must have C≤ψ. In addition, if Cis /, then the discharge of [ϕ] must not be vacuous. However, in cases where Cis ψitself, the discharge [ϕ] may be vacuous. In →E, the discharge [ψ] may not be vacuous. The major premise of →E is ϕ→ψ. 2.2.4. Negation [ϕ]n . . . / ¬In ¬ϕ ¬ϕ ϕ ¬E/ Discharge restriction: in ¬I, the discharge [ϕ] may not be vacuous. The major premise of ¬E is ¬ϕ. 150 Emma van Dijk, David Ripley, Julian Gutierrez 2.3. Core derivations and core logic What we have in view so far is in fact a proof system for intuitionistic logic, not core logic. That is, an argument Γ ϕis provable in this system iff it is intuitionistically valid, and a set Γ of formulas is refutable in this system iff it is intuitionistically inconsistent.3 To get to core logic, we use the notion of a core derivation, which we now present. A derivation is core iff every major premise of every elimination rule in it is an assumption, and a sequent is core derivable iff it is the sequent of some core derivation. We say that an argument is core provable iff it has a proof that is core, and that a set of formulas is core refutable iff it has a refutation that is core. Not every provable argument is core provable. For example, ¬p, p qis provable as follows: ¬p[p]1 ¬E/ →I1 p→q p [q]2 →E2q This derivation is not core, as the major premise of →E in it is the conclusion of a step of →I rather than an assumption. And indeed there is no core proof of ¬p, pq. To see this, note (by checking the rules) that in a core derivation, every formula that occurs must be a subformula either of some open assumption or of the conclusion. That gives very little room to work with when attempting to prove ¬p, p q, and it’s not hard to see that the task can’t be done. The closest we can get is instead a core refutation of the set {¬p, p}:¬p p ¬E/ Similarly, not every refutable set of formulas is core refutable. For example, the set {¬p, p, q}is refutable as follows: ¬p p q ∧Ip∧q[p]1 ∧E1p ¬E/ 3For discussion of this point, see [13,20]. Core Type Theory 151 However, this set has no core refutation, by similar reasoning to the above. Again, the closest we can get is a core refutation of the distinct set {¬p, p}. One way to see core logic as a consequence relation is this: say that a sequent Γ Cis in core logic iff it is core derivable. As we’ve just seen, then, neither ¬p, p qnor ¬p, p, q /is in core logic, but ¬p, p /is in core logic. In this sense, then, core logic is nonmonotonic on both sides: neither ⊆on the left nor ≤on the right preserves core derivability. Core logic is probably best known for not admitting cut: there are cases where both Γ ϕand ϕ, ∆Care in core logic, but where Γ,∆Cis not. For example, pp∨qand ¬p, p ∨qqare both core derivable, but we’ve just seen that ¬p, p qis not. What holds instead is a property Tennant calls epistemic gain: whenever both Γ ϕand ϕ, ∆Care in core logic, then there is some Σ Din core logic such that Σ ⊆Γ∪∆ and D≤C. Tennant appeals to epistemic gain to defuse criticisms of core logic based on its not admitting cut, and we will depend on epistemic gain in much of our reasoning that follows. It’s not our purpose here, however, to evaluate core logic, so we don’t discuss such defenses further; our purposes just involve noting that this epistemic gain property holds. 2.4. The Prawitz restriction That, then, is the natural deduction system we will work with in what follows. It differs from Tennant’s own systems for core logic and its relatives in one important respect, which is the topic of this subsection and Sections 3.5 and 5.1. Tennant’s systems, as we interpret them, impose a further restriction on discharges, one that we do not impose: that whenever a rule application can discharge an occurrence of an open assumption, it must discharge that occurrence. The first thing to note about this restriction is that it has nothing special to do with core logic. Restrictions like this can be imposed, or not, in ordinary natural deduction systems for logics of all sorts. For example, Gentzen’s original system NJ (in [5]) for intuitionistic logic does not impose any such restriction; but Prawitz’s closely-related system I(in [12]) for intuitionistic logic adds this restriction. Accordingly, we call this restriction ‘the Prawitz restriction’, and call a derivation ‘Prawitz’ when it obeys this restriction.4 4For Tennant’s imposing this restriction, see, e.g., [16, p. 674], [22,§§2.3.2, 4.6]. In some other places, however, Tennant is less explicit. For example, [21, p. 454] imposes the restriction explicitly only for those cases of →I where vacuous discharge 152 Emma van Dijk, David Ripley, Julian Gutierrez 2.4.1. Keeping track of discharge The main reason to impose the Prawitz restriction, as we see it, is that it saves on some bookkeeping. (This is discussed in [12,§I.4].) With the restriction imposed, there is no need to mark separately in a derivation which assumptions are discharged, and no need to mark what rules do the discharging work. In a Prawitz derivation, each assumption is discharged if and only if it can be, and discharged by the earliest rule that could have done the discharging.5 For example, take our above-presented natural deduction system. Now consider this: p p ∧Ip∧p →Ip→p∧p →Ip→p→p∧p If this is to be understood as a Prawitz derivation, both assumptions of pmust in fact be discharged—despite the fact that these occurrences of →I allow for vacuous discharges. This is because the Prawitz restriction requires every rule to discharge every assumption it can. Since these occurrences of →I introduce formulas with antecedent p, they can discharge assumptions of p; and so they must discharge any such assumptions not already discharged. This means, in addition, that both assumptions of p must be discharged by the upper instance of →I. The lower instance, then, does feature vacuous discharge, since by the time it is reached there are no further open assumptions. It is the Prawitz restriction that allows us to conclude all this from the structure above. Without the Prawitz restriction in place, there are would be permissible; and [20] does not state any explicit policy, but on p. 315 includes discussion that seems to require the Prawitz restriction. We (tentatively) think it’s probably best to interpret these sources too as imposing the restriction. 5An anonymous referee suggests that another motivation for the Prawitz restriction might come from searching for derivations of a given sequent, because the restriction ‘allows for faster breakdown in the complexity of sequents for which proofs are being sought’. However, we think that imposing the Prawitz restriction simply cannot be an aid to finding derivations of a given sequent. Any derivation-search strategy that succeeds in finding a Prawitz derivation thereby succeeds in finding a derivation. So any strategy that works in the presence of the Prawitz restriction will work exactly as well in its absence. Core Type Theory 153 options. Since these uses of →I both allow vacuous discharge, each assumption of pmight be discharged by the upper →I, by the lower →I, or not at all; and these choices can be made independently. This means that the above display, read as containing no information about discharges, corresponds to nine distinct derivations.6 Working in systems without the Prawitz restriction, then, more bookkeeping is needed to indicate which assumptions are discharged and which are not, and to indicate which rules do the discharging. Our convention is a usual one: every occurrence of a discharging rule in a derivation must be annotated with a distinct numeral, and every discharged assumption in a derivation must appear surrounded by [square brackets] and annotated with the numeral of the rule that discharged it. Using this convention, we could indicate the Prawitz derivation described above like so: [p]1[p]1 ∧Ip∧p →I1 p→(p∧p) →I2p→p→(p∧p) However, we can also use this convention to indicate non-Prawitz derivations, for example this one: [p]2[p]1 ∧Ip∧p →I1 p→p∧p →I2 p→p→p∧p Indeed, one of the key reasons we do not impose the Prawitz restriction is because we want to study derivations like this latter example. Already, though, we can see one important effect of the restriction on Tennant’s own natural deduction systems: the property of being a Prawitz derivation is not closed under substitution of arbitrary formulas for atomic formulas. To see this, return to the most recent displayed derivation, the non-Prawitz 6According to some conventions, this display would be read as containing the information that no discharges have occurred, thus picking out a particular one of these nine. 160 Emma van Dijk, David Ripley, Julian Gutierrez 3.4. Substitution Capture-avoiding substitution of terms for variables in this calculus works as it does in similar calculi; there’s nothing particularly remarkable about it. We pause to go through the details nonetheless; many aspects of core type theory do not work as usual, so it’s worth checking the details even of those aspects that do. Where xϕ1 1, . . . , xϕn nare distinct variables and Nϕ1 1, . . . , Nϕn nterms of corresponding types, then [x17→ N1, . . . , xn7→ Nn] is a substitution. (Note that all substitutions are finite.) Given a substitution σ, the substitution σ↓yis just like σexcept that it does not substitute anything for the variable y. That is, [x17→ N1, . . . , xn7→ Nn]↓xiis [x17→ N1, . . . , xi−17→ Ni−1, xi+1 7→ Ni+1, . . . , xn7→ Nn]; and [x17→ N1, . . . , xn7→ Nn]↓yis just [x17→ N1, . . . , xn7→ Nn] if yis not one of the xis. Say that a variable yis free in [x17→ N1, . . . , xn7→ Nn] iff it is free in some Ni; and say that y is acted on by [x17→ N1, . . . , xn7→ Nn] iff it is one of the xi. Given a term or eliminator, capture-avoiding substitution works as usual: •xi[x17→ N1, . . . , xn7→ Nn] = Ni; •y[x17→ N1, . . . , xn7→ Nn] = y, where yis not one of the xis; • hM, Niσ=hMσ, Nσi; •inl(M)σ=inl(Mσ); inr(M)σ=inr(Mσ); •(λ→y.M)σ=λ→y.(Mσ↓y), assuming yis not free in σ;10 •(λ¬y.M)σ=λ¬y.(Mσ↓y), assuming yis not free in σ; •(ME)σ= (Mσ)(Eσ); •¬ϕLMMσ=¬ϕLMσM; •ϕ∧ψLhx, yi.MMσ=ϕ∧ψLhx, yi.Mσ↓x↓yM, assuming neither xnor yis free in σ; 10Recall that we identify terms up to change of bound variable. So if yis free in σ, we first change the bound variable yin λ→y.M to some variable that is not free in σ. (Since all substitutions are finite, there is always some such.) All similar assumptions in this definition should be read the same way. Core Type Theory 161 •ϕ∨ψLx.M, y.NMσ=ϕ∨ψLx.Nσ↓x, y.Oσ↓yM, assuming neither xnor y is free in σ; and •ϕ→ψLM, x.NMσ=ϕ→ψLMσ, x.Nσ↓xM, assuming xis not free in σ. Note two things: first that, since there are no variables with hat /, that M[x7→ N/] is never defined; and second that substitution never affects hats: that is, the hat on MC[x7→ N] is always exactly C. Substitution interacts pleasantly with composition of eliminators: Lemma 3.2.Given eliminators Eand Fsuch that LEFMis defined, and a substitution σ, the eliminator L(Eσ)(Fσ)Mis LEFMσ. Proof: Unpacking definitions. 3.5. The Prawitz restriction on terms Recall that the Prawitz restriction on derivations requires that when any rule application in a derivation can discharge any open assumption, it must discharge that open assumption. The corresponding restriction on terms is this: that whenever a component of a term binds a variable of type ϕ, it binds all free variables of type ϕin its scope. Equivalently, the Prawitz restriction corresponds to a term system with a single variable of each type, rather than the denumerably many variables of each type that we have assumed.11 We noted in Section 2.4 that there are many derivations in our system that do not obey the Prawitz restriction, such as the derivation repeated here: [p]2[p]1 ∧Ip∧p →I1 p→p∧p →I2 p→p→p∧p This derivation corresponds to the term (λ→xp.λ→yp.(hx, yi)p∧p)p→p→p∧p. This term requires two distinct variables of type p. This is because λ→y 11Term systems like this are not often explored, because they do not allow for a definition of capture-avoiding substitution; our definition in Section 3.4, like other definitions, relies crucially on being able to draw on fresh variables of a given type to avoid clashes between free and bound variables. (As we will see in Section 5.1, this interference with substitution also blocks strong normalization.) 162 Emma van Dijk, David Ripley, Julian Gutierrez must bind the yin hxp, ypiwithout binding the x, so that the outer λ→x can bind the xinstead. This brings us to the main reason we’ve chosen to go without the Prawitz restriction: the terms it excludes include terms with natural and important computational behaviour. The term λ→x.λ→y.hx, yiis a very simple pairing function, a function that takes inputs xand yand returns their ordered pair.12 Imposing the Prawitz restriction would allow us to define this function only in the case where the two inputs have distinct types, but it is also perfectly natural to want to pair up two pieces of data that have the same type. Indeed, the Prawitz restriction prevents us from defining any functions that take multiple inputs of the same type: the binding required for the final input is required by the Prawitz restriction to bind all free variables of that type; any outer bindings of that same type turn out vacuous. It would be impossible, for example, to build basic arithmetic on the Church numerals (see [7, Ch. 4]) in a system obeying the Prawitz restriction, since this requires defining addition and multiplication functions, each of which takes two inputs of the same (numeric) type. We take it, then, that most standard term systems work without the Prawitz restriction for good reason, and so we develop core type theory without any such restriction. 4. Reduction In this section, we define two relations of reduction on terms of our calculus: what we call principal reduction and full reduction. The difference is that full reduction includes commuting conversions; principal reduction does not. We then prove a number of lemmas about these reduction relations, in the leadup to Section 5, where we prove that principal reduction is strongly normalizing. We conjecture that full reduction is also strongly normalizing, but leave that question for future work. 4.1. Redexes and reducts Both reduction relations are defined by identifying a class of special terms called redexes, and assigning to each redex a term called its reduct. The 12This is the function written (,) in Haskell, for example. Core Type Theory 163 difference between principal reduction and full reduction is entirely in which terms are redexes. Then, given a chosen notion of redex, for any term M that contains a redex Ras a subterm, we define a specific term as the onestep reduction of Mat R. The move from redexes to one-step reduction is very much not as usual; this is one of the more distinctive features of core type theory, and it is a key motivation of this work to explore this nonstandard notion. Let’s dive in. 4.1.1. Principal redexes The following table displays the forms of all principal redexes and their corresponding reducts. Redex Reduct hM, NiLhx, yi.OMO[x7→ M, y 7→ N] inl(M)Lx.N, y.OMN[x7→ M] inr(M)Lx.N, y.OMO[y7→ M] (λ→x.(Mψ))LN, y.OMO[y7→ M[x7→ N]] (λ→x.(M/))LN, y.OMM[x7→ N] (λ¬x.M)LNMM[x7→ N] In defining principal reduction, all and only the principal redexes count as redexes. 4.1.2. Commuting redexes Any term of the form (ME)Fis a commuting redex; its reduct is MLEFM. Note that LEFMis defined, and MLEFMwell-formed, whenever (ME)Fis well-formed. Note as well that no commuting redex is a principal redex, so given a redex (of either kind), the reduct of that redex is unambiguously determined. In defining full reduction, both principal redexes and commuting redexes count as redexes. Since we focus on principal reduction rather than full reduction in Section 5, we don’t linger specifically on commuting redexes. However, the 164 Emma van Dijk, David Ripley, Julian Gutierrez definitions and lemmas in this section don’t care about the difference; when we speak of ‘reduction’ unqualified, we are making a definition or claim that applies to both principal and full reduction.13 4.2. One-step reduction Using these redexes and their reducts, we define a relation of one-step reduction between terms. (Since we have two different choices for what counts as a redex—principal only or principal plus commuting—we end up with two different choices for a one-step reduction relation: principal or full.) Given any term that contains an occurrence of a redex at a subterm, we define the unique result of reducing that term at that redex occurrence. That much is as usual for term systems like this. However—and this is not usual—reduction in this system is not a compatible relation. That is, we do not always simply replace a redex with its reduct in place, leaving its context alone. Such a procedure could not work in core type theory. The reason is that the result of such a procedure is not always well-formed in this system. For example, consider the redex ((λ→yϕ.xψ)wϕ)ψwith reduct xψas it occurs in the term (λ→w.(z¬ψL(λ→y.x)wM)/)ϕ→θ. Replacing this redex with its reduct would yield (λ→w.(z¬ψLxψM)/)ϕ→θ. This latter, however, is not a term, as it violates a restriction on λ→, which may not bind w vacuously in this situation. (This restriction corresponds to the restrictions against certain cases of vacuous discharge in the rule →I.) This is an example of the following. Many of our formation rules (in the above example, using λ→to bind into an exceptional term) require certain variables to appear free; but some redexes, because they themselves involve vacuous binding, contain free variables that are not contained in their reducts. That is, core type theory allows vacuous binding in some 13There are two more potential sources of redexes that might come to mind, although we use neither in this paper. First, uses of an explosion rule like typical ⊥E in natural deduction systems create possible violations of the subformula property, and so reduction steps are sometimes introduced to prevent these violations, as in [12, p. 40]. However, core logic contains no such explosion rules, so no such reduction steps are needed or even possible. Second, [18] considers a type of reduction there called ‘shrinking’, which in effect allows a one-step reduction directly from MCto NCwhenever Nis a subterm of M. This makes havoc for computational interpretations of the term language, for reasons discussed in [11]; we leave it aside here. Core Type Theory 165 circumstances but not all, and it is the interaction between these circumstances that creates the phenomenon of interest.14 For a different kind of example, consider the redex ((λ→yϕ.(z¬ϕy)/)ϕ→ψLxϕ, wϕ.wM)ψ with redex (zx)/as it occurs in the term (h(λ→y.zy)Lx, w.wM, vθi)ψ∧θ. Replacing this redex with its reduct would yield h(zx)/, wi. This latter, however, is not a term, as the constructor h,irequires two typed subterms, and (zx)/is exceptional. This corresponds to the rule ∧I’s requiring formulas as premises. This is an example of a different kind of phenomenon. Many of our formation rules for terms (in the above example, using h,i) require terms to be typed; but some redexes are typed and yet have exceptional reducts. Reducing such a redex in place, then, yields a nonsensical result. The troubles with reducing in place, then, are twofold: moving from a redex to its reduct can drop free variables, and it can move from a typed term to an exceptional one. But these reductions can happen in places where free variables or types are required. Leaving everything else in place, then, won’t do in general. In what follows, we show how to handle these problems. We start by noting two important facts about redexes and their reducts: for any redex RCwith reduct R0D, we always have FV(R0)⊆FV(R) and D≤C. That is, free variables and hats do not always remain constant between a redex and its reduct, but they cannot change freely; when there is a change, it is always in the same direction. We repeatedly use this constraint—which is the term-level reflection of epistemic gain—in what follows. Basically, our strategy works like this: where we can get away with reducing in place, leaving the immediate context alone, that’s what we do. Where the result would not be well-formed, we simply drop the immediate context altogether. That’s the intuition, anyhow; here’s the precise definition of one-step reduction. 14Contrast a usual simply-typed lambda calculus, where vacuous binding is always allowed; but also contrast the lambda calculus of [3], standardly now called the λI calculus, where vacuous binding is never allowed; also see [2, Ch. 9]. In this calculus, redexes and their corresponding reducts always have exactly the same free variables (see [2, Lemma 9.1.2]), so any nonvacuous binding into a redex remains nonvacuous into its reduct. 166 Emma van Dijk, David Ripley, Julian Gutierrez Definition 4.1 (One-step reduction).First, if Ris a redex and Sits reduct, then Rreduces to Sin one step; as we write, R 1S. The rest of the definition contains a number of conditions. These are expressed in the form: X 1Y Z 1W Here is how such a condition should be read. We only apply it if X,Y,Z are each well-formed, without any assumption that Wis well-formed. Under these conditions, if X 1Yand Wis well-formed, then Z 1W; on the other hand, if X 1Yand Wis not well-formed, then Z 1Yinstead. This fallback condition—that when Wis not well-formed we have Z 1 Y—is what gives one-step core reduction its distinctive flavour. Note that there is no indeterminism or choice introduced here: if Wis well-formed we do not have Z 1Yfrom such a condition. Only in the case that Wis not well-formed do we fall back to Z 1Y. Here, then, are the conditions: M 1M0 ME 1M0E E 1E0 ME 1ME0 E 1N ME 1N M 1M0 hM, Ni 1hM0, Ni N 1N0 hM, Ni 1hM, N0i M 1M0 inl(M) 1inl(M0) M 1M0 inr(M) 1inr(M0) M 1M0 λ→x.M 1λ→x.M0 M 1M0 λ¬x.M 1λ¬x.M0 M 1M0 LMM 1LM0M M 1M0 Lhx, yi.MM 1Lhx, yi.M0M Core Type Theory 167 M 1M0 LM, x.NM 1LM0, x.NM N 1N0 LM, x.NM 1LM, x.N0M M 1M0 Lx.M, y.NM 1Lx.M0, y.NM N 1N0 Lx.M, y.NM 1Lx.M, y.N0M Expressed in this way, these conditions might look like usual reduce-inplace conditions. But recall our distinctive way of reading these, involving fallback in case the lower-right component is not well-formed; this is the key to the definition. Since this is an unusual way to handle one-step reduction, let’s look at an example. Consider the condition for inl(), reproduced here: M 1M0 inl(M) 1inl(M0) Suppose first that Mψis (λ→xϕ.yψ)Lz, v.vM. Then Mis a redex, with reduct y. So, according to the condition for inl(), we can conclude that inl(M)ψ∨θcan be reduced in one step to inl(y). So far, so normal. Suppose instead, though, that Mψis (λ→xϕ.y¬ϕLxM)Lz, v.vM. Then M is again a redex, now with reduct (yLzM)/. By the same condition, then, inl(M)ψ∨θcan be reduced. However, note that inl(yLzM) is not well-formed; inl() can only be applied to typed terms, and yLzMis exceptional. Thus, inl(M) cannot reduce to inl(yLzM), since the latter isn’t a term at all. So, according to the condition for inl(), we conclude that inl(M) reduces in one step directly to yLzM. Three important facts about one-step reduction. First, terms always reduce to terms, while eliminators sometimes reduce to eliminators and sometimes to terms. Second, if MC 1ND, then D≤C. Finally, if M 1N, then FV(N)⊆FV(M). (All these can be shown by induction on the above definition.) Let’s look at an example that demonstrates some of these complexities. Consider the term M¬(ϕ∧ψ)= (λ¬xϕ∧ψ.(w¬θLxLhyϕ, zψi.(λ→vϕ.uθ)yϕMM)/). The free variables of this term are w¬θand uθ, and so this term corresponds to a derivation of the sequent ¬θ, θ¬(ϕ∧ψ). It contains a redex (λ→v.u)y with reduct u, inside the eliminator Lhy, zi.(λ→v.u)yM. Let’s go through the one-step reduction of Mat this redex. 168 Emma van Dijk, David Ripley, Julian Gutierrez First, we note that Lhy, zi.uMis not well-formed, since a conjunction eliminator cannot bind fully vacuously; so we reduce Lhy, zi.(λ→v.u)yMdirectly to uitself. Having done this, we note that xϕ∧ψuθis also not wellformed; no rule allows us to juxtapose two terms at all. So we reduce xLhy, zi.(λ→v.u)yMalso directly to u. The next two layers do work in place, so we reduce wLxLhy, zi.(λ→v.u)yMM to wLuM. The final layer, however, runs into trouble again; as xis not free in wLuM, the binder λ¬xmay not bind into wLuM. So Mitself reduces to (wLuM)/. Although we have here worked through this reduction layer by layer, we emphasize that this is one-step reduction; this is the result of reducing a single term at a single redex. 4.3. Reduction concepts Definition 4.2 (Reduction paths).Given a relation 1of one-step reduction, a reduction path from Xis a sequence (finite or infinite) X0,...,Xn, . . . such that X0=X, and for each n,Xn 1Xn+1. For a finite reduction path X0,...,Xn, we say it is a reduction path from X0to Xn, and its length is the number nof reduction steps in it. Definition 4.3 (Normal, strongly normalizing).A term or eliminator is normal iff all reduction paths from it have length 0. A term or eliminator is strongly normalizing iff all reduction paths from it are finite. If a term Mis strongly normalizing, then |M|is the length of its longest reduction path. (If Mis not strongly normalizing, |M|is not defined.) We also define |E| for eliminators E, but slightly differently: |E| is the total of all |N|for E’s immediate subterms N, and is undefined if any such |N|is undefined. Definition 4.4 (Multistep reductions).We say Xreduces to Y, written X Y, iff there is a (necessarily finite) reduction path from Xto Y. We say Xproperly reduces to Y, written X +Y, iff there is a reduction path from Xto Ywith length at least 1. Note, now by induction on reduction paths, that if MC ND(and so also if M +N), then D≤Cand FV(N)⊆FV(M). Since we have two different notions of reduction in view (principal and full), we also have two different notions of normal form, strongly normalizing, etc. It’s worth pausing here to think a bit about relations between these. Since full reduction is defined in terms of all the principal redexes Core Type Theory 169 (and then some), we have that any principal reduction path is also a full reduction path. This gives us that any term in full normal form is also in principal normal form, and that any term that is fully strongly normalizing is also principally strongly normalizing.15 We also note that the full normal forms are exactly the core terms. Corresponding to our definition of core derivations, we say that a term is core iff in all its subterms of the form ME, the term Mis a variable. This is also what it takes to be a full normal form: Mis an introduction iff ME is a principal redex, and Mis an elimination iff MEis a commuting redex. 4.4. Reduction lemmas Here we prove a number of facts about reduction, and about interactions between reduction and substitution, that will be used in Section 5. These facts hold for both principal and full reduction. Lemma 4.5.All the clauses of Definition 4.1 hold as well for . That is, where X 1Y Z(X) 1Z(Y) is a condition appearing in Definition 4.1, for any terms or eliminators X,Y,Z(X)such that X Y: if Z(Y)is well-formed we have Z(X) Z(Y), and if Z(Y)is not well-formed we have Z(X) Y.16 Proof: Induction on the reduction path from Xto Y. At each step, we need to know that if Z(Y) is well-formed and W 1Y, then Z(W) is also well-formed—this way, if Z(Y) is well-formed, we can ensure that all the needed intermediate links from Z(X) to Z(Y) are also well-formed. This holds, though, because of what we know about how reduction affects hats and free variables. 15We do not consider in this paper, outside this footnote, the notion of weak normalization, where a term Mcounts as weakly normalizing iff there is some normal form Nwith M N. In general, when we have two notions of reduction a⊆ b, like our principal and full reductions, nothing useful follows about a relationship between weak normalization for aand b. In this regard, weak normalization is unlike both strong normalization and normal forms. 16Here, Z(X) should be understood as a term or eliminator with Xas an immediate constituent, and similarly for Z(Y). 176 Emma van Dijk, David Ripley, Julian Gutierrez works because the inductive structures of terms and of types do not align, so we can play them off against each other. Lemma 5.2 (Variables).For any type ϕ, every variable of type ϕis SC. Proof: All variables xϕdo not contain any redexes as subterms, thus do not have any one-step reductions, and hence all reduction paths from xϕ are of length 0, so finite. When ϕis complex, the additional conditions following “whenever it reduces” are vacuously fulfilled, as variables never reduce to such forms. So all variables are SC. Lemma 5.3 (Closure by reduction).If Mis SC and M N, then Nis SC.18 Proof: Note first that if Mis strongly normalizing and M N, then Ntoo must be strongly normalizing; any infinite reduction path starting from Nwould give rise to an infinite reduction path starting from M. Since Mis SC, it must be strongly normalizing, so Ntoo must be strongly normalizing. It remains only to check the additional requirements for Nto be SC, according to N’s hat. Recall that if Nis Nϕ, then Mmust be Mϕ. •If Nis N/, then there are no additional requirements, and we’re done. •If Nis Npfor an atomic type p, then there are no additional requirements, and we’re done. •If Mϕ∧ψ Nϕ∧ψ, then if Nϕ∧ψreduces to hO, P iso does M. Since Mis SC, in this case Oand Pmust be SC, so the additional requirement on Nis met. •If Mϕ∨ψ Nϕ∨ψ, then if Nϕ∨ψreduces to inl(O) or inr(O) so does M. Since Mis SC, in these cases Omust be SC, so the additional requirement on Nis met. •If Mϕ→ψ Nϕ→ψ, then if Nreduces to λ→x.O so does M. Since Mis SC, in these cases it must be that for all SC terms Pϕ, the term O[x7→ P] is SC. So the additional requirement on Nis met. 18Note that Mand Nneedn’t have the same hat, so this claim precisely as stated in [4] would be false. Core Type Theory 177 •If M¬ϕ N¬ϕ, then if Nreduces to λ¬x.O so does M. Since M is SC, in these cases it must be that for all SC terms Pϕ, the term O[x7→ P] is SC. So the additional requirement on Nis met. Lemma 5.4 (Girard’s lemma).Let Mbe a term that is not an introduction, such that for all Nwith M 1N,Nis SC. Then Mis SC. Proof: If there does not exist such an Nthen Mis SC because Mdoes not have any one-step reductions, hence all reduction paths from Mare of finite 0 length and additional requirements depending on hat do not apply. Since Nis SC, every reduction path is finite from N, hence Mis strongly normalizing because Mreduces finitely in one step to N. •If all Nhave hat /, then Mis SC because Mis SN and additional requirements depending on hat don’t apply because Mdoes not reduce to any introductions. •If there exists Nwith an atomic hat, then Mhas an atomic hat and is SC because Mis SN. Since Mis not an introduction, it is not, in reduction to itself, required to satisfy the additional conditions for Mto be SC for the following hats: •If there exists Nwith a hat of the form ϕ∧ψ, then Mhas hat ϕ∧ψ. If M 1N hO, P i,Oand Pare SC because Nis SC. Since Mis strongly normalizing and whenever Mreduces to a term hO, P i,O and Pare SC, Mis SC. •If there exists Nwith a hat of the form ϕ∨ψ, then Mhas hat ϕ∨ψ. If M 1N inl(O) or M 1N inr(O), Ois SC because Nis strongly normalizing. Since Mis SN and whenever Mreduces to a term inl(O) or inr(O), Ois SC, Mis SC. •If there exists Nwith hat ϕ→ψ, then Mhas hat ϕ→ψ. If M 1N λ→x.O, for all SC terms Pϕ, the term O[x7→ P] is SC. Since Mis strongly normalizing and whenever Mreduces to a term λ→x.O, for all SC terms Pϕ, the term O[x7→ P] is SC, Mis SC. •If there exists Nwith hat ¬ϕ, then Mhas hat ¬ϕ. If M 1N λ¬x.O, for all SC terms Pϕ, the term O[x7→ P] is SC. Since Mis 178 Emma van Dijk, David Ripley, Julian Gutierrez strongly normalizing and whenever Mreduces to a term λ¬x.O, for all SC terms Pϕ, the term O[x7→ P] is SC, Mis SC. Lemma 5.5 (Adequacy of λ(I)).If for all SC Mϕwe have Nψ[x7→ M]is SC, then (λ→x.N)ϕ→ψis SC. Proof: By Lemma 5.2 , all variables are SC. Let M:= x,N[x7→ x] = Nis SC and hence Nis strongly normalizing. Thus, λ→x.N is strongly normalizing because the only possible reductions involve reducing Nwithin the term or reduction to an exceptional term. Thus, the reduction paths of Nbind the reduction paths of λ→x.N. If λ→x.N λ→x.N0, then N N0by the reduction rules. By Lemma 4.12,N[x7→ M] N0[x7→ M] and N0[x7→ M] is SC by Lemma 5.3. Thus, λ→x.N is SC because it is strongly normalizing and whenever it reduces to λ→x.N0, for any SC Mϕ,N0[x7→ M] is SC. Lemma 5.6 (Adequacy of λ(II)).If for all SC Mϕwe have N/[x7→ M] is SC (and so long as x∈FV(N)), then (λ→x.N)ϕ→ψand (λ¬x.N)¬ϕare both SC. Proof: By Lemma 5.2 , all variables are SC. Let M:= x,N[x7→ x] = Nis SC and hence Nis strongly normalizing. Thus, both λ→x.N and λ¬x.N are strongly normalizing because the only possible reductions involve reducing Nwithin the term or reduction to an exceptional term. Thus, the reduction paths of Nbind the reduction paths of λ→x.N and λ¬x.N. If λ→x.N λ→x.N0or λ¬x.N λ¬x.N0, then N N0by the reduction rules. By Lemma 4.12,N[x7→ M] N0[x7→ M] and N0[x7→ M] is SC by Lemma 5.3. Thus, λ→x.N and λ¬x.N are SC because they are strongly normalizing and whenever they respectively reduce to λ→x.N0and λ¬x.N0, for any SC Mϕ,N0[x7→ M] is SC. Lemma 5.7 (Adequacy of h,i).If Mϕand Nψare both SC, then hM, Niϕ∧ψ is SC. Proof: hM, Niis strongly normalizing because the only possible reductions involve reducing Mand Nwithin the term or reduction to an exceptional term. Thus, since Mand Nare strongly normalizing, their reduction paths bind the reduction paths of hM, Ni. Core Type Theory 179 By Lemma 5.3, if M M0and N N0then M0and N0are SC. Whenever hM, Nireduces to an introduction hM0, N0i,M0and N0are SC, thus, since hM, Niis also strongly normalizing, by Definition 5.1 it is SC. Lemma 5.8 (Adequacy of inl,inr).If Mϕis SC, then inl(M)and inr(M) are both SC. Proof: Wlog, we consider just inl(M). inl(M) is strongly normalizing because the only possible reductions involve reducing Mwithin the term or reduction to an exceptional term. Thus, since Mis strongly normalizing, reduction paths from inl(M) are bound by reduction paths of M. By Lemma 5.3 if M M0, then M0is SC. Whenever inl(M) reduces to an introduction inl(M0), M0is SC, thus, since inl(M) is also strongly normalizing, by Definition 5.1 it is SC. Lemma 5.9 (Adequacy of application (I)).If Mϕ→ψis SC, Nϕis SC, and for all SC Qψ,O[x7→ Q]is SC, then MLN, x.OMis SC. Proof: Let Q=xwhere xis SC by Lemma 5.2, thus O[x7→ x] = Ois SC. Since M,Nand Oare SC, they are strongly normalising and hence |M|,|N|and |O|are defined. We proceed by induction on |M|+|N|+|O|. By Lemma 5.4, to prove that MLN, x.OMis SC, we need to prove that all one-step reducts are SC. Given M 1M0or N 1N0or O 1O0where M0,N0, and O0are SC by Lemma 5.3: •If MLN, x.OM 1M0LN, x.OMor MLN, x.OM 1MLN0, x.OM or MLN, x.OM 1MLN, x.O0M, then we apply the induction hypothesis and Lemma 4.9 to obtain |M|+|N|+|O|>|M0|+|N|+|O|, |M|+|N|+|O|>|M|+|N0|+|O|or |M|+|N|+|O|>|M0|+|N|+|O0|. •If MLN, x.OM 1M0/or MLN, x.OM 1N0/or MLN, x.OM 1O0/, then we already have M0,N0, or O0SC. •If MLN, x.OMis a principal redex, then Mis of the form λ→y.P D. If D=/, then MLN, x.OM 1P[y7→ N] which is SC by Definition 5.1. Otherwise MLN, x.OM 1O[x7→ P[y7→ N]] which is SC by the lemma statement. 180 Emma van Dijk, David Ripley, Julian Gutierrez Lemma 5.10 (Adequacy of application (II)).If M¬ϕis SC and Nϕis SC, then MLNMis SC. Proof: Since Mand Nare SC, they are strongly normalising and hence |M|and |N|are defined. We proceed by induction on |M|+|N|. By Lemma 5.4, to prove that MLNMis SC, we need to prove that all one-step reducts are SC. Given M 1M0or N 1N0where M0and N0are SC by Lemma 5.3: •If MLNM 1M0LNMor MLNM 1MLN0Mthen we apply the induction hypothesis and Lemma 4.9 to obtain |M|+|N|>|M0|+|N|or |M|+|N|>|M|+|N0|. •If MLNM 1M0/or MLNM 1N0/, then we already have M0or N0 SC. •If MLNMis a principal redex, then Mis of the form λ¬x.O, and MLNM 1O[x7→ N] which is SC by Definition 5.1. Lemma 5.11 (Adequacy of Conjunction elimination).If Mϕ∧ψis SC, and for all SC Pϕ,Qψthe term N[x7→ P, y 7→ Q]is SC, then MLhx, yi.NMis SC (if well-formed). Proof: Let P=xand Q=ywhere xand yare SC by Lemma 5.2, thus N[x7→ x, y 7→ y] = Nis SC. We proceed by induction on |M|+|N|. By Lemma 5.4, to prove that MLhx, yi.NMis SC, we need to prove that all one-step reducts are SC. Given M 1M0and N 1N0where M0and N0 are SC by Lemma 5.3: •If MLhx, yi.NM 1M0Lhx, yi.NMor MLhx, yi.NM 1MLhx, yi.N0M then we apply the induction hypothesis and Lemma 4.9 to obtain |M|+|N|>|M0|+|N|or |M|+|N|>|M|+|N0|. •If MLhx, yi.NM 1M0/or MLhx, yi.NM 1N0/, then we already have M0and N0SC. •If MLhx, yi.NMis a principal redex, then Mis of the form hR, Si and MLhx, yi.NM 1N[x7→ R, y 7→ S] which is SC by the lemma statement and Definition 5.1. Core Type Theory 181 Lemma 5.12 (Adequacy of Disjunction elimination).If Mϕ∨ψis SC, and for all SC Pϕthe term N[x7→ P]is SC, and for all SC Qψthe term O[y7→ Q]is SC, then MLx.N, y.OMis SC (if well-formed). Proof: Let P=xand Q=ywhere xand yare SC by Lemma 5.2, thus N[x7→ x] = Nand O[y7→ y] = Oare SC. Since M,Nand Oare SC, they are strongly normalising and hence |M|,|N|and |O|are defined. We proceed by induction on |M|+|N|+|O|. By Lemma 5.4, to prove that MLx.N, y.OMis SC, we need to prove that all one-step reducts are SC. Given M 1M0or N 1N0or O 1O0where M0,N0, and O0are SC by Lemma 5.3: •If MLx.N, y.OM 1M0Lx.N, y.OMor MLx.N, y.OM 1MLx.N0, y.OM or MLx.N, y.OM 1MLx.N, y.O0M, then we apply the induction hypothesis and Lemma 4.9 to obtain |M|+|N|+|O|>|M0|+|N|+|O|, |M|+|N|+|O|>|M|+|N0|+|O|or |M|+|N|+|O|>|M0|+|N|+|O0|. •If MLx.N, y.OM 1M0or MLx.N, y.OM 1N0or MLx.N, y.OM 1 O0, then we already have M0,N0, or O0SC. •If MLx.N, y.OMis a principal redex, then Mis of the form inl(R) or inr(R) and MLx.N, y.OM 1N[x7→ R] or MLx.N, y.OM 1O[y7→ R] which are both SC by the lemma statement and Definition 5.1. Definition 5.13.A substitution [x17→ P1, . . . , xn7→ Pn] is SC iff P1, . . . , Pn are all SC. A term Mis SC under substitution iff for all SC substitutions σ, the term Mσ is SC. Theorem 5.14.All terms are SC under substitution. Proof: Take any term M. To see that Mis SC under substitution, proceed by induction on M’s formation. •If Mis xϕthen any substitution for xwill be a variable and Lemma 5.2 applies. •If Mis hN, Oi: take any SC substitution σ. By the induction hypothesis, Nand Oare SC under substitution, so Nσ and Oσ are SC. Thus, by Lemma 5.7,hNσ, Oσiis SC; but this is just Mσ. •If Mis inl(N) or inr(N), the reasoning is similar to the h,icase. 182 Emma van Dijk, David Ripley, Julian Gutierrez •If Mis λ→xϕ.N: take any SC substitution σ, and change M’s bound variables so that xis neither acted on by σnor free in σ. By the induction hypothesis, Nis SC under substitution, so for any SC term Pϕ, we have that Nσ[x7→ P] is SC. Thus, by Lemma 5.5 and Lemma 5.6, λ→x.(Nσ) is SC; but this is just Mσ. •If Mis λ¬x.M, the reasoning is similar to the λ→case. •If Mis NLO, x.P M: take any SC substitution σ, and change M’s bound variables so that xis neither acted on by σnor free in σ. By the induction hypothesis, N,Oand Pare SC under substitution, so Nσ,Oσ and P σ are SC. Given SC Qϕ, we have P σ[x7→ Q] is SC. Thus, by Lemma 5.9,NσLOσ, x.P σMis SC; but this is just Mσ. •If Mis NLOM: take any SC substitution σ. By the induction hypothesis, Nand Oare SC under substitution, so Nσ and Oσ are SC. Thus, by Lemma 5.10,NσLOσMis SC; but this is just Mσ. •If Mis NLhx, yi.OM: take any SC substitution σ, and change M’s bound variables so that xand yare neither acted on by σnor free in σ. By the induction hypothesis, Nand Oare SC under substitution, so Nσ and Oσ are SC. Given SC Pϕand Qψ,O[x7→ P, y 7→ Q] is SC. Thus, by Lemma 5.11,NσLhx, yi.OσMis SC; but this is just Mσ. •If Mis NLx.O, y.P M: take any SC substitution σ, and change M’s bound variables so that xand yare neither acted on by σnor free in σ. By the induction hypothesis, N,Oand Pare SC under substitution, so Nσ,Oσ and P σ are SC. Given SC Qϕand Rψ,Oσ[x7→ Q] and P σ[y7→ R] are SC. Thus, by Lemma 5.12,NσLx.Oσ, y.P σMis SC; but this is just Mσ. Corollary 5.15.All terms are strongly normalizing. Proof: Take any term M. By Theorem 5.14,Mis SC under substitution; clearly, then, Mis SC. (Consider the substitution [xϕ7→ xϕ].) By Definition 5.1, then, Mis strongly normalizing. Core Type Theory 183 6. Conclusion In this paper, we’ve presented a natural deduction system for core logic, and developed a term calculus that corresponds to this natural deduction system. We’ve defined two reduction relations on this term calculus—principal and full reduction—and explored the ways that core logic’s restrictions make reduction somewhat different from reduction in more familiar term calculi. We’ve discussed the Prawitz restriction and our reasons for dropping it. And finally, we’ve shown that principal reduction in this system is strongly normalizing (although it would not be with the Prawitz restriction in place). In future work, we hope to extend this strong normalization to full reduction as well, but as that will require different techniques, only time will tell. Acknowledgements. This research was supported by the Monash Faculty of Information Technology, the Monash Laboratory for the Foundations of Computing, the Australian Research Council fellowship “Substructural logics for bounded resources” (FT190100147), and PLEXUS (grant agreement 101086295), a Marie-Sk lodowska-Curie action funded by the EU under the Horizon Europe Research and Innovation Programme. Many thanks also to Sara Ayhan and Neil Tennant for helpful discussions, to Elaine Pimentel for pointing us to [4], and to two anonymous referees for their comments. References [1] S. Ayhan, H. Wansing, On synonymy in proof-theoretic semantics: The case of 2Int,Bulletin of the Section of Logic, vol. Online First (2023), DOI: https://doi.org/10.18778/0138-0680.2023.18. [2] H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, Elsevier, Amsterdam (1984). [3] A. Church, The Calculi of Lambda-Conversion, Princeton University Press, Princeton, New Jersey (1941). [4] A. D´ıaz-Caro, G. Dowek, A new connective in natural deduction, and its application to quantum computing, [in:] International Colloquium on Theoretical Aspects of Computing, Springer (2021), pp. 175–193, DOI: https://doi.org/10.1007/978-3-030-85315-0 11. 184 Emma van Dijk, David Ripley, Julian Gutierrez [5] G. Gentzen, Investigations Into Logical Deduction (1935), [in:] M. E. Szabo (ed.), The Collected Papers of Gerhard Gentzen, North-Holland Publishing Company, Amsterdam (1969), pp. 68–131. [6] J. Girard, P. Taylor, Y. Lafont, Proofs and Types, Cambridge University Press, Cambridge (1989). [7] J. Hindley, J. P. Seldin, Lambda-Calculus and Combinators: an Introduction, Cambridge University Press, Cambridge (2008), DOI: https://doi.org/10.1017/CBO9780511809835. [8] W. H. Howard, The formulae-as-types notion of construction (1969), [in:] To HB Curry: Essays on combinatory logic, lambda calculus, and formalism, Academic Press (1980), pp. 479–490. [9] D. Leivant, Assumption classes in natural deduction,Mathematical Logic Quarterly, vol. 25(1–2) (1979), pp. 1–4, DOI: https://doi.org/10.1002/ malq.19790250102. [10] S. Negri, J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge (2001), DOI: https://doi.org/10.1017/ CBO9780511527340. [11] M. Petrolo, P. Pistone, On paradoxes in normal form,Topoi, vol. 38(3) (2019), pp. 605–617, DOI: https://doi.org/10.1007/s11245-018-9543-7. [12] D. Prawitz, Natural Deduction: A Proof-Theoretical Study, Almqvist and Wiksell, Stockholm (1965). [13] D. Ripley, Strong normalization in core type theory, [in:] I. Sedl´ar, M. Blicha (eds.), The Logica Yearbook 2019, College Publications (2020), pp. 111– 130. [14] M. H. Sørensen, P. Urzyczyn, Lectures on the Curry-Howard isomorphism, Elsevier (2006). [15] N. Tennant, Anti-Realism and Logic, Oxford University Press, Oxford (1987). [16] N. Tennant, Natural deduction and sequent calculus for intuitionistic relevant logic,Journal of Symbolic Logic, vol. 52(3) (1987), pp. 665–680, DOI: https://doi.org/10.2307/2274355. [17] N. Tennant, Autologic: Proof theory and automated deduction, Edinburgh University Press, Edinburgh (1992). [18] N. Tennant, On Paradox without Self-Reference,Analysis, vol. 55(3) (1995), pp. 199–207, DOI: https://doi.org/10.2307/3328581. Core Type Theory 185 [19] N. Tennant, What is Negation?, [in:] D. M. Gabbay, H. Wansing (eds.), Negation, Absurdity, and Contrariety, Kluwer Academic Publishers, Dordrecht (1999), pp. 199–222, DOI: https://doi.org/10.1007/978-94-0159309-0 10. [20] N. Tennant, Ultimate normal forms for parallelized natural deductions, Logic Journal of the IGPL, vol. 10(3) (2002), pp. 299–337, DOI: https://doi.org/doi.org/10.1093/jigpal/10.3.299. [21] N. Tennant, Cut for Core Logic,Review of Symbolic Logic, vol. 5(3) (2012), pp. 450–479, DOI: https://doi.org/10.1017/S1755020311000360. [22] N. Tennant, Core Logic, Oxford University Press, Oxford (2017). [23] H. Wansing, Proofs, disproofs, and their duals, [in:] L. Beklemishev, V. Goranko, V. Shehtman (eds.), Advances in Modal Logic, vol. 8, College Publications (2010), pp. 483–505. [24] H. Wansing, Falsification, natural deduction and bi-intuitionistic logic, Journal of Logic and Computation, vol. 26(1) (2016), pp. 425–450, DOI: https://doi.org/10.1093/logcom/ext035. [25] H. Wansing, A more general general proof theory,Journal of Applied Logic, vol. 25(1) (2017), pp. 23–46, DOI: https://doi.org/10.1016/j.jal.2017. 01.002. Emma van Dijk Independent scholar Melbourne, VIC, Australia e-mail: emmav[email protected] David Ripley Monash University Philosophy Department, SOPHIS Building 11, Monash University Clayton, VIC, Australia e-mail: dav[email protected]