Advertisement

Stabilizing Quantum Disjunction

  • Luca Tranchini
Open Access
Article
First Online:
Received:
Accepted:
  • 646 Downloads

Abstract

Since the appearance of Prior’s tonk, inferentialists tried to formulate conditions that a collection of inference rules for a logical constant has to satisfy in order to succeed in conferring an acceptable meaning to it. Dummett proposed a pair of conditions, dubbed ‘harmony’ and ‘stability’ that have been cashed out in terms of the existence of certain transformations on natural deduction derivations called reductions and expansions. A long standing open problem for this proposal is posed by quantum disjunction: although its rules are intuitively unstable, they pass the test of existence of expansions. Although most authors view instabilities of this kind as too subtle to be detected by the requirement of existence of expansions, we first discuss a case showing that this requirement can indeed detect instabilities of this kind, and then show how the expansions for disjunction-like connectives have to be reformulated to rule out quantum disjunction. We show how the alternative pattern for expansions can be formulated for connectives and quantifiers whose rules satisfy a scheme originally developed by Prawitz and Schroeder-Heister. Finally we compare our proposal with a recent one due to Jacinto and Read.

Keywords

Harmony Stability Expansion Quantum-disjunction Permutative conversion 

1 Harmony via Reductions and Expansions

According to inferentialism, the meaning of logical constants is given by laying down their inference rules. Prior [11] convincingly argued that not every collection of rules succeeds in endowing a logical constant with an acceptable meaning. Since then, inferentialists wrestled with the task of finding an appropriate characterization of the condition for inference rules to count as proper inferential definitions, a condition called, after Dummett [3, 4], harmony.

When rules are given in the setting of Gentzen [6] natural deduction, aproposal that has gained popularity is that of understanding harmony as the requirement that

What can be inferred from alogically complex sentence governed by acertain logical constant using its elimination rules should be no more and no less than what is needed in order to derive that very logically complex sentence using its introduction rules.

Dummett [4] sometimes uses ‘harmony’ to refer to both the no less and the no more aspects of this informal characterization, and sometimes to refer only to the no more part, using ‘stability’ to refer to the no less part.

It is quite uncontroversial that the rules for Prior’s :
display no match between what can be inferred from A B using E and what is needed to establish A B using I, and it is also quite uncontroversial that the (Gentzen-Prawitz) conjunction rules
display a perfect match. One way of cashing out the perfect match displayed by harmonious rules consists in observing that they give rise to two particular kinds of deductive patterns. Patterns of the first kind are constituted by an application of an introduction rule followed immediately by one of the corresponding elimination rules, and have been referred to as hillocks [19] or complexity peaks [4], since in these patterns one finds a formula which is more logically complex than those surrounding it:
The occurrence of a pattern of this kind within a derivation certainly constitutes a redundancy, since what is obtained from the elimination must have already been established, if the major premise of the elimination (i.e. the premise containing the logical constant to be eliminated) was obtained by introduction. Thus, when rules are in harmony, complexity peaks can be levelled, the levelling procedure being referred to as reduction. In the case of conjunction, the levelling procedure consists in replacing, within a derivation, patterns of the above kind with the following:
$$\begin{array}{c} \mathscr{D}_{1}\\ A\end{array} $$
A similar procedure allows to level complexity peaks constituted by an application of the introduction rule followed by an application of the second elimination rule.

Existence of reductions reflects the no more aspect of harmony, since it shows that what one gets from an elimination is no more than what has to be established in order to infer its major premise by introduction.

Patterns of the other kind may be referred to as valleys or complexity riffs, since logical complexity goes down and then up again as a result of an application of an introduction following applications of the elimination rules:
In this case, it is the possibility of expanding a derivation ending with A&B that has been taken to reflect the no less aspect of harmony. The expansion, which can be depicted as follows:

makes clear that what one gets from the elimination is no less that what one needs in order to reintroduce the logically complex sentence A&B using the introduction rules.

It is worth observing that this account of harmony does not consist in imposing certain conditions on derivability, but rather in imposing certain requirements on the internal structure of derivations, namely the possibility of transforming them according to some operations. Thus this account of harmony is not mainly concerned with what a collection of inference rules allows one to derive, but rather with how a certain collection of rules allows one to establish certain derivability claims. For this reason it has been dubbed “intensional” [18] in contrast to other “extensional” accounts of harmony, such as the one of [1] or of [17].

2 The Problem with “Quantum” Disjunction

The account of harmony in terms of reductions and expansions is however threatened by a difficulty which goes back to some remarks of Dummett [4]. The difficulty arises in connection with the rules for disjunction:
Like in the case of conjunction, it is quite uncontroversial that the rules satisfy both aspects of the informal characterization of harmony, and in fact deductive patterns of the two kinds just discussed, as well as reductions and expansions can be exhibited in this case as well:1
(Also in this case an analogous procedure allows for levelling complexity peaks constituted by applications of the second introduction rule followed by an application of the elimination rule.)

(with n and mfresh2 for \(\mathscr {D}\))

Besides these rules for disjunction (which in most formulations are common to both intuitionistic and classical logic), Dummett discusses also those for quantum disjunction (more commonly referred to as lattice disjunction) \(\overline {\vee }\). The rules for this connective differ from those of standard disjunction in that the elimination rule comes with a restriction, to the effect that the rule can be applied only when the minor premises C depend on no other assumptions than those that get discharged by the rule application (we indicate this using double square bracket in place of the usual ones):

Using the elimination rule for quantum disjunction one can derive from A∨¯ B less than what one can derive from a A ∨ B using ∨E. Thus, on the assumption that the standard rules for disjunction are in perfect balance, we expect the rules for quantum disjunction not to be in perfect harmony.3 In particular, we expect the no less aspect of harmony not to be met. That is, we expect the rules for \(\overline {\vee }\) to be unstable.4

However, and here is the problem, reductions and expansions are readily available in the case of quantum disjunction as well (again with double square brackets we indicate that no other assumptions than those indicated occur in \(\mathscr {D}_{1}\) and \(\mathscr {D}_{2}\)):

Observe in particular that the restriction on \({\overline {\vee }}\)E is satisfied by the applications of the rule in the expanded derivations and thus that, though unstable, the restricted elimination rule allows one to derive from A∨¯ B no less than what is needed in order introduce A∨¯ B back again.

Most authors (see, e.g., [2, 16]) have taken the modest stance of regarding instabilities of this kind as too subtle to be ruled out by the existence of expansions. In the remaining part of the paper we argue against this modest stance, by showing that, once properly formulated, expansions are perfectly capable of detecting instabilities of this kind.

3 Intermezzo: “Quantum-like” Implication

Before reformulating the expansion pattern for disjunction, we would like to point at some independent evidence in favour of the view that the existence of expansions should rule out instabilities of this kind. In so doing, we hope to dispel the possible mistaken impression that our solution to the problem of quantum disjunction is merely ad hoc.

The Gentzen-Prawitz rules for (classical and intuitionistic) implication are the following:
That the rules are in harmony is shown by the following:
The aforementioned evidence in favour of our bolder stance towards stability and expansions arises when one considers a restriction on ⊃I analogous to the one yielding to quantum disjunction (also briefly discussed by [4] p. 289 as a case of instability). Let \(\overline {\supset }\) be the ‘quantum-like’ implication connective governed by the following rules:

where the introduction rule is restricted to the effect that it can be applied only when the premise B depends on no other assumptions than those of the form A that get discharged by the rule application.

The restricted introduction rule sets higher standards for inferring a sentence of the form \(A{\overline {{\supset }}} B\) than those set by ⊃I to derive a sentence of the form A⊃B. Thus, on the assumption that modus ponens is in perfect harmony with the standard introduction rule, we expect it not to be in perfect harmony with the restricted introduction rule. In particular, as the restricted introduction rule sets higher standards to derive an implication, we expect modus ponens not to permit to derive from \(A{\overline {{\supset }}} B\) all that is needed to introduce \(A{\overline {{\supset }}} B\) again using its introduction rule. In other words, we expect also in this case the no less aspect of harmony not to be met. That is we expect the rules for \({\overline {{\supset }}}\) to be unstable, the kind of instability at stake being the same as the one flawing the rules for \({\overline {\vee }}\).

As in the case of \({\overline {\vee }}\), in the case of \({\overline {{\supset }}}\) we have a reduction readily available which shows that – as expected – the no more aspect of harmony is satisfied:
Moreover, it is easy to see that the expansion pattern for standard implication does not work for quantum-like implication, as the application of \(\overline {\supset }\)I would violate the restriction that the premise B depends on no other assumptions than those of the form A that get discharged by the rule: In the expanded pattern B would depend not only on A but also on all assumptions on which \(A\overline {\supset }B\) depends:

The requirement that it should be possible to equip the rules with both reductions and expansions is thus capable of detecting the instability of the rules of quantum-like implication. We take this as a reason to consider an alternative pattern for the expansion of disjunction, namely one capable of detecting the disharmony induced by the restriction on the quantum disjunction elimination rule.5

4 Generalizing the Expansions for Disjunction

The expansion pattern for disjunction we considered above – which was first proposed by Prawitz [9] – gives the instructions to expand a derivation in which the sentence governed by disjunction figures as conclusion of the whole derivation.

The idea behind the alternative pattern is that an expansion operates on a formula which is not, in general, the conclusion of a derivation, but on one that occurs at some point in the course of a derivation. Consider a derivation \(\mathscr {D}\) in which the formula A ∨ B may occur at some point. Such a derivation may be depicted as follows:

that is it may be viewed as the result of plugging a (certain number k ≥ 0) of copies of a derivation \(\mathscr {D}^{\prime }\) of A ∨ B on top of a derivation \(\mathscr {D}^{\prime \prime }\) of C depending on (k copies of) the assumption A ∨ B, possibly alongside other assumptions Γ.

It is certainly true that Prawitz’s expansion can also be used to expand a derivation \(\mathscr {D}\) of this form: To expand \(\mathscr {D}\), we can apply Prawitz’s expansion to the upper chunk \(\mathscr {D}^{\prime }\) of \(\mathscr {D}\) (in which A ∨ B figures as conclusion), and then we can plug the result of the expansion on top of the lower chunk \(\mathscr {D}^{\prime \prime }\) of \(\mathscr {D}\), thereby obtaining the following :
It is however possible to define an alternative procedure to directly expand the whole of \(\mathscr {D}\), namely the following:

In the alternatively expanded derivation, the application of the elimination rule ∨E is postponed to the effect that its minor premises are not the two copies of A ∨ B obtained respectively by ∨I1 and ∨I2 (as in Prawitz’s expansion), but rather two copies of C which are the conclusions of two copies of the lower chuck \(\mathscr {D}^{\prime \prime }\) of \(\mathscr {D}\) that now constitute the main part of the derivations of the minor premises of the application of ∨E.

This alternative pattern, first proposed by Seely [15], is a generalization of Prawitz’s expansion pattern: Each instance of Prawitz’s pattern corresponds to an instance of the alternative pattern in which the lower chunk \(\mathscr {D}^{\prime \prime }\) of the derivation \(\mathscr {D}\) is ‘empty’ i.e. it just consists of the sentence A ∨ B .

Moreover, it is easy to see that we cannot replace ∨ with \({\overline {\vee }}\) in the above pattern for generalized expansions, since the application of \({\overline {\vee }}\)E in the expanded derivation would violate the quantum restriction: The minor premises C would not depend only on the assumptions of the form A and B that get discharged by the rules, but also on all other undischarged assumptions of \(\mathscr {D}^{\prime \prime }\):

Thus when stability is understood as the existence of generalized expansions, quantum disjunction does turn out to be unstable, in accordance with what we would expect.

5 Stability and Permutations

It is worth observing that, combined with the reductions, the generalized expansion allows to recover all kind of conversions usually dicussed in the literature on natural deduction. For example, the permutative conversions first introduced by Prawitz [8, Ch. IV] in order to establish the normalization theorem for the natural deduction system of intuitionistic logic:6
can be “simulated” by first performing an expansion on the derivation on the left-hand side of the permutation: by instantiating in the schema for the generalized expansion given on page 8 \(\mathscr {D}^{\prime }\) with \(\mathscr {D}_{1}\) and \(\mathscr {D}^{\prime \prime }\) with
one obtains the following derivation:

in which the two rightmost occurrences of A ∨ B constitute two complexity peaks. Their reduction yields the derivation on the right-hand side of the permutation.

The relevance of permutations to harmony and in particular for stability, was already pointed out by Dummett [4] and has been recently stressed by Francez [5]. The fact that permutative conversions can be recovered from generalized expansions thus provides on the one hand further evidence for the significance of permutative conversions for an inferential account of meaning, and on the other hand, offers further reasons to view the generalized expansion as the proper way to capture stability.

6 Generalized Expansions for Arbitrary Connectives and Quantifiers

The alternative expansion pattern is readily available for all connectives satisfying the scheme first proposed by Prawitz [10] and then refined by Schroeder-Heister [12, 13, 14]. For a detailed formal treatment we refer the interested reader to [18]. In this section, we summarize the results presented there for arbitrary connectives, and sketch how they can be generalized to arbitrary first-order quantifiers.

In the simplest case, a connective satisfying the Prawitz–Schroeder-Heister scheme (for short a PSH connective) is governed by a collection of r ≥ 0 distinct introduction rules of the following form:
where for all 1 ≤ k ≤ r and 1 ≤ j ≤ m k there is an 1 ≤ i ≤ n such that B k j ≡ A i , and by a (unique) elimination rule with r minor premises:

where C is distinct from each A i .

Each complexity peak constituted by an application of one of the introductions followed by an application of the elimination can be get rid of as follows (we abbreviate ‡ (A1,…,A n ) with ‡):
and given a derivation \(\mathscr {D}^{\prime }\) of C depending on some assumptions of the form ‡ (A1,…,A n ) and a derivation \(\mathscr {D}\) of ‡ (A1,…,A n ) we have that (again we abbreviate ‡ (A1,…,A n ) with ‡):
The previously discussed disjunction rules are obtained by instantiating these schemata for r = 2 and m1 = m2 = 1. To give a further example, for r = 1 and m1 = 2 we obtain the PSH connective with the same introduction rule of standard (Gentzen-Prawitz) conjunction:7
for which we have the following reduction and (generalized) expansion:
We intend the schema to cover also the limit case of m = 0 that gives us the standard intuitionistic rules for ⊥:
for which we have no reduction but the following (generalized) expansion:
In the setting of Schroeder-Heister’s calculus of higher level rules the above schemata cover also the cases in which the B k j s are not formulas (i.e. rules of lowest level), bur rules of arbitrary level.8 For example the PSH connective with the same introduction rule as ⊃ is governed by the following rules:
for which we have the following reduction:9
and (generalized) expansion:
It should be clear that the schemata above can be generalized to apply to the more general class of connectives whose introduction rules may not only be of arbitrary higher level but also contain propositional quantification (as in [14]). A generalization covering first-order quantification is also possible and expectedly straightforward. We limit ourselves to discuss a (hopefully suggestive) example, the binary quantifier encoded by the I corner of the traditional square of oppositions (“Some A are B”). Its introduction and elimination rules are the following (with A(t) we indicate the result of replacing t for x in A, similarly for A(y), B(t) and B(y); the free occurrences of x in A and B are bound in I x (A,B)):
where y must satisfy an eigenvariable condition, i.e. it cannot occur free in any assumption of the sub-derivation of the minor premise C other than those discharged by the rule, nor in the minor premise C. Clearly, also for this quantifier we have a reduction and a (generalized) expansion following the pattern of those of ∧ above:

7 Comparison with Jacinto and Read’s GE-stability

What the alternative expansion expresses is ageneralization of the no less aspect of harmony that could be roughly approximated as follows:

The elimination rule should allow to derive no less than what is needed to derive all consequences from alogically complex sentence of agiven form.

The need of generalizing the usual formulation of the no less aspect of harmony in order to properly capture stabilty has been recently pointed out by Jacinto and Read [7], who refer to the original formulation of the no less aspect of harmony as local completeness and propose to replace it in favour of what they call generalized local completeness.

Rather than cashing out stability by formulating generalized expansions as we did, Jacinto and Read formalize stability as a complex requirement on derivability. It is true that, in order to establish that the members of the family of connectives they consider do satisfy the condition, they show how to construct a derivation which closely resembles the (generalized) “expanded” derivations obtained by our generalized expansions. There are however some crucial shorcomings of Jacinto and Read approach that stems from the fact that Jacinto and Read consider elimination rules of a different form from the one we considered.

In particular, given a collection of r introduction rules for a connective ‡ of the above form, they consider all choice functions that select one of the premises of each of the r introduction rules of ‡. Clearly, the number of these functions is the product of the numbers m k (1 ≤ k ≤ r) of premises of each of the r introduction rules, thus for each \(1\leq h \leq {\prod }_{k = 1}^{r} m_{k}\) we have a choice function f h such that for each 1 ≤ k ≤ r, f h (k) = B k j for some 1 ≤ j ≤ m k . A connective ‡ governed by r introduction rules obeys Jacinto and Read’s scheme (for short is a JR connective) if and only if its collection of elimination rules consists of \({\prod }_{k = 1}^{r} m_{k}\) rules, each of which has the following form:

where f h is the h th choice function considered above.

Connectives whose collections of introduction rules consist of rules of at most one premise (as in the case of disjunction) satisfy the PSH scheme if and only if they satisfy the JR scheme. Not so if at least one of the introduction rules has more than one premises. However, pairs of connectives obeying respectively one of the two schemata and sharing the collection of introduction rules are “interderivable”. For instance the JR connective with the same introduction rule of & and ∧ is governed by the following rules:

and clearly A ∧ B is interderivable with A ⋅ B in a system containing both connectives.

In general, a PSH connective is interderivable with the formula \(\bigvee _{k = 1}^{r} \bigwedge _{j = 1}^{m_{k}} \overline {B_{kj}}\) in the extension of Gentzen-Prawitz natural deduction system for intuitionistic logic with the connective in question, and similarly a JR connective is interderivable with the forumla \(\bigwedge _{h = 1}^{{\Pi }_{k = 1}^{r} m_{k}} \bigvee _{k = 1}^{r} \overline {B_{kf_{h}(k)}}\).10 The interderivability of the two intuitionistic formulas follows by a generalized distributivity principle. An analogous reasoning shows that the two connectives are interderivable in a system containing both.

When it comes to quantifiers however – and this is the first shortcoming – the JR scheme shows its deficiency. Apart from the case of quantifiers with at most one premise in each introduction rule (in which case the JR scheme delivers the same elimination rule as the PSH scheme) the JR scheme delivers elimination rules which are not stable. The JR quantifier with the same introduction rule as I above should be governed by the following rules:
with an eigenvariable condition on y in the two elimination rules. Contrary to the case of I, in the case of I′ it is not even possible to formulate an expansion following the simpler pattern of Prawitz, since the application of the first elimination rule would violate the eigenvariable condition:

In general, it does not seem that the JR scheme can deliver stable rules for quantifiers apart from those instances in which it coincides with the PSH scheme.

But even leaving the quantifiers aside, the approach of Jacinto and Read is not fully satisfactory. To begin with a simple example, in establishing that the connective ⋅ introduced above satisfies the condition for generalized local completeness, Jacinto and Read show how to construct the following derivation:
Although they do not define an operation of expansion, one could argue that they could have defined it, by positing the derivation just given as what one obtains by expanding the following:
However, there is no principled reason why the expansion of this derivation should not rather be the following:

in which the elimination rules are applied in a different order.

By looking at connectives governed by collections of more complex introduction rules, one immediately realizes that the problem is not just the order in which the different elimination rules are applied. Consider the following quaternary JR connective (we abbreviate ⊙ (A,B,C,D) with ⊙):
Using Jacinto and Read’s receipt, one can cook up the following derivation:
However, also in this case there is no principled reason to claim that a derivation of the form:
should expand that way rather than, say, this way:

where not only the order, but also the number of applications of the different elimination rules changes. By considering connectives with more complex introduction rules, the situation quickly becomes unwieldy as to the number of possible ways of expanding a given derivation.

In the light of this, it thus seems to be no accident that Jacinto and Read do not seem to envisage the possibility of cashing out their generalization of the no less aspect of harmony in terms of (generalized) expansions as it has been done here. For the family of connectives they consider, there is no operation (i.e. function) to expand a given derivation, since in their case the process of expansion is, at best, highly non-deterministic.

It is instructive to compare ⊙ with the PSH connective with the same collection of introduction rules:
For this connective, we only need two reductions (instead of the the eight reductions that Jacinto and Read have to lay down), and the way in which a derivation should be expanded is unequivocally determined: in the expanded derivation each of the introduction rules and the elimination rule is applied exactly once, and each rule application discharges exactly one copy of each dischargeable assumption:
Finally, even if one wished to admit non-deterministic expansions for JR connectives, the value of the expansions would still be doubtable. In particular, it is unclear whether it is possible to recover permutative conversions for the JR elimination rules using a combination of expansions and reductions as we have done for disjunction above. The strategy used to simulate the permutation for disjunction elimination generalizes straightforwardly to all PSH connectives. For instance we have that:
and the latter reduces to
The same is not true for JR connectives, where we get, for instance:
and the latter reduces to following rightmost (and not leftmost, as desired) derivation:

The remarks contained in this section are not meant to deny that JR connectives are also stable (though JR quantifier certainly are not!), but only to point out that an exact formulation of generalized expansions for JR connectives requires further investigation.

8 Conclusions

We have shown how the instability of quantum disjunction can be ruled out by requiring that introduction and elimination rules should allow the formulation of expansions, provided the latter are properly understood. We have shown how the alternative pattern for expansions can be formulated for the family of connective satisfying the scheme first proposed by Prawitz and Schroeder-Heister, and sketched how it can be applied to a family of quantifiers whose rules are obtained by opportunely generalizing that scheme. Finally we compared the results with a recent proposal of Jacinto and Read, showing its weaknesses compared to ours.

Footnotes

  1. 1.

    We observe the notational conventions of [8]: In rule schemata, we use square brackets to indicate the form of the assumptions that can be discharged by rule applications. In derivations, on the other hand, a formula in square brackets indicates an arbitrary number (≥ 0) of occurrences of that formula, if the formula is in assumption position, or of the whole sub-derivation having the formula in brackets as conclusion; discharge is indicated with letters placed above the discharged assumptions and to the left of the inference line of the rule application discharging the assumptions.

  2. 2.

    By this we mean that the application of ∨E in the expanded derivation discharges no assumptions of the form A and B in \(\mathscr {D}\).

  3. 3.
    Prompted by a remark of one of the referees, we observe that we are not assuming that given a collection of introduction rules, at most one collection of elimination rules can be in perfect harmony with it. We only assume that if a collection of elimination rules is in harmony with a given collection of introduction rules, a necessary condition for another collection of elimination rules to be also in harmony with that collection of introduction rules is that the two collections of elimination rules are interderivable. (A collection of rules \(\mathbb {R}\) is interderivable with another collection \(\mathbb {R}^{\prime }\) when for each rule R of \(\mathbb {R}\) there is a derivation \(\mathscr {D}\) of the conclusion of R from (at most all) the premises of R such that \(\mathscr {D}\) consists only of rules in \(\mathbb {R}^{\prime }\), and vice versa.) That this condition is not sufficient is suggested by the operator governed by the following (doubtly harmonious) rules:

    For a more substantial example and discussion cf. [18].

  4. 4.

    According to one of the referees, the difficulty with quantum disjunction consists in the fact that in a system containing both standard disjunction and quantum disjunction the two connectives are interderivable, i.e. they “collapse” on one another. It is true that the collapse of quantum disjunction on standard disjunction is clearly related to the problem of stability. However, at least according to Dummett [4, p. 290], this is “another interesting phenomenon illustrated by the restricted ‘or’-elimination rule”, rather than than an illustration of the failure of stability itself. In fact, stability (in Dummett’s sense at least) seems to be orthogonal to this kind of “collapses”: An analogous collapse takes place if one considers a natural deduction system with both intuitionistic and classical negation, but this is usually (and certainly by Dummett) not taken as a reason for deeming intuitionistic negation as unstable. Conversely, as it is shown by the expample discussed in the next section, we may have instability (in Dummett’s sense) without an analogous collapse taking place (see below footnote 5). Although the point is certainly debatable, the given reconstruction is, at least, sound to Dummett’s intent.

  5. 5.

    It is worth remarking that, contrary to what happens in the case of the two disjunctions, ‘quantum like’ implication does not collapse on standard implication in a system containing both connectives (although A⊃B is implied by \(A{\overline {{\supset }}} B\), the converse is not true). As for Dummett the rules of ‘quantum-like’ implication give rise to a situation of instability analogous to the one of quantum disjunction, the collapse issue cannot be the heart of the problem for him (cf. footnote 4 above).

  6. 6.

    In the derivation schemata, \(\langle \mathscr {D}\rangle \) indicates the possible presence of minor premises in ‡E, where ‡E stands for the elimination rule of some connective ‡.

  7. 7.

    We say that two connectives ♯ and ♭ have (or share) the same collection of introduction rules iff the introduction rules for ♯ can be obtained from those for ♭ by replacing each occurrence of ♭ with ♯, and viceversa.

  8. 8.
    For a definition of how the schemata

    are to be understood in the context of the calculus of higher level rules see [12, p. 60–65, in German] and [18, Appendix].

  9. 9.
    A derivation of the rule A ⇒ B is equated by definition with a derivation of B from A, thus the derivation \(\mathscr {D}\) of B from A is ipso facto a derivation of A ⇒ B. The result of substituting the derivation \(\mathscr {D}\) of A ⇒ B for the rule assumption A ⇒ B in \(\mathscr {D}^{\prime }\) can be informally decribed as the derivation which results by removing all applications of the assumption rule A ⇒ B in \(\mathscr {D}^{\prime }\) and inserting \(\mathscr {D}\) to fill the gap, i.e. by successively replacing all patterns of the form on the right with patterns of the form on the left.

    Observe that depending on the number of copies of the assumption A in \(\mathscr {D}\) and the number of applications of A ⇒ B in \(\mathscr {D}^{\prime }\), the operation requires a quite involved transformation already for a rule of almost lowest level such as A ⇒ B. For the exact definition (covering rules of arbitrary level) see references in footnote 8.

  10. 10.

    Where \(\overline {B_{kj}}\) is just B k j if the latter is a formula; if B k j is a rule of the form R1,…,R l ⇒ B, then \(\overline {B_{kj}}\) is \((\overline {R_{1}}\wedge ({\ldots } \wedge \overline {R_{l}})\ldots )\supset B\). For a proof of these claims see [10] and [7, Theorem 2].

Notes

Acknowledgements

I thank both referees for insightful comments on previous versions of the paper. This work has been financed by the Deutsche Forschungsgemeinschaft as part of the project “Logical Consequence and Paradoxical Reasoning” (Tr1112/3-1) and by the Deutsche Forschungsgemeinschaft and the Agence Nationale de la Recherche as part of the project “Beyond Logic” (Schr 275/17-1).

References

  1. 1.
    Belnap, N.D. (1962). Tonk, plonk and plink. Analysis, 22(6), 130–134.CrossRefGoogle Scholar
  2. 2.
    Dicher, B. (2016). Weak disharmony: some lessons for proof-theoretic semantics. Review of Symbolic Logic, 9(3), 583–602.CrossRefGoogle Scholar
  3. 3.
    Dummett, M. (1981). Frege. Philosophy of language, 2edn. London: Duckworth.Google Scholar
  4. 4.
    Dummett, M. (1991). The logical basis of metaphysics. London: Duckworth.Google Scholar
  5. 5.
    Francez, N. (2017). On harmony and permuting conversions. Journal of Applied Logic, 21, 14–23.CrossRefGoogle Scholar
  6. 6.
    Gentzen, G. (1935). Untersuchungen über das logische Schließen, Mathematische Zeitschrift 39. eng. transl. Investigations into logical deduction. In Szabo, M.E. (Ed.) The collected papers of Gerhard Gentzen, North-Holland 1969 (pp. 68–131).Google Scholar
  7. 7.
    Jacinto, B., & Read, S. (2017). General-elimination stability, Studia Logica. Online First.  https://doi.org/10.1007/s11225-016-9692-x.
  8. 8.
    Prawitz, D. (1965). Natural deduction. A proof-theoretical study. Stockholm: Almqvist & Wiksell. Reprinted in 2006 for Dover Publication.Google Scholar
  9. 9.
    Prawitz, D. (1971). Ideas and results in proof theory. In Fenstad, J. (Ed.) Proceedings of the Second Scandinavian Logic Symposium, Vol. 63 of Studies in Logic and the Foundations of Mathematics (pp. 235–307): Elsevier.Google Scholar
  10. 10.
    Prawitz, D. (1979). Proofs and the meaning and completeness of the logical constants. In Hintikka, J., Niiniluoto, I., & Saarinen, E. (Eds.) Essays on Mathematical and Philosophical Logic: Proceedings of the Fourth Scandinavian Logic Symposium and the First Soviet-Finnish Logic Conference, Jyväskylä, Finland, June 29–July 6, 1976, Kluwer, Dordrecht (pp. 25–40).Google Scholar
  11. 11.
    Prior, A.N. (1960). The runabout inference-ticket. Analysis, 21(2), 38–39.CrossRefGoogle Scholar
  12. 12.
    Schroeder-Heister, P. (1981). Untersuchungen zur regellogischen Deutung von Aussagenverknüpfungen, PhD thesis, Bonn University.Google Scholar
  13. 13.
    Schroeder-Heister, P. (1984). A natural extension of natural deduction. The Journal of Symbolic Logic, 49(4), 1284–1300.CrossRefGoogle Scholar
  14. 14.
    Schroeder-Heister, P. (2014). The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony. Studia Logica, 102(6), 1185–1216.CrossRefGoogle Scholar
  15. 15.
    Seely, R.A.G. (1979). Weak adjointness in proof theory. In Proceedings of the Durham Conference on Applications of Sheaves, Vol. 753 of Springer Lecture Notes in Mathematics (pp. 697–701). Berlin: Springer.Google Scholar
  16. 16.
    Steinberger, F. (2013). On the equivalence conjecture for proof-theoretic harmony. Notre Dame journal of Formal Logic, 54(1), 79–86.CrossRefGoogle Scholar
  17. 17.
    Tennant, N. (2008). Inferentialism, logicism, harmony, and a counterpoint. In Coliva, A. (Ed.) Essays for Crispin Wright: Logic Language and Mathematics. Oxford: Oxford University Press.Google Scholar
  18. 18.
    Tranchini, L. (2016). Proof-theoretic harmony: towards an intensional account, Synthese, Online First.  https://doi.org/10.1007/s11229-016-1200-3.
  19. 19.
    von Plato, J. (2008). Gentzen’s proof of normalization for natural deduction. Bulletin of Symbolic Logic, 14(2), 240–257.CrossRefGoogle Scholar

Copyright information

© The Author(s) 2018

Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.

Authors and Affiliations

  1. 1.Wilhelm-Schickard-InstitutEberhard Karls Universität TübingenTübingenGermany

Personalised recommendations