Stabilizing Quantum Disjunction
- 261 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 conversion1 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.
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.
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.
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
(with n and mfresh2 for \(\mathscr {D}\))
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
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.
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 }}\).
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.
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 Γ.
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 .
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
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.
where C is distinct from each A i .
7 Comparison with Jacinto and Read’s GE-stability
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.
where f h is the h th choice function considered above.
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.
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.
in which the elimination rules are applied in a different order.
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.
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.
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.
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.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.
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.
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.
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.
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.
- 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.
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.Belnap, N.D. (1962). Tonk, plonk and plink. Analysis, 22(6), 130–134.CrossRefGoogle Scholar
- 2.Dicher, B. (2016). Weak disharmony: some lessons for proof-theoretic semantics. Review of Symbolic Logic, 9(3), 583–602.CrossRefGoogle Scholar
- 3.Dummett, M. (1981). Frege. Philosophy of language, 2edn. London: Duckworth.Google Scholar
- 4.Dummett, M. (1991). The logical basis of metaphysics. London: Duckworth.Google Scholar
- 5.Francez, N. (2017). On harmony and permuting conversions. Journal of Applied Logic, 21, 14–23.CrossRefGoogle Scholar
- 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.Jacinto, B., & Read, S. (2017). General-elimination stability, Studia Logica. Online First. https://doi.org/10.1007/s11225-016-9692-x.
- 8.Prawitz, D. (1965). Natural deduction. A proof-theoretical study. Stockholm: Almqvist & Wiksell. Reprinted in 2006 for Dover Publication.Google Scholar
- 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.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.Prior, A.N. (1960). The runabout inference-ticket. Analysis, 21(2), 38–39.CrossRefGoogle Scholar
- 12.Schroeder-Heister, P. (1981). Untersuchungen zur regellogischen Deutung von Aussagenverknüpfungen, PhD thesis, Bonn University.Google Scholar
- 13.Schroeder-Heister, P. (1984). A natural extension of natural deduction. The Journal of Symbolic Logic, 49(4), 1284–1300.CrossRefGoogle Scholar
- 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.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.Steinberger, F. (2013). On the equivalence conjecture for proof-theoretic harmony. Notre Dame journal of Formal Logic, 54(1), 79–86.CrossRefGoogle Scholar
- 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.Tranchini, L. (2016). Proof-theoretic harmony: towards an intensional account, Synthese, Online First. https://doi.org/10.1007/s11229-016-1200-3.
- 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
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.