Notes to Sentence Connectives in Formal Logic
1. Probably the best all-purpose understanding of what logics are would take them as equivalence classes of proof systems under the relation of having mutually interderivable rules, though even this ignores issues about translational equivalence across differing languages. For many practical purposes it is sufficient to individuate logics more coarsely, as consequence relations or generalized consequence relations, or even, as is common in some areas, simply sets of formulas.
2. There has been much controversy as to how well this or that set of rules governing implication or disjunction, for example, manages to capture the (putatively) corresponding natural language analogue—if-then, or (in the cases cited)—but this entry will not be considering such connective-specific issues.
3. This coincides with the algebraically defined notion of a context given above.
4. Sometimes we will speak of # as truth-functional over a class of valuations instead of truth-functional with respect to the class, when the immediate linguistic context contains another occurrence of the phrase “with respect to”.
5. See Leblanc (1966), p. 169 and n. 14; also Sundholm (2001), p. 38.
6. We could make the same point apropos of the consequence relation, ⊢∨ say, determined by the class of all boolean valuations.
7. Had the historical development of logic run differently and the framework we would naturally call Fmla-Set come to initial prominence, we would have been fussing about the consistent valuations being closed under disjunctive combinations, and the sequent-undefinability of the class of ∧-boolean valuations. As it is, we shall be hearing no more of + and ∑.
8. That is, if σ = Γ ≻ Δ and σ′= Γ′ ≻ Δ′, σ + σ′ is Γ, Γ′ ≻ Δ, Δ′.
9. A somewhat similar range of properties is the focus of Williamson (2006a), though with definitions that make the concepts in question apply to arbitrary linguistic contexts and not just to connectives (see Section 1 above), and without the explicit relativity to logics (consequence relations or generalized consequence relations).
10. The fact that a generalized consequence relation is a binary relation means that we need to distinguish symmetric and non-symmetric such relations, as in general, and means that it is an unwise terminological decision to call generalized consequence relations symmetric consequence relations, as in Dunn and Hardegree (2001), Chapter 6. There seems to be a confusion here between whether a binary relation is symmetric and whether the treatment of its two relata is symmetrical. Note, incidentally, that it is binary relations that are symmetric, not binary operations (connectives or otherwise), pace Restall (1999), p. 385, who writes of a binary operation corresponding to a kind of conjunction that it is “idempotent, symmetric, and associative”. The word wanted is ‘commutative’. (Of course a connective qua syntactic operation can never literally be commutative; what is meant is that the corresponding ‘Lindenbaum-algebraic’ operation on synonymy-classes of formulas is commutative.) Restall is in famous—if muddled—company here; compare Quine (1951), describing conjunction as transitive on one page (p. 18) and associative on the next. The present point is not that one should never use terminology appropriate to binary relations when speaking of connectives—since there is, for instance, for any valuation v the relation Rv, say, holding between φ and ψ just in case v(φ ∧ ψ) = T, and for boolean valuations at least, this relation is symmetric. It is just that a clearer head is called for than Quine and Restall—and many other writers—have displayed in jumbling up the binary relational terminology (reflexive, symmetric, transitive,…) with the binary operational terminology (idempotent, commutative, associative, …). Among the ‘others’ are Dunn and Hardegree (again), who write on p. 215 of Dunn and Hardegree (2001) of the “symmetry of conjunction”.
11. Just as the sequents of Set-Fmla can be thought of as those Set-Set sequents Γ ≻Δ with Δ having exactly one element, those of Fmla have the further feature that Γ is empty, making these sequents stand in a one-to-one correspondence with the formulas of the language, with which for practical purposes we may identify them, explaining the following words of the main text. There are still two possibilities here, though. When the axiomatic or ‘Hilbert’ approach is taken, the rules are formula-to-formula rules and the objects proved are formulas. On the other hand, in our initial presentation of natural deduction, before assumption discharging rules got into the act, the rules were again presented as formula-to-formula rules, but with the things proved with these rules were in effect Set-Fmla sequents: meaning that the rules enabled us to pass from a set of initial assumptions to a final formula. Should we say that the logical framework here is Set-Fmla on the basis of what ends up being proved, or that it is Fmla, on the basis of what the premisses and conclusions of the rules involved are? Now that the distinction has been duly noted, there is no urgent need to supply an answer to this question.
12. The two views contrasted here are distinguished in Meyer (1974).
13. In fact for any rules R ∪ {ρ}, ρ is derivable from R together with these structural rules if and only if Glo(R) ⊆ Glo(ρ).
14. Note that the operations + and · on valuations give least upper bounds and greatest lower bounds with respect to this partial order.
15. In fact, Garson works with a variation on the framework Set-Fmla which allows sequents Γ ≻ φ with Γ infinite, and this feature is essential to his proof of the claim here reported. Whether it is essential for the correctness of the claim, I do not know.
16. The condition for → in Garson (2001) has been misstated, and Garson (1990) should be consulted for the correct formulation.
17. Dummett (1991) provides an extended discussion of such positions. There is an interesting proposal in Peacocke (1987) for “reading off” (boolean) valuational semantics from inference rules found ‘primitively compelling’ by reasoners (as a necessary condition for their possessing the concepts expressed by and, or, etc.), which for some cases may be introduction rules and others elimination rules. This attractive suggestion has unfortunately come in for worrying criticism more recently: for example in Williamson (2006b).
18. Thus the consequence relation associated with the present natural deduction system is trivial—“almost inconsistent”, as it sometimes put—in the sense introduced apropos of Rautenberg’s maximality theorem in Section 2. (For a proper formulation of the natural deduction rules here the above formula-to-formula rules should be explicitly represented as sequent-to-sequent rules with a set parameter, “Γ” sitting on the left of a “≻”.) The provable sequents φ ≻ φ Tonk ψ and φ Tonk ψ ≻ ψ represent conditions on this consequence relation induced by the determinants ⟨T, x, T⟩ for x = T, F, in the former case and ⟨y, F, F⟩ for y = T, F, in the latter. Thus any valuation consistent with this consequence relation must respect each of two opposite determinants—making Tonk overdetermined—⟨T, F, T⟩, taking x = F and ⟨T, F, F⟩ taking y = T. The only valuations that respect both these determinants are vT, assigning T to every formula, and vF assigning F to every formula, and the logic determined by {vT,vF} is the smallest trivial consequence relation on the language concerned. This is our semantic gloss on the Tonk example. It would be quite wrong to diagnose the problem in terms of the non-existence of a truth-function corresponding to Tonk, or to say, as Stevenson (1961), p. 127, does, that the problem is that Prior “gives the meanings of connectives in terms of permissive rules, whereas they should be stated in terms of truth-function statements in a metalanguage.” (Prior (1976) replies to Stevenson, and inter alia suggests that the consequence relation just described can be thought of as “one-valued logic”—cf. Hamblin (1967); the better term would be constant-valued logic.) There is nothing incoherent about non-truth-functional—or more accurately, not fully determined—connectives: the problem arises from being overdetermined. The same objection, as Read (1988), p. 168, observes, appears to apply to the remark in Peacocke (1987) that the “semantical objection to tonk is that there is no binary function on truth values which validates both its introduction and its elimination rules”, though there is more room for manoeuvre here: the implicit suggestion is that coherence requires soundness, not soundness and completeness, under some truth-functional interpretation. This amounts to deeming unintelligible any connective whose logical properties are ‘strongly contra-classical’, in the terminology of Humberstone (2000a). But what does soundness under ‘some truth-functional interpretation’ mean? It will not do to say: soundness with respect to some V over which the connective in question is truth-functional, since the there may not be enough variety in the truth-values supplied by V to the formulas of the language, in which case its elements may respect the determinants for a truth-function only vacuously because some possibilities do not arise. (For an extreme case, consider V = ∅.) One natural thing to require is that all combinatorially possible truth-value assignments to the propositional variables are provided, i.e., that ∀X ⊆ ℕ ∃v ∈ V ∀k ∈ ℕ [v(pk) = T] iff k ∈ X. Note that this makes V uncountable. For most purposes, including the present one, a much weaker condition suffices, namely that V should be non-constant in the sense that V contains some valuation distinct from vT and vF.
19. The same phenomenon occurs with the proof system for the 1-ary ‘anticipation’ connective of Humberstone (2001), as was shown by Brian Weatherson (personal communication), whose proof is given in the as yet unpublished monograph mentioned in Section 5.
20. Of necessity, some examples in this paragraph have been mentioned without the explanation that would accompany them in a fuller treatment of this material. There is also a philosophical complication ignored in the use, above and below, of such phrases as ‘adherent of intuitionistic logic’, in that they seem at least to presume the incorrectness of a position that has been called logical pluralism and defended under that name in Beall and Restall (2006).
21. Cf. Koslow (1992), base of p. 129.
22. Requiring Δ = Θ = ∅ in (∨-E) blocks the proof of the quantum-logically contested distribution sequent p ∧ (q ∨ r) ≻ (p ∧ q) ∨ (p ∧ r).
23. Rules for multiplicative and additive conjunction are given in note 43. See Troelstra (1992) for further information about linear logic.
24. Actually a bit more is needed to obtain R, in that distribution of additive conjunction over additive disjunction is part of R which does not follow from the description given. Further details can be found in Avron (1988).
25. Here we see that the empty succedent is something of a luxury in intuitionistic logic, rather than a necessity, since we could always use F to fill it—or rather, ⊥, as one would say, since there are no F-vs.-f subtleties to worry about.
26. Actually, there is a complication (being ignored here) because of the contraction rule. One disadvantage of the set-based frameworks is that, loosely speaking, applications of this rule become invisible.
27. Notice that with “φ Tonk ψ” replaced by “φ, ψ” the inset sequents are available by (Id) and (Weakening) on the left and right. Since the comma here is not a connective, however, there is no formula—in the absence of Tonk—which could serve as a cut formula on the basis of these two sequent premisses. On one usage of the term ‘connective’, that associated with Belnap's Display Logic (see Restall (2000), Chapter 6) something corresponding to the comma and many more somewhat analogous devices are sometimes referred to as ‘structure connectives’ (as opposed to ‘formula connectives’). This whole topic lies outside of our purview.
28. This example appears in a slightly different form, but explicitly contrasted with that of Tonk in the same way, on p. 164 of Došen and Schroeder-Heister (1985).
29. This idea is essentially that of Setlur (1970), where a variation on the theme of Helena Rasiowa's, of taking hybrids in the framework Fmla—holding fixed the remaining connectives—is to be found. The device of taking direct products of matrix tables which works in Fmla does not fare so well in the richer frameworks; some remarks on the comparison with Set-Fmla in this respect can be found in Rautenberg (1985), pp. 7–9, and (1989), esp. p. 532. In an earlier publication, not listed in the bibliography, I used the term ‘products’ instead of ‘hybrids’ for the greatest lower bounds with respect to the subconnective relation, oblivious to the confusion this might engender. It did at least have one advantage, not shared by ‘hybrids’, of calling readily to mind a word—namely sums—for the corresponding least upper bounds, as illustrated by Tonk+ below (for ∧ and ∨).
30. The term harmony has been used mostly, and subject to various degrees of technicalization, for the relation of mutual appropriateness of elimination and introduction rules in natural deduction rather than, as here, to left and right rules in a sequent calculus. See Section 5 for references.
31. The idea that we could use a rule of ☐ introduction or insertion on the right with a proviso to the effect that formulas on the left be ‘fully modalized’, and use this in the reduplicated system to argue that since ☐φ ≻ φ is provable, the duplicated version of this rule allows the transition to ☐φ ≻ ☐′φ, on the grounds that the formula on the left is ‘fully modalized’, involves an illicitly equivocal use of the latter phrase. Something close to a model-theoretic version of this mistake would be involved in the suggestion that since S5 is determined by the class of models in which the accessibility relation is universal, and there is only one universal relation on any given set, ☐ is uniquely characterized by this logic. The mistake here is to think that because we can simplify the completeness result for S5 from equivalence-relational models to universal models, the same applies to the bimodal “reduplicated S5” logic that is at issue for the unique characterization claim. (“Something close”, because the syntactical argument would also apply in the case of S4 too, where nothing like the fallacy in this model-theoretic reasoning is likely to seem tempting.)
32. As with talk of the commutativity of conjunction, etc., what is meant is that the corresponding operation in the Lindenbaum algebra of formulas is a left inverse of that corresponding to ¬.
33. Substitution-invariance implies that the class of propositional variables is not special; the latter is equivalent to substitution-invariance given closure under uniform variable-for-variable substitutions, a weakening of substitution-invariance usually satisfied even by proposed logics not closed under arbitrary (uniform) substitution—in which case, accordingly, the propositional variables are special.
34. One could understand this in terms of the constancy of an associated truth function, but also purely syntactically: # is constant according to ⊢ if all formulas with # as main connective are ⟛-equivalent.
35. There is a natural notion of conservative extension which applies directly to (pairs of) consequence relations, but to avoid going into that here, we have adopted a formulation in terms of conservative extension as a relation between proof systems. Such a formulation would not be ideal here anyway because the fact that the initial consequence relation is ∨-classical does not imply that the extended consequence relation is, by contrast with the situation in Set-Set, since the conditional condition corresponding to (∨E) is not guaranteed to be preserved under extensions.
36. This is sometimes put by saying that ⊢ enjoys the Deduction Theorem, generalizing some terminology from a particular way of defining consequence relations on the basis of rules and axioms in logic treated by the axiomatic approach.
37. See Rousseau (1968).
38. A more detailed discussion of the notions in play here can be found in Humberstone (2005).
39. This example is discussed in §§3–4 of Humberstone (2000a).
40. This is because there is no 1-ary truth-function f with f(f(T)) = F and f(f(F)) = T.
41. As it happens, the (published) quantum-mechanically motivated work on √not antedates the philosophically motivated work by six years: see Deutsch (1989). Note that the phrase “the proposed connective” is used unapologetically here—as in the hybrids cases—in the absence of any suggestion that the conditions to which we have subjected it suffice for unique characterization.
42. See §§3 and 4 of Humberstone (2000c) for further discussion and references.
43. Contraction can be understood as the structural rule of that name in the multiset-based frameworks or, for the axiomatic approach in Fmla, as the schema (φ → (φ → ψ)) → (φ → ψ). The sequent calculus rules for (additive) ∧ are (∧ Left) as given in Section 2, with capital Greek letters reconstrued as multiset-variables, along with (∧ Right) taking us from Γ ≻ φ, Δ and Γ ≻ ψ, Δ to Γ ≻ φ ∧ ψ, Δ, while those for (multiplicative) ○ are as follows. The left insertion rule takes us from Γ, φ, ψ ≻ Δ to Γ, φ ○ ψ ≻ Δ, while the right insertion rule takes us from Γ ≻ φ, Δ and Γ′ ≻ ψ, Δ′ to Γ, Γ′ ≻ φ ○ ψ, Δ, Δ′. The Mset-Fmla0 rules suited to Intuitionistic Linear Logic are obtained from these Mset-Mset rules by the obvious restrictions on the right-hand sides.
44. In linear logic already we have t → T provable without its converse, for instance.
45. In a sequent calculus presentation one would instead add the inverted form, sometimes called Expansion, of the structural rule Contraction.
46. Theorem 5.8 in Blok and Pigozzi (1989) gives the desired ψ and χ for a given φ as φ ∧ (φ → φ) and φ → φ respectively. The proof on p. 49 of Blok and Pigozzi (1989) is seriously garbled, though the result is correct. Speaking of errors, let me mention that Dunn and Hardegree's attempt to explain what Blok and Pigozzi mean by “algebraizable”, at Definition 7.13.3 of Dunn and Hardegree (2001), rather misses the point, leaving out the requirement for two-way invertible translations between ⊢ and ⊨K, and ends up singling out the consequence relations which, in Blok and Pigozzi's terminology, “have an algebraic semantics” (the algebraizable ones being those having what Blok and Pigozzi call an equivalent algebraic semantics).
47. This perspective has been urged by many theorists with otherwise differing inclinations, including Michael Dummett, Dana Scott, and Roman Suszko. When dealing with a two-element matrix exactly one of which is designated, as in Rautenberg's maximality result in Section 2, the distinction between h and vh collapses.