(PDF) When Rules Define Logical Operators: Rules as Second-Order Definitions

When Rules Define Logical Operators: Rules as Second-Order Definitions Hannes Leitgeb Abstract Logical inferentialists hold that the meaning of logical operators is given by their rules of inference. Arthur Prior cast doubt on this by introducing rules for his tonk operator that would allow for the derivation of any sentence whatsoever from any sentence whatsoever. The obvious inferentialist reply was to require some constraints on the defining rules, such as conservativeness (Belnap) or harmony (Dummett). In this paper, I will defend and investigate a different constraint: rules define a classical logical operator just in case they translate into an explicit definition in pure classical second-order logic. The right-hand side of this criterion will be found (i) to be philosophically principled in taking the idea of rules as definitions perfectly seriously, (ii) to explain how the semantic meaning of the operators can be determined from their rules, (iii) to be local in a similar sense as harmony, (iv) to validate the intuitionistic natural deduction rules and the intuitionistic/classical sequent calculus rules as defining the classical propositional operators while ruling out Prior’s rules for tonk, (v) to make clear why already the intuitionistic natural deduction rules define the classical meaning of logical operators so long as metavariables are interpreted as expressing classical propositions, (vi) to validate the classical natural deduction rules as analytic, (vii) to entail consistency, and, in the case of propositional operators (not quantifiers), (viii) to be decidable and (ix) to determine precisely those operators to be definable by rules that correspond to truth-functions. Keywords: logical inferentialism, Prior, tonk, definitions, second-order logic. Acknowledgements: I am very grateful to Johan van Benthem, Denis Bonnay, Roy Cook, Matteo De Benedetto, Valentin Goranko, Norbert Gratzl, Volker 1 Halbach, Levin Hornischer, Luca Incurvati, Bruno Jacinto, Elio La Rosa, Graham Leigh, Benedikt Leitgeb, David Makinson, Julien Murzi, Sophie Nagler, Stephen Read, Greg Restall, Pablo Rivas Robledo, Marcus Rossberg, Lorenzo Rossi, Gil Sagi, Helmut Schwichtenberg, Neil Tennant, Brett Topey, Dag Westerståhl, Ed Zalta, and audiences at Munich, Paris, Salzburg, St Andrews, Turin, and the Nordic Online Logic seminar for comments on earlier versions of this paper. 1 Introduction: Logical Inferentialism Following a tradition going back at least to Gentzen (1934/1935) and Carnap (1934/1937)1 , logical inferentialists hold that the meaning of logical operators is given by their rules of inference.2 Prior (1960) cast doubt on this by introducing rules for his so-called tonk operator that would seem to allow for the derivation of any sentence whatsoever from any sentence whatsoever: (L tonk ) A tonk B ⊢ B (R tonk ) A ⊢ A tonk B For clearly, assuming Cut (Transitivity)3 , these rules yield: A ⊢ B.4 The obvious inferentialist reply was to require some constraints on the defining rules, such as: relative to a given derivability relation ⊢, rules accomplish to define a logical operator just in case they are conservative over ⊢, that is, when adding them does not extend ⊢ on the language without the operator. That was Belnap’s (1962) reply to tonk, which was further developed by Dummett (1991) later. However, e.g. the classical rules for negation in natural deduction are known not to be conservative over the ⊢ that is given by the rules for → on a language with → as sole operator. More1 Carnap (1937, §5): “In a strictly formally constructed system, the meaning of [. . .] symbols [. . .] arises out of the rules of transformation”. 2 Popper (1946–1947) is another early reference defending a similar view. For more on the closely related field of proof-theoretic semantics, see Prawitz (1965) and SchroederHeister (1991, 2024); see Murzi and Steinberger (2017) for a survey of inferentialism; and see Brandom (1994, 2000, 2018), Incurvati and Schlöder (2023), and Hlobil and Brandom (2024) for combinations of expressivism and inferentialism. 3 As shown by Cook (2005), the rules for tonk do not trivialize the derivability relation if transitivity is dropped. See Ripley (2015) for more on the role of structural rules in the tonk problem. 4 Popper (1946–1947, p. 284) also suggested a rule-based definition of a logical operator that would lead to inconsistency. 2 over, conservativeness is a global constraint that concerns the effect of adding rules to an inferential system as a whole: accordingly, rules may be conservative over one derivability relation while being non-conservative over another, and each of two rule extensions may be conservative separately while being non-conservative jointly (see e.g. Humberstone 2011, pp. 568f). To many inferentialists this suggested that conservativeness should count at best as a desideratum rather than as the solution to the tonk problem. That is one reason why the recent literature focused on more local constraints, such as a restriction to natural deduction rules in which the introduction and elimination rules of an operator are “harmonious” with each other (see Dummett 1991, Chapter 11). But the explication of harmony turned out itself to be riddled with difficulties.5 In what follows, I will propose a different criterion for when rules define logical operators that takes the standard theory of definitions (about which more in Section 2) as its starting point: according to that well-established theory, which rationally reconstructs mathematical practice, an explicit (normal form) definition of a function symbol is required to have a certain logical form and presumes a unique-existence assumption to be satisfied. The basic idea of the new inferentialist criterion will be to translate a logical operator into a propositional function symbol, to translate the rules for the operator into a statement that aims to define the corresponding function symbol in the language of pure classical second-order logic, and then to determine whether the rules define the operator by determining whether their corresponding second-order translation defines the corresponding function symbol: (Translation Criterion) Rules define a classical logical operator just in case they translate into an explicit definition of a propositional function symbol in pure classical second-order logic. In this way, the standard theory of definitions of function symbols by declarative statements will be extended to definitions of logical operators by systems of rules. The rationale behind the criterion is to take the inferentialist credo maximally seriously by regarding the rules by which a logical operator is introduced as aiming to constitute a definition. The standard theory of definitions can tell us which statements ought to count as definitions and thus 5 See Steinberger (2011) for a summary and analysis, and see Read (2000, 2010, 2015), Rumfitt (2017), and Jacinto and Read (2017) for recent explications and criticisms of harmony. 3 may serve as a yardstick, so long as one manages to translate rules into statements that the theory of definitions can potentially recognize as definitions. The paper will explain how the required translation is meant to proceed, why the resulting criterion is attractive, and which logical consequences it has. No new proof-theoretic results are going to emerge from this; in fact, some of the results of this paper will be folklore. Instead, the goal is really a philosophical-conceptual one: to explicate under which conditions a system of rules defines a logical operator, and to determine systematically, for simple but non-trivial rule systems, which of them end up defining logical operators. For instance, as will be explained in full detail in Section 3, assume the usual natural deduction rules for disjunction to be presented in a sequent . . . ⊢ . . . format: (∨Il ) Γ⊢A Γ⊢A∨B (∨Ir ) Γ⊢B Γ⊢A∨B (∨E) Γ⊢A∨B ∆, A ⊢ C ∆′ , B ⊢ C Γ, ∆, ∆′ ⊢ C In the course of translation, all metavariables (side formulas/context, active formulas, principal formulas) will be replaced by second-order set variables. Once the rules from before will have been translated into the language of pure second-order logic, the resulting statement will be: Def. 1 ∀A, B, X: Disn (A, B) = X ↔ (∨∗ Il ) ∀G: ∀w(G(w) → A(w)) → ∀w(G(w) → X(w)) ∧ (∨∗ Ir ) ∀G: ∀w(G(w) → B(w)) → ∀w(G(w) → X(w)) ∧ (∨∗ E) ∀G, D, D′ , C: ∀w(G(w) → X(w)) ∧ ∀w(D(w) ∧ A(w) → C(w)) ∧ ∀w(D′ (w) ∧ B(w) → C(w)) → ∀w(G(w) ∧ D(w) ∧ D′ (w) → C(w)). And the standard theory of definition will recognize that statement as an explicit definition of the second-order function symbol Disn (where the ‘n’ in ‘Disn ’ is for natural deduction). Hence, by the Translation Criterion, the original rules for ∨ constitute a definition. In contrast, when the same translation manual is applied to Prior’s rules for tonk (or similarly “badly” behaved rule systems, as will be the topic of Section 6), the resulting secondorder statement will turn out not to satisfy the requirements of the standard 4 theory of definitions. Therefore, the Translation Criterion will not accept Prior’s rules as defining tonk. The literature relating to this topic is vast and cannot be summarized properly here. It does not just concern the logical-inferentialist thesis itself (the thesis that rules determine the meaning of logical operators) but prooftheoretic semantics (semantics based completely on the notion of proof), logicality (what makes an operator logical), and categoricity (whether the rules for the usual logical operators determine their truth-conditional meaning uniquely). Garson (2013, p. 5) helpfully distinguishes between inferentialism proper and proof-theoretic semantics: (Inferentialism) The connectives obtain their meanings from the proof-theoretic roles that are established by the rules that govern them. (Proof-Theoretic Semantics) The meanings determined for the connectives must be characterized using only concepts found in proof-theory. In particular, notations like denotation and truth are not to be employed. And he adds, “(Proof-Theoretic Semantics) is not essential to inferentialism, despite its centrality in the historical tradition going back to intuitionism” (Garson 2013, p. 5). Accordingly, I should make clear from the start that the target of this paper is inferentialism, not proof-theoretic semantics, and I follow Garson in believing the former is not just by itself committed to the latter. So far as proof-theoretic semantics is concerned,6 its proponents are typically highly skeptical of truth-conditional semantics or even outright reject it. In contrast, I want to bracket general foundational questions about semantics as much as possible and just concentrate on the conditions under which systems of rules manage to define logical operators. This said, the most straightforward interpretation of the Translation Criterion from above is to understand the second-order reformulation of a rule system as making the truth-conditional meaning of a logical operator explicit and to take the rule system as determining that truth-conditional meaning. E.g., Def. 1 above, which results from translating the natural deduction rules for ∨ into the language of second-order logic, will be seen to capture the truth-conditional 6 For recent proof-theoretic approaches to definition by rules, see Schroeder-Heister (2007) and Tennant (2020). 5 meaning of disjunction. This interpretation of the Translation Criterion will then be congenial to a position that results from pairing inferentialism not with (Proof-Theoretic Semantics) from above but with what Garson (2013, p. 6) describes as follows: (Model-Theoretic Semantics) When characterizing the meaning of the connectives, it is of interest (and even helpful to those in the proof-theoretic tradition) to employ concepts from model theory such as truth, reference, and validity understood as preservation of truth. But perhaps even those who reject (Model-Theoretic Semantics) in favour of (Proof-Theoretic Semantics) might be able to embrace the Translation Criterion and the system of classical second-order logic it involves on merely instrumentalist grounds, reassured by the translation being purely syntactical, the defining rule systems for the classical operators being the intuitionistic ones (as will be shown in Sections 4 and 5), the verification of that fact only requiring the deductive system of second-order logic, and the Criterion being decidable in the case of propositional operators. And the explicit relativity of the Translation Criterion to the background framework of classical secondorder logic may turn into an asset when one realizes that the framework may be exchanged for a non-classical version thereof (as will be highlighted in Section 7). Indeed, proof-theoretic semanticists have famously made use of second-order intuitionistic logic when deriving e.g. the natural deduction rules for disjunction from those of implication (Prawitz 1965; see also Ferreira and Ferreira 2009, Tranchini et al. 2019). This said, it seems clear that for many proof-theoretic semanticists the Translation Criterion will be, at best, extensionally adequate. But already that would be valuable and certainly good enough for my own purposes.7 The relevant literature on logicality (see e.g. Van Benthem 2017 for a survey) proceeds from Tarski’s famous permutation criterion for logical concepts (further developed by Sher 1991), observes that the Tarski-Sher conception of logicality might overgenerate e.g. with respect to cardinality quantifiers, and therefore seeks to strengthen that conception by some inferentialist component (see e.g. Feferman 2015 and Bonnay and Speitel 2021). By way of contrast, it is not the aim of the present paper to explicate logicality, and the article will focus on rule systems for propositional operators, not quantifiers. In a nutshell: the target is not the non-logicality of the Härtig or 7 I am very grateful to Luca Incurvati and an anonymous reviewer for discussions of this point. 6 the Rescher quantifier but the non-definitional character of Prior’s rules for tonk. This said, assuming the standard interpretation of second-order logic, every concept defined in the language of second-order logic is known to be invariant under permutations of the underlying first-order domain. (See e.g. Van Benthem 1989.) Therefore, the second-order reformulation of any rule system that defines a logical operator according to the Translation Criterion will automatically also define a concept that is permutation-invariant. The categoricity properties of logical rules have experienced a general renewal of interest in recent years, triggered by discussions of some of Carnap’s considerations on categoricity (see Raatikainen 2008, Murzi and Hjortland 2009, Bonnay and Westerståhl 2016, Murzi and Topey 2021). In the present paper, the categoricity of rule systems will only be relevant as a by-product of a rule system successfully defining a logical operator.8 While the present approach has nothing to say about proof-theoretic explications of uniqueness (see Zucker and Tragesser 1978, Harris 1982 on that topic), we will get the kind of uniqueness that is already built into the traditional theory of definitions of function symbols: e.g., Def. 1 from above determines Disn uniquely, and Disn (A, B), the proposition expressed by a disjunction, will be a function of A and B, the propositions expressed by the disjuncts, and will be determined from them uniquely. So far as the existing literature is concerned, Garson (2013) is the most comprehensive study of how rules determine the meaning of logical operators. When setting up the translation of rules into the language of second-order logic, I will follow Garson in interpreting rules as globally valid (see Garson 2013, pp. 15–16), that is, as preserving sequent validity. E.g.: (∨Il ) Γ⊢A Γ⊢A∨B translates into (suppressing second-order quantifiers, see Def. 1 above) (∨∗ Il ) ∀w(G(w) → A(w)) → ∀w(G(w) → X(w)) which might be read as: if every w that satisfies Γ/G also satisfies A, then every w that satisfies Γ/G will also satisfy A ∨ B/X.9 Just like Gar8 Uniqueness, that is, the requirement that the meaning of an operator is to be determined uniquely by its defining rules, was also listed as a desideratum by Belnap, although he regarded it as “not as essential” (Belnap 1962, p. 133) as conservativeness. 9 In second-order logic, (∨∗ Il ) prefixed by ∀G is of course immediately logically equivalent to ∀w(A(w) → X(w)). 7 son (2013, Section 1.8), I take this to be the correct semantic reading of (rules involving) the turnstile.10 But Garson does not translate rules into statements in order to determine whether the latter constitute explicit definitions. And our classical second-order framework will be more restrictive than Garson’s model-theoretic framework (which involves canonical models and Kripke models), which is why even the natural deduction rules for ∨ or → will define the respective classical operators (different from Garson 2013, p. 54). The other parts of the literature that come close to the account to be developed are Koslow (1992), McGee (2015) (who builds on Koslow), and Feferman (2015): Koslow does not consider rules for logical operators in formal languages but defines logical operators by characterizing them relative to abstract implication structures that consist of an arbitrary set and an implication relation on that set. But the characterization is still structurally in line with rules of inference. McGee takes over that structural perspective but pins down the members of implication structures to be propositions in the sense of sets of possible worlds that can be expressed by open-ended schematic letters. Later I will adopt McGee’s understanding of metavariables as being capable of expressing arbitrary propositions in the sense of intensional semantics. And I will invoke McGee’s idea of using rules of inference to determine functions on propositions in that sense. The main differences will be: where Koslow and McGee leave the underlying framework informal, I will make it precise in the form of second-order logic.11 Feferman (2015) does the same,12 considers a general translation manual by which rules can be translated into second-order statements, and applies the manual in order 10 See, e.g., Murzi and Topey (2021, Section 2.2) for a different semantic understanding of rules as merely locally valid, that is, as preserving sequent satisfaction. E.g., they would understand (∨Il ) as: for every w, if w satisfies Γ ⊢ A, then w also satisfies Γ ⊢ A ∨ B, where w satisfies a sequent just in case it satisfies the corresponding material conditional. However, in my view, a sequent should not express semantically what its corresponding material conditional does. Instead, Γ ⊢ A should rather express strict truth preservation: in all possible cases w, if all members of Γ are satisfied, then also A is satisfied. 11 If it was not for the possibility to formulate definitions and to be able to extend the account to rules for quantifiers, much simpler formalizations than second-order logic could have been chosen, such as propositional logic or logic programming. The approach of the present paper, like Koslow’s, McGee’s, and Feferman’s, also has an affinity to algebraic logic, such as logic in cylindric algebras (Henkin et al. 1981). 12 Historically, Russell (1903) might have been the first to translate rules into the language of higher-order logic. I am grateful to Elio La Rosa for reminding me of this. 8 to determine a plausible necessary condition for the logicality of quantifiers. (Feferman does not defend logical inferentialism. See Bonnay and Speitel 2021 for a criticism and further development of Feferman’s theory.) The difference is that Feferman only considers whether these second-order translations define quantifiers implicitly in the relevant models, while my focus will be on whether they conform to the logical form and properties of explicit definitions in normal form. This is important: e.g., consider the higher-order statement ∀A, X: Op(A) = X ↔ ∀w ¬Op(A)(w) which constrains Op to be the function that maps each proposition A to the contradictory proposition (the empty set of worlds). While the statement thus manages to define that function implicitly, it would clearly not be acceptable as an explicit definition of Op in view of the circular appearance of Op both in the definiendum and the definiens. As will be seen later, it is a crucial aspect of the approach of the present paper that it may drive a wedge between rules systems that, model-theoretically, define the same function implicitly: for one of them might translate into an explicit definition whilst the other one does not. And in my view this is exactly as it should be: systems of rules—just like ordinary explicit definitions—are syntactic constructions, and when they count as definitions, this is at least partly so in virtue of their syntactic form.13 Finally, none of Koslow, McGee, or Feferman distinguishes between definitional and merely analytic rule systems, as I will do later (in Section 4). This said, the present paper can and should be viewed as further developing some of the thoughts originating from Garson (2013), Koslow (1992), McGee (2015), and Feferman (2015). This is the plan for the remainder of the paper: Section 2 describes the languages we are dealing with and recalls the standard theory of definitions of function symbols. Section 3 details the Criterion in the case of ∨, whereas Section 4 presents it for propositional rule systems in general. Along the way, 13 In the previous example, the implicit definition of Op could of course easily be turned into an equivalent explicit definition that would still belong to the language of secondorder logic: ∀A, X: Op(A) = X ↔ ∀w ¬X(A)(w). However, the standard general method by which a finite implicit definition of a function on propositions (second-order entities) is converted into an equivalent explicit definition would involve quantification over such functions and would thus become a third -order definition in the language of third -order logic. In contrast, the paper will only deal with explicit definitions that are second-order. See the end of Section 2 and Section 8 for more on this. 9 Section 3 will also explain how the required translation determines the semantic meaning of operators from their rules; and Section 4 will demonstrate the locality of the Criterion and its decidability for propositional rule systems, it will show that precisely those operators are defined by propositional rule system that—in a sense explained by their second-order translations— express truth functions, and it will define analyticity for rule systems. The main outcomes for the standard classical logical operators are summarized at the end of Section 4. Section 5 demonstrates that already the intuitionistic natural deduction rules for →, ⊥, ¬ define the respective classical operators and explains why a classically deductively incomplete rule system may still successfully define a classical operator. The section will also prove the classical rules for ⊥ and ¬ to be analytic but not definitional. Section 6 clarifies what kind of conservativeness the Criterion supports and shows that the rules for tonk are not definitional or analytic. Section 7 sums up, makes clear how the second-order translations of logical rules may be viewed as uncovering the tacit commitments of classical inferentialism about these rules, proposes extensions (e.g. to quantifiers), and suggests that if the Translation Criterion is changed by translating rules into definitions in non-classical second-order logic, analogous results might be achieved for non-classical logical operators. A brief appendix (Section 8) explains how classical rule systems could also be translated into third-order definitions but why this would come with theoretical costs if compared to second-order definitions. 2 Preliminaries As explained in the introduction, the aim is to develop a criterion for whether a system of rules manages to define a logical operator. According to the criterion to be developed, this will involve translating such a system into a second-order statement. In order to make this more precise, we will need to distinguish two kinds of languages: (a) the language(s) in which the supposedly meaning-constitutive rules for a supposedly logical operator are formulated; and (b) the language in which these rules will be recast as a candidate for an explicit definition of the meaning of that operator. I will restrict (a) to: 10 (Ad a) languages that are built solely from finitely many metavariables/schematic letters for formulas, finitely many metavariables/schematic letters for sequences of formulas, commas, the turnstile symbol ⊢, and finitely many propositional connectives, where the propositional connectives in question are to be defined by finite systems of finitary rules that are formulated in these languages with the help of the turnstile. For propositional rules of that sort, the new Translation Criterion will be stated completely and suggested to be necessary and sufficient for defining a logical operator. I will not deal with quantifiers; and infinitary rules and infinite systems of finitary rules will be disregarded, too. The criterion for whether the rules formulated in the languages in (a) amount to a definition will be explicated with the help of the language in (b), which will be (with the only exception of Section 8): (Ad b) the pure language of classical second-order logic that is based solely on firstorder variables (w, x, y, z,. . .), second-order variables (X,. . .), the usual logical operators (¬, ∧, ∨, →, ↔, ∀, ∃), auxiliary expressions, and terms explicitly defined from these primitive terms. The plan will be to translate a rule system formulated in (a) into a secondorder statement in (b), to check whether the resulting statement is an explicit definition in the ordinary sense of the term, to regard the original rule system as definitional just in case the check is positive, and to verify positive checks by proofs in the deductive system of second-order logic. The context will always clarify which language is used: when stating rules, it will be the language(s) in (a), and when stating definitions or theorems, it will be the language in (b). The translation manual itself, which will be uniform across all rule systems, will be explained with the help of natural language terms. Some extensions and variations of the languages in (a) and (b) will be discussed in Sections 7–8. What motivates choosing the pure language of second-order logic as the background language is that it allows for the formulation of explicit definitions, it makes (in future extensions of the approach) the translation of rules for quantifiers possible, and it is logical (Quinean worries notwithstanding), which is going to ensure that what will be determined is whether a logical operator is defined by rules. The idea of exploiting the expressive power of a second-order language to throw light on the meaning of first-order expressions is not new, of course: e.g., one may regard the first-order scheme of axioms/rules for induction over natural numbers as a first-order approximation of the second-order Axiom 11 of Induction, and when a predicate is defined inductively by a finite system of first-order axioms or rules, the inductive definition can be turned into an explicit second-order definition of the same predicate. In a similar manner, I will regard the rules of inference for a logical operator in a first-order language, such as the rules for disjunction or tonk, as aiming to approximate an explicit second-order definition, which may succeed or fail. Applications of the resulting Translation Criterion will not exploit the second-order resources in (b) to formulate second-order definitions of True(x) or Defines(x, y) or of any other semantic notion for our given first-order language(s) in (a). However, I will often use classical-semantic considerations to motivate and justify the Criterion and its consequences. Furthermore, proofs in (b) by which certain rule system will be shown to define logical operators will not require the system of full second-order logic that is defined model-theoretically by quantification over all full/standard secondorder models (see Shapiro 1991, p. 72) but just the recursively axiomatizable deductive system of second-order logic that is sound and complete with respect to the larger class of all Henkin models that satisfy Comprehension (see Van Dalen 2013, Chapter 5). In particular, in the rest of the paper, I will make use of suitable instances of the second-order Axiom Scheme of Comprehension that is included in the deductive system. In addition, I will presuppose an identity predicate for second-order entities that satisfies the Axiom of Extensionality: e.g., for unary second-order variables X and Y we will have ∀X, Y : X = Y ↔ ∀w(X(w) ↔ Y (w)). The intended interpretation of second-order variables is thus as ranging over extensional properties, relations, and functions: sets of individuals, set-theoretic relations of individuals, and set-theoretic functions on individuals.14 14 Should one worry about the potential circularity of using second-order logic to characterize the rule systems that define logical operators, when second-order logic itself comes with rules for its logical operators? I do not think so, for similar reasons for which it is unproblematic to use metalinguistic rules for disjunction to prove the correctness of first-order rules for disjunction in the course of the soundness proof for first-order logic, or to employ a metalinguistic disjunction symbol when stating the truth conditions for object-linguistic disjunctions while formulating a Tarskian truth definition. (Compare the corresponding defence against the circularity objection in Tarski’s 1944, Section 15.) The deductive system of second-order logic functions as a tool for rational reconstruction much in the same sense in which, e.g., Tarski used second-order logic to define truth for first-order languages. Indeed, every rational reconstruction must presuppose some means of reconstruction, and presupposing the basic resources of the deductive system of pure second-order logic hardly seems extravagant. Moreover, the translation between rule sys- 12 When I will speak of definitions in the following, I will always mean explicit definitions or definitions in normal form in the usual sense of the traditional theory of definitions (see e.g. Suppes 1957, Chapter 8), not any kind of implicit definitions in the sense of axiomatic characterizations (even when they would support eliminability and non-creativity). In particular, as will be the focus in the subsequent sections, a second-order definition of an n-ary function constant F that denotes a function mapping n sets to a set is understood to be a second-order formula Second-Order Def. of F : ∀A1 , . . . , An , X: F (A1 , . . . , An ) = X ↔ S[A1 , . . . , An , X] in which (1) A1 , . . . , An , X are n + 1 pairwise distinct unary set variables, (2) the variables free in S[A1 , . . . , An , X] are included in A1 , . . . , An , X, (3) S[A1 , . . . , An , X] is a second-order formula in which the only non-logical constants are previously defined symbols, and (4) where the universally quantified unique-existence (UE ) formula for F , U EF : ∀A1 , . . . , An ∃!XS[A1 , . . . , An , X], is derivable in the deductive system of pure second-order logic (perhaps extended by previous definitions). While (1)–(3) are purely syntactic requirements for definitions, (4) is a syntactic-deductive requirement. The definition of function symbols is traditionally relativized to background theories from which the required universally quantified unique-existence formulas must be derivable, and in our case that background theory will be the deductive system of second-order logic (and prior definitions). The second-order definition of a unary second-order constant C (denoting a set) proceeds accordingly, the only difference being that A1 , . . . , An drop out, so that the definition is of the form ∀X: C = X ↔ S[X] and U EC reduces to a mere unique-existence claim of the form ∃!XS[X]. Definitions like these, or rather their right-hand sides, are known to not only satisfy suitably formulated criteria of eliminability15 and non-creativity/conservativeness (see Gupta 2021) but also to conform to mathematical tems and the language of pure second-order logic will not in any way presuppose that, e.g., the meaning of ∨ in a rule system relates to that of ∨ in the language of second-order logic. Rather, the meaning Dis(A, B) of A ∨ B as given by the natural deduction rules for ∨ will emerge from applying a perfectly general translation manual to the rules for ∨—the same manual that will apply to propositional rule systems in general. 15 E.g., it follows from the previous definition of F , Extensionality, and U EF that a predication of the form F (A1 , . . . , An )(w) can be reformulated equivalently as the following second-order statement without F : ∃!X(S[A1 , . . . , An , X] ∧ X(w)). 13 practice. E.g., in set theory, the standard characterization of the union ∪A of (the members of) a set A only becomes acceptable as a definition once the universally quantified unique-existence claim ∀A∃!X∀x(x ∈ X ↔ ∃y(y ∈ A ∧ x ∈ y)) has been derived from the Union Axiom (see Bell and Machover 1997, p. 466; see also Hilbert and Bernays 1968, p. 393). Note that although the defined function constant F above is itself thirdorder, no third-order quantification is involved in its second-order definition, and F (A1 , . . . , An ) is a second -order function term (just as e.g. f (x, y) would be a first-order function term that might figure in the definiendum of a definition of f in a first-order language). If read with the help of a definite description operator, the definition above says that, for all A1 , . . . , An , the set F (A1 , . . . , An ) is defined to be the uniquely determined set X, such that S[A1 , . . . , An , X]. And using Extensionality, the equality F (A1 , . . . , An ) = X may be unpacked as ∀w(F (A1 , . . . , An )(w) ↔ X(w)) with a first-order w. Such a second-order definition of F should therefore not be mixed up with a third-order definition of F , which would be of the form Third-Order Def. of F : ∀X : F = X ↔ S[X ] in which F would be a third-order function constant denoting a function on sets, X a third-order function variable ranging over functions on sets, and U EF3 : ∃!X S[X ] would a third-order unique-existence formula. If read again with the help of a definite description operator, such a third-order definition would say that F is defined to be the uniquely determined function X on sets, such that S[X ]. The aim of the paper is not to translate rules of inference into such third-order definitions but rather into second-order definitions of the form discussed before. It is only in the appendix that I will consider third-order definitions in order to discuss how they differ from second-order definitions. Finally: when I will turn to the rules for the standard logical operators, I will only aim at defining the logical operators of classical logic, and I will take a thoroughly classical-semantical point of view on what it would mean to pin down their meanings by definition (variations being considered in Section 7). But I will discuss minimal, intuitionistic, and classical natural deduction and sequent calculus rules, for which I will use their formulations in Troelstra and Schwichtenberg (2000) (though in the case of negation I will also use some other references). I will not consider Hilbert-style rule systems for the usual 14 logical operators at all, as logical inferentialists normally do not regard them to be definitional. 3 From Rules to Second-Order Definitions: Disjunction as Initial Example Before turning to rule systems in general in Section 4, let me start by explaining the manual for translating rule systems into second-order statements by means of a concrete example: the translation of the standard natural deduction rules and the sequent calculus rules for disjunction, which are the same in minimal, intuitionistic, and classical logic. (Conjunction works analogously but is less interesting, as its rules are simpler than those for ∨.) Here and in what follows, I will state all rules in a sequent . . . ⊢ . . . format where the antecedent and consequent are formulas built from metavariables or sequences of such formulas, as this will facilitate the formulation of the translation manual. In that format, natural deduction rules will be characterized by every sequent having a unique consequent, and by introduction and elimination rules affecting the occurrence of the relevant operator in the consequent of sequents. Sequent calculus rules may have more than one formula to the right of the turnstile, and they introduce the operator in question either to the left of the turnstile or to the right of it. First, let us consider the natural deduction rules for ∨: (∨Il ) A A∨B (∨Ir ) B A∨B (∨E) A∨B [A]u .. . [B]v .. . C C C Or in sequent format again: (∨Il ) Γ⊢A Γ⊢A∨B (∨Ir ) Γ⊢B Γ⊢A∨B (∨E) Γ⊢A∨B ∆, A ⊢ C ∆′ , B ⊢ C Γ, ∆, ∆′ ⊢ C Let us call this rule system: R∨ . Its rules are to be understood in the way that its metavariables range over arbitrary (sequences of) formulas of whatever object language is used. In addition, I will always presuppose the premise-free “Axiom” of Reflexivity (all instances of . . . ⊢ . . . with the same expression to the left and to the right of the turnstile) and the usual 15 structural Gentzen rules for systems in sequent notation, that is, Permutation, Weakening, Contraction, and Cut (Transitivity).16 However, I will not bother translating Reflexivity or the structural rules below, as their secondorder translations would turn out to be logical truths and thus would not add anything substantial to the definitions to be generated.17 Although the translation of R∨ will be a purely syntactical procedure, it will be useful to keep the following semantic picture in mind (whether taken at face value or as a merely instrumental guide): just as a disjunction formula A∨B results from applying ∨ to the formulas A and B, I intend to determine the meaning of A ∨ B functionally from the meanings of A and B; and I want to do so in line with the inference rules above. Taking a classical point of view and following standard intensional semantics, let us think of the meaning of a sentence as a set of possible worlds. So I will presuppose from the start that meanings are (extensionalised) truth conditions, but without making any assumptions which of these meanings is to be expressed by A ∨ B. We can use our second-order language to refer to such sets of possible worlds as follows: re-interpret the metavariables A and B in the rules above as unary second-order variables for extensional properties or sets; and assume the underlying first-order domain to be the relevant space of possible worlds. In this way, A and B may be taken to stand for arbitrary sets of possible worlds—arbitrary propositions—and A(w) expresses that w ∈ A or that the proposition A is true in the possible world w. No assumptions concerning the “nature” of possible worlds are required.18 Thus, in the case of disjunction, when A and B are arbitrary propositions, Dis(A, B) will be defined to be another proposition that will be true in a world w just in case Dis(A, B)(w). Since the formulas A and B in the rules above may be open formulas, it 16 These structural rules were also taken for granted by Belnap (1962). One of the open questions at the end of the paper will thus be how the present approach could be generalized to substructural rule systems. See Ripley (2015) for more on structural rules and tonk. 18 An alternative would be to re-interpret A and B as propositional variables, that is, 0-ary second-order relation variables for propositions (as in, e.g., Zalta 2020). But the language of second-order logic is not always assumed to include such expressions: e.g., Shapiro (1991) omits them completely, and Van Dalen (2013), Feferman (2015), and Väänänen (2021) regard propositional variables as denoting truth-values. By conceiving of propositions as extensional properties of possible worlds, and by expressing these extensional properties by unary set variables, we can stick to standard second-order logic without further ado. 17 16 would also be natural to re-interpret A and B as second-order relation variables with arities greater than 1. But doing so will not be necessary so far as our Translation Criterion for rules for propositional operators, such as ∨, are concerned, as all relevant results can be shown already for propositions (sets) A and B. However, there would be analogous versions of these results in which e.g. the proposition A (in set notation, {w: A(w)}) would be replaced by a relation or propositional function A(x) (= {w: A(w, x)}). And the usage of relation variables would become strictly mandatory if and when the translation account got extended to quantifiers. A disadvantage of my approach will be that the types of Dis and Dis(A, B) will always vary with the types of A and B varying, which could be avoided by determining the truth values A(w, x) and B(w, x) first and only then applying the truth function Dis to them (as in: Dis(A(w, x), B(w, x))). The advantage will be that, when one understands a disjunction A ∨ B, the determination of its content from the contents expressed by its disjuncts seems prior to determining truth values relative to worlds and sequences of objects.19 In order to translate the ⊢ rules above into what will become a secondorder definition ultimately, we will not consider which sequents are provable from them but rather translate each rule into a statement that expresses that if the premises of the rule are strictly truth-preserving inferences, then so is its conclusion inference. This is achieved by appying the following steps to 19 I am grateful to Volker Halbach for a discussion of this matter. 17 all occurrences of the relevant syntactic expressions in the rules above: T1 Replace A ∨ B by the atomic formula X(w) with the unary set variable X and the first-order variable w. T2 Replace the remaining metavariables for formulas, A, B, C, by respective atomic formulas A(w), B(w), C(w) with unary set variables (we use A, B, C again) and the first-order variable w. Occurrences of pairwise identical/distinct metavariables are thereby replaced by occurrences of pairwise identical/distinct set variables. T3 Replace metavariables for sequences of formulas, Γ, ∆, ∆′ , by respective atomic formulas G(w), D(w), D′ (w) with unary set variables G, D, D′ and the first-order variable w. Once again, occurrences of pairwise identical/distinct metavariables are replaced by occurrences of pairwise identical/distinct set variables. T4 Replace ⊢ by the implication operator →. One remark on T3 (and similarly T8 below): in the present case of a classical or intuitionistic rule for a propositional operator, it turns out to be sufficient to translate a metavariable for a sequence of formulas by a single atomic formula with a unary set variable. In other contexts, a more complex treatment of metavariables for formula sequences may be necessary.20 20 I am grateful to an anonymous reviewer for highlighting that. 18 The procedure so far leads to the following output: G(w) → B(w) G(w) → X(w) G(w) → A(w) G(w) → X(w) G(w) → X(w) D(w), A(w) → C(w) D′ (w), B(w) → C(w) G(w), D(w), D′ (w) → C(w) The next translations steps are: T5 Replace commas in antecedents of implications by conjunction symbols. T6 Universally quantify the resulting replacement of each sequent by the first-order quantifier expression ∀w. Which leaves us with: ∀w(G(w) → A(w)) ∀w(G(w) → X(w)) ∀w(G(w) → B(w)) ∀w(G(w) → X(w)) ∀w(G(w) → X(w)) ∀w(D(w) ∧ A(w) → C(w)) ∀w(D′ (w) ∧ B(w) → C(w)) ∀w(G(w) ∧ D(w) ∧ D′ (w) → C(w)) Continue by: 19 T7 Join the resulting replacements of premises in each rule by conjunction (here this is just relevant for the third rule). Replace the horizontal line in the resulting replacement of each rule by the implication →. T8 Universally quantify the resulting replacement of each rule by universal secondorder quantifier expressions for the replacements of metavariables for sequences in that rule (∀G, ∀D, ∀D′ ) and by universal second-order quantifier expressions for the replacements of all metavariables for formulas in that rule other than A and B (here this is just ∀C). T9 Join the resulting replacements of the rules by conjunction. This generates a conjunction starting with ∀G: ∀w(G(w) → A(w)) → ∀w(G(w) → X(w)) ∧ ∀G: . . . Finally: T10 Use the resulting replacement of the rule system for ∨ as the definiens of a definition that starts with universal second-order quantifier expressions of the form ∀A, B, X, followed by the definiendum Disn (A, B) = X where Disn is a function constant and the index ‘n’ signals that the translation has been carried out for the natural deduction rules, and add the equivalence ↔ and the definiens that was constructed by T1–T9 on the right. Let us call the translation of R∨ by T1–T10: T [R∨ ]. T [R∨ ] is our intended second-order definition of Disn : Def. 1 ∀A, B, X: Disn (A, B) = X ↔ (∨∗ Il ) ∀G: ∀w(G(w) → A(w)) → ∀w(G(w) → X(w)) ∧ (∨∗ Ir ) ∀G: ∀w(G(w) → B(w)) → ∀w(G(w) → X(w)) ∧ (∨∗ E) ∀G, D, D′ , C: ∀w(G(w) → X(w)) ∧ ∀w(D(w) ∧ A(w) → C(w)) ∧ ∀w(D′ (w) ∧ B(w) → C(w)) → ∀w(G(w) ∧ D(w) ∧ D′ (w) → C(w)). 20 As we shall see shortly, this is a definition in the sense explained in the last section, as the universally quantified unique-existence claim for (the definiens of) Disn , U EDisn : ∀A, B ∃!X (∀G: ∀w(G(w) → A(w)) → . . . ∧ D′ (w) → C(w))), is provable in the deductive system of second-order logic (and hence logically true in second-order logic). But first let us be clear why this definition tracks the original rules for ∨: the reason is simply that its definiens gets the inferential role of ∨ as determined by these rules right. For example: just as the given left-introduction rule (∨Il ) allows one to turn an inference from Γ to A into one from Γ to A ∨ B (thereby introducing disjunction), the corresponding clause (∨∗ Il ) in the definiens expresses in second-order terms that if there is a strictly truthpreserving transition from an arbitrary G to A, then there is also one from the same G to the very X that is to be determined by the definiens. The same holds for the other two rules of inference and their corresponding parts of the definiens. Of course, if things go well, X should be nothing but the proposition expressed by A∨B ultimately. So the definiens of Definition 1 is just the immediate second-order reformulation of the original rule system except that X takes the place of A ∨ B, metavariables for arbitrary (sequences of) formulas are interpreted as expressing arbitrary propositions, with propositions being understood as in classical intensional semantics21 , and the turnstile is interpreted as strict truth-preservation. Other than through its consequences and applications, to which I will turn in the remaining sections, the Translation Criterion I am going to formulate now should be intrinsically plausible in light of this structural similarity between a rule system and its secondorder translation: a rule system should count as definitional just in case its second-order translation yields a definition in normal form. In the present case, our criterion for whether a system of rules defines a logical operator amounts to:22 Metadef. 2 (Translation Criterion for ∨ in Natural Deduction) The rule system R∨ of the natural deduction rules for ∨ defines ∨ just in case T1–T10 translate the system into a definition T [R∨ ] of the corresponding function 21 As mentioned in Section 1, I am building on McGee (2015) here. In what follows, when I refer to definitions of function symbols in the language of second-order logic, I will simply speak of definitions. When I refer to definitions belonging to the metalanguage (in which I talk about the language of rule systems and the language of second-order logic), I will introduce them by the term metadefinitions. 22 21 constant Disn in the language of pure classical second-order logic. If so, call the rule system R∨ definitional. Since all the purely syntactic requirements for a definition are clearly met by the second-order translation from before, it remains to be shown that the deductive requirement is satisfied, too, that is, here: U EDisn is provable in the deductive system of second-order logic. For then the natural deduction rules for ∨ will have passed the test. Indeed, the natural deduction rules for ∨ do define ∨. (I will merely sketch the argument and use set-theoretic notation.) Given arbitrary A and B, the existence of the required X follows from the instance of Comprehension that postulates the (with Extensionality, unique) existence of the disjunction proposition A ∪ B of propositions A and B, ∀A, B ∃X∀w(X(w) ↔ A(w) ∨ B(w)), as the deductive system of second-order logic proves of that X (= A ∪ B) that it satisfies (∨∗ Il ), (∨∗ Ir ), (∨∗ E). Uniqueness follows from Comprehension for A, B, A ∪ B, {w | w = w}: for consider an arbitrary X that satisfies (∨∗ Il ), (∨∗ Ir ), (∨∗ E). With G = A it follows from (∨∗ Il ) and second-order logic that A ⊆ X, and with G = B it follows from (∨∗ Ir ) and second-order logic that B ⊆ X; hence, by secondorder logic, A ∪ B ⊆ X. Furthermore, for G = X, D = D′ = {w | w = w}, and C = A ∪ B, it follows from (∨∗ E) that, since A ⊆ A ∪ B and B ⊆ A ∪ B by second-order logic, it holds that X ⊆ A ∪ B. Combining Extensionality with what has been shown yields that X = A ∪ B. So U EDisn can be proven on purely logical grounds, which is why the natural deduction rules for disjunction define disjunction according to our Criterion. And since U EDisn is provable by logic alone, Def. 1 constitutes a definition of a function symbol that combines successfully with every theory whatsoever and can be interpreted in every second-order model with whatever underlying domain of “worlds”. In fact, as we shall see in the next section, there is even a computational method by which it can be decided in general whether a simple propositional rule system such as the one for ∨ defines an operator. But in the present positive case (and in the positive cases to be considered later) the proofs of the required unique-existence claims can be found easily without exploiting a general decision method. It should be noted that in order for U EDisn to be provable, the presence of both (the translations of) introduction and elimination rules is crucial. 22 E.g., if the elimination rule had been dropped, the translation of the rule system consisting just of the two introduction rules for ∨ would have led to a second-order statement that would not be a definition, as there would be more than one X that would satisfy the resulting definiens: next to X = A ∪ B, choosing X = {w: w = w} would be another option. Therefore, in the present account, the introduction rules for an operator should not by themselves be regarded as definitional, which contrasts with the prooftheoretic tradition originating from Gentzen in which the introduction rules alone are taken to define operators (see Gentzen 1935, p. 189). Other than playing its role in the Translation Criterion, the translation manual T1–T10 is also important for another reason: it determines the standard semantic meaning of ∨. For we have just shown that Def. 1 entails that Disj(A, B) = X = A ∪ B: hence, the proposition X that is expressed by the disjunction formula A ∨ B as determined by the natural deduction rules for disjunction is just the union A ∪ B of the propositions expressed by the two disjuncts. Or equivalently, for all w: X is true in w iff A is true in w or B is true in w. And since the translation is perfectly general, the same may be expected of its application to other natural deduction rules systems for other logical operators—an expectation to be confirmed in the subsequent sections. That is remarkable in so far as the best worked out methods of determining the truth-conditional meanings of logical operators from their rules only work well for sequent calculus rules but happen to be formally or philosophically problematic for certain natural deduction rule systems, including those for disjunction (compare Garson 2013, p. 6 and pp. 20f). Before we turn to other logical operators, let us apply our translation method also to the sequent calculus rules for disjunction: (L∨) A, Γ ⊢ ∆ B, Γ ⊢ ∆ A ∨ B, Γ ⊢ ∆ (R1∨) Γ ⊢ ∆, A Γ ⊢ ∆, A ∨ B (R2∨) Γ ⊢ ∆, B Γ ⊢ ∆, A ∨ B The translation manual will remain the same, except that T5 from before needs to be augmented by a translation rule for commas on the right-hand side of the turnstile, as the sequent calculus allows for sequents with multiple 23 conclusions: T5 (Extended Version) Replace commas in antecedents of implications by conjunction symbols and in consequents of implications by disjunction symbols. Applying the so extended translation manual T1–T10 to the sequent calculus rules for ∨ leads to the following second-order statement: Def. 3 ∀A, B, X: Diss (A, B) = X ↔ (L∨∗ ) ∀G, D: ∀w(A(w)∧G(w) → D(w))∧∀w(B(w)∧G(w) → D(w)) → ∀w(X(w)∧ G(w) → D(w)), (R1∨∗ ) ∀G, D: ∀w(G(w) → D(w) ∨ A(w)) → ∀w(G(w) → D(w) ∨ X(w)), (R2∨∗ ) ∀G, D: ∀w(G(w) → D(w) ∨ B(w)) → ∀w(G(w) → D(w) ∨ X(w)). Since the syntactic restrictions are satisfied again and the required universally quantified unique-existence claim is provable in the deductive system of second-order logic by a similar argument as before, this second-order statement follows to be a definition of Diss (where the subindex is for ‘sequent calculus’ now). Which means, according to the analogous sequent calculus version of our Criterion: the sequent calculus rules for ∨ define ∨, too. Indeed, second-order logic derives the equivalence of the two definitions, ∀A, B, w: Disn (A, B)(w) ↔ Diss (A, B)(w), or with Extensionality, ∀A, B: Disn (A, B) = Diss (A, B). If we want, we may therefore simply write: Dis(A, B). 4 From Rules to Second-Order Definitions: The General Propositional Case Now I will explain how the translation method from the previous section can be applied to rule systems in a much more general sense. In order to do so, I need to specify first what these systems are like. 24 Consider m propositional operators o1 , . . . , om , each oi having a finite arity ji ≥ 0 (when ji = 0, oi is a propositional constant). The operators are propositional in the sense that their application to formulas yields formulas again, and, unlike quantifier expressions, they are not binding variables. Accordingly, we will not need to go beyond unary set variables when specifying their inferential roles in second-order terms later. A rather general notion of propositional rule system is given by: Metadef. 4 A propositional rule system R for the sequence o1 , . . . , om of propositional operators is a sequence of the following components: • A specification of whether multiple conclusions are syntactically permissible in a sequent (as in the sequent calculus) or not (as in natural deduction). • Reflexivity and the usual structural rules of Permutation, Weakening, Contraction, and Cut (suitably adapted to the chosen specification). • For each i with 1 ≤ i ≤ m, a sequence of ki -many rules for oi , R1i , . . . Rki i , where for all l with 1 ≤ l ≤ ki , Rli is an expression of the form (oi Rli ) i,l i,l Φi,l . . . Φi,l nl ⊢ Ψnl 1 ⊢ Ψ1 i,l Φi,l nl +1 ⊢ Ψnl +1 in which nl ≥ 0 (when nl = 0 the rule is premise-free), the antecedents and consequents of all sequents in R1i , . . . Rki i are finitely long (perhaps zero length) strings of schematic expressions separated by commas, and the schematic expressions that may occur in the sequents in R1i , . . . Rki i are given by the following prescription: (i) metavariables for formulas and metavariables for sequences of formulas are schematic expressions; (ii) an application (of the appropriate arity) of any operator of any index to schematic expressions that are formulas yields a schematic expression again; and (iii) nothing else is a schematic expression. Other than their initial specification part and their structural rules, propositional rule systems are thus nothing but finite sequences of finite sequences of finitary rules; infinite rules, such as e.g. the infinitary ω-rule for natural numbers, are therefore excluded from the start. But otherwise propositional rule system are very much unconstrained. In particular, the syntactic form 25 of propositional rule systems need not have anything in common with that of definitions: e.g., the rules for the operator o1 might involve the operator o2 but also vice versa (circularity); a single rule for o1 might simultaneously include different applications of o1 to different sequences of metavariables (unlike a definiens in an explicit definition of a function symbol which includes a single X that is to be characterized); and the rules for o1 might include an application of o1 to a sequence of metavariables where the metavariables are not all pairwise distinct (unlike in the definiendum in an explicit definition). For that reason, I will define an additional, much more restrictive notion of simple propositional rule system now. The second-order counterpart of any such simple system will be a second-order statement satisfying at least the syntactic requirements of definitions. Whether it will also satisfy the deductive requirement of its unique-existence claim being provable in the deductive system of second-order logic remains to be seen in a case-by-case manner. For each operator oi of arity ji , consider its application to the ji -many pairwise distinct metavariables A1 , . . . , Aji , oi (A1 , . . . , Aji ), and speak of this very formula as being the one and only formula that is in simple general form for oi . (It is only important that we fix one application of oi to a sequence of pairwise distinct metavariables; but choosing them to be A1 , . . . , Aji will not restrict generality in any way.) We will make sure that all occurrences of oi in its “defining” rules will be in the context of the formula oi (A1 , . . . , Aji ) that is in simple general form for oi , so that there will be a uniquely determined expression that can be replaced by X later. In the standard theory of definitions, the counterpart of this is the constraint that the definiendum of a definition must be an atomic formula in which all variables are pairwise distinct. Other than that, simple propositional rule systems will also have a well-founded structure that mimics that of sequences of explicit definitions in which each definition may only use terms that have been defined “before”. Finally, as mentioned in the last section, I will always presuppose Reflexivity and the usual structural rules to be present: Metadef. 5 A simple propositional rule system R for the sequence o1 , . . . , om of propositional operators (in that order) is a sequence of the following components: • A specification of whether multiple conclusions are syntactically permissible in a sequent (as in the sequent calculus) or not (as in natural deduction). 26 • Reflexivity and the usual structural rules of Permutation, Weakening, Contraction, and Cut (suitably adapted to the chosen specification). • For each i with 1 ≤ i ≤ m, a system of ki -many rules for oi , R1i , . . . Rki i , where for all l with 1 ≤ l ≤ ki , Rli is an expression of the form (oi Rli ) i,l i,l Φi,l . . . Φi,l nl ⊢ Ψnl 1 ⊢ Ψ1 i,l i,l Φnl +1 ⊢ Ψnl +1 in which nl ≥ 0 (when nl = 0 the rule is premise-free), the antecedents and consequents of all sequents in R1i , . . . Rki i are finitely long (perhaps zero length) strings of schematic expressions separated by commas, and the schematic expressions that may occur in the sequents in R1i , . . . Rki i are given by the following prescription: (i) metavariables for formulas and metavariables for sequences of formulas are schematic expressions; (ii) an application (of the appropriate arity) of any operator with index less than i to schematic expressions that are formulas and that do not include any operator with index greater than i yields a schematic expression again; (iii) the uniquely determined formula oi (A1 , . . . , Aji ) that is in simple general form for oi is a schematic expression; and (iv) nothing else is a schematic expression. The potentially “non-definitional” syntactic features of general propositional rule systems are thus prohibited now: e.g., it could not simultaneously be the case that the rules for o1 involve o2 and the rules for o2 involve o1 . It also follows that o1 (A, B) and o1 (B, A) could not occur simultaneously in the rules for o1 (where A = A1 and B = A2 ); similarly, while o1 (A, B) may occur in the rules for o1 , the expression o1 (o1 (A, B), A) must not occur; and o1 (A, A) could not occur in the rules for o1 either. But e.g. o1 (B, o2 (A)) may well occur in the rules for o2 (where A = A1 , and o1 would have been characterized by its own rules beforehand). Call R a [simple] propositional rule system just in case there is a sequence o1 , . . . , om of propositional operators, such that R is a [simple] propositional rule system for o1 , . . . , om . Every simple propositional rule system is of course also a propositional rule system, and the system of natural deduction rules for ∨ from the last section constitutes an instance of such a simple propositional rule system, as does the system of sequent calculus rules for ∨. The goal is now to translate such simple propositional rule systems into sequences of second-order definitions and to do so in a stepwise manner: 27 first applying the translation manual to the rules for o1 , yielding the first definition; then to the rules for o2 , generating the second definition; and so on. But for that purpose we need to adapt T1, T2, T4, T5, T8, T10 from the last section so that they can be applied to the rules R1i , . . . Rki i for an operator oi in an arbitrary simple propositional rule system: T1 (Generalized) Replace oi (A1 , . . . , Aji ) by the atomic formula X(w) with the unary set variable X and the first-order variable w. T2 (Generalized) Replace each remaining schematic expression that is a formula and that does not occur as proper part of another schematic expression by changing o1 , . . . , oi−1 into O1 , . . . , Oi−1 , respectively, and of adding ‘(w)’ at the very end of the result. In this way, if a metavariable A does not occur as part of a larger schematic expression, it is still replaced by the respective atomic formula A(w) with a unary set variable A and the first-order variable w, and occurrences of pairwise identical/distinct metavariables are still replaced by occurrences of pairwise identical/distinct set variables. But additionally, e.g., if o1 and o2 are both binary, every occurrence of o1 (o2 (A, B), C) that is not part of a larger schematic expression is replaced by O1 (O2 (A, B), C)(w); etc. T4 (Generalized) For each premise-free rule, replace the empty premise sequent by ‘w = w’. Replace ⊢ by the implication operator →. T5 (Further Extended) Replace commas in antecedents of implications by conjunction symbols and in consequents of implications by disjunction symbols. Replace an empty antecedent by w = w and an empty consequent by w ̸= w. T8 (Generalized) Universally quantify the resulting replacement of each rule by universal second-order quantifier expressions for the replacements of metavariables for sequences in that rule and by universal second-order quantifier expressions for the replacements of all metavariables for formulas in that rule other than A1 , . . . , Aji . T10 (Generalized) Use the resulting replacement of the rule system for oi as the definiens of a definition that starts with universal second-order quantifier expressions of the form ∀A1 , . . . , Aji , X, followed by the definiendum Oi (A1 , . . . , Aji ) = X where Oi is a function constant, and add the equivalence ↔ and the definiens that was constructed by T1–T9 on the right. With these adjustments in place, we can apply the translation manual to an arbitrary simple propositional rule system in the intended step-by-step 28 manner: first to the system of k1 -many rules for o1 , leading to a statement that aims to define O1 in the language of pure classical second-order logic; then the same for o2 and O2 ; and so forth. Just as for disjunction in the last section, the resulting second-order statement for Oi captures the inferential role that oi plays in its own rule system R1i , . . . Rki i . Since it is easy to see that these second-order statements also satisfy the syntactic requirements for definitions, they constitute definitions of the respective O1 , . . . , Om just in case the following deductive conditions concerning the corresponding universally quantified unique-existence formulas are satisfied: U EO1 is provable in the deductive system of second-order logic; U EO2 derivable in the deductive system of second-order logic from the previous definition of O1 ; and so forth, all the way to: U EOm is derivable in the deductive system of second-order logic from the previous definitions of O1 , . . . , Om−1 . This leads to our general criterion for whether a given propositional rule system R for o1 , . . . , om defines o1 , . . . , om : Metadef. 6 (Translation Criterion for Propositional Rule Systems) A propositional rule system R for o1 , . . . , om defines o1 , . . . , om just in case (a) R is a simple propositional rule system in the sense of Metadef. 5, and (b) T1–T10 (as generalized above) translate R into a sequence T [R] of definitions of the corresponding function constants O1 , . . . , Om in the language of pure classical second-order logic expanded by previously defined expressions. If so, call R definitional. Part (a) ensures the translation will meet the syntactic conditions for the definition of function symbols. So what part (b) actually adds to this is that the unique-existence conditions U EO1 , . . . , U EOm follow from the deductive system of second-order logic and previous definitions. Whether they do, obviously depends on what the rules in their respective rule system are like. E.g., as we will see in Section 6, the unique-existence requirement fails for the rules for tonk and hence these rules do not define tonk. But whenever a rule system R does define its operators in the sense of Definition 6, the sequence T [R] of second-order definitions that results from translating the rules of R determine the semantic meanings of the respective operators uniquely, just as for disjunction in the last section. Furthermore, checking whether R defines o1 , . . . , om decomposes into a sequence of such checks for its sub-rule-systems R1i , . . . Rki i for the respective operators oi : while each such test must trivially depend on previous checks of the sub-rule-systems of those operators of index less than i that occur in 29 the rules for oi , the test for the sub-rule-system for oi is independent of that for the sub-rule-systems for operators with an index greater than i. And if oi is the only operator that occurs in its supposedly meaning-constitutive rules R1i , . . . Rki i , its test will solely concern its own rules. In other words: Fact 7 The Translation Criterion is local in the same sense as harmony is. What is more: once each defined expression has been unpacked in terms of its defining expressions, each of the universally quantified unique-existence claims U EOi that results as a by-product of applying our translation manual T1–T10 to a simple propositional rule system is in fact a statement in the language of pure monadic second-order logic: the set of formulas of pure classical second-order logic (without descriptive terms) in which only unary set variables and no function variables occur. But pure monadic second-order logic without function variables is decidable (cf. Löwenheim 1915, Skolem 1919, Behmann 1922, Ackermann 1968), and hence there is a mechanical procedure by which it can be decided whether T1–T10 translate a simple propositional rule system into a sequence of second-order definitions. Since it is also decidable on grounds of syntactic form whether an arbitrary propositional rule system is a simple propositional rule system in the sense of Metadef. 5, we get: Fact 8 It is decidable whether, according to the Translation Criterion, a propositional rule system R defines its operators. In fact, one would not have to invoke any general decidability result to see that this is so: once a simple propositional rule system has been translated into a sequence of statements in the language of pure monadic second-order logic, it is easy to see that whether the required unique-existence claims hold only depends on facts about truth value assignments to finitely many atomic formulas (A(w), X(w),. . .) which can be checked computationally. Equivalently: one can decide such claims by only testing assignments of ∅ and {w: w = w} to set-variables. By the same token, it becomes possible to clarify which second-order functions from propositions to propositions get defined by the translations of propositional rule systems that manage to define their operators. As we have seen, both the natural deduction rules and the sequent calculus rules for ∨ define ∨ and translate into the second-order definition of Dis, where Dis expresses nothing else than the set-theoretic union of propositions. And 30 unions can be determined by the pointwise application of the standard classical truth function for ∨ at each w. This generalizes: if a propositional rule system defines an operator according to the Translation Criterion, the operator is such that it expresses a function on propositions that can be defined by a truth table; and for each function on propositions that can be defined by a truth table there is a propositional rule systems that defines an operator expressing that function after second-order translation: Fact 9 The set-functions Op that correspond to operators op defined by propositional rule systems are precisely those that can be generated pointwise from classical truth functions fOp . Or in other words, the following two statements are equivalent for an arbitrary n-ary propositional operator op and its second-order translation Op: 1. op is defined by a propositional rule system in the sense of the Translation Criterion (Metadef. 6). 2. There is a classical n-ary truth function fOp (mapping n-tuples of truth values to truth values), such that for all A1 , . . . , An , for all w, IOp(A1 ,...,An ) (w) = fOp (IA1 (w), . . . , IAn (w)) (where IX is the characteristic function of X). Proof. First, we show the left-to-right direction: every Op corresponding to an op defined by a propositional rule system is generated pointwise from a classical truth function. Secondly, we show the right-to-left direction: every Op generated pointwise from a classical truth function corresponds to an op defined by a propositional rule system. Left-to-right: Consider an arbitrary set-function Op that is defined, via the Translation Criterion, by the second-order translation of a propositional rule system. Since the unique-existence claim for Op must be provable logically, it must also be true in “the” (up to isomorphism uniquely determined) smallest secondorder model that has precisely one individual in its first-order domain D. Thus, in that model, Op is nothing but a truth function, say, fOp . Now, for arbitrary second-order models, define a set-function Op∗ from fOp in the pointwise manner described in 2. Op∗ will satisfy the translations of the rules of the given propositional rule system in any such model for the same reason for which fOp satisfied them in the model in which the domain was a singleton. The existence of a set-function distinct from Op that would also satisfy the translation of the given propositional rule system in any of these models would contradict the uniqueexistence claim for Op in that model, which is impossible, as the unique-existence 31 claim for Op is logically true. Hence, Op∗ must be identical to Op, which means that Op is given by a truth function in the way described above. Right-to-left: Now consider an arbitrary n-ary set-function Op that is generated pointwise from a classical truth function fOp . By the well-known functional completeness of the classical propositional operators, say, ∨ and ¬, fOp is definable as some complex composition of the truth functions for ∨ and ¬. Let ϕ(A1 , . . . , Aj ) express that truth function in the language of classical propositional logic with operators ∨ and ¬ and propositional variables A1 , . . . , Aj . It follows that op(A1 , . . . , Aj )—to which Op(A1 , . . . , Aj ) corresponds via translation—is definable by the rule system that consists of the natural deduction rules for ∨ (recall Section 3) and ¬ (see Section 5) and these two additional rules for op: op(A1 , . . . , Aj ) ⊢ ϕ(A1 , . . . , Aj ) ϕ(A1 , . . . , Aj ) ⊢ op(A1 , . . . , Aj ) Semantically speaking, this result entails that the set-functions Op that correspond to operators op defined by propositional rule systems are not just permutation-invariant but also uniform over, and hence insensitive to, the size of the underlying first-order domain.23 There is one final bit of conceptual machinery I need to introduce that will be important for the next section. Consider the system of just the natural deduction introduction rules for ∨ from the last section: as remarked there, that system does not define ∨, but intuitively it should still count as “analytic” in the sense of “following from” the definition of ∨ as given by the system of its introduction and elimination rules. In the present case, there would be an obvious proof-theoretic manner of making this more precise, as the introduction rules for ∨ are (trivially) derivable from the system R∨ of introduction and elimination rules for ∨. But that proof-theoretic understanding of ‘analytic’ and ‘following from’ will not be sufficient for some other purposes that will become relevant in the next section. Rather, I want to express the thought that once the meaning of an operator (such as ∨) has been fixed by its definition through a definitional rule system R (such as R∨ ), that meaning guarantees that the rules in some other rule system R′ (such as just the introduction rules for ∨) are strictly truth-preserving. And that can be made precise by translating R′ into another second-order statement T ′ [R′ ] and determining whether T ′ [R′ ] is derivable in the deductive system of second-order logic from the second-order definition T [R] that corresponds 23 I am very grateful to discussions with Johan van Benthem on this matter. 32 to R. This time, the required translation T ′ [R′ ] of R′ is not meant to have the form of a definition but to be just the conjunction of the immediate second-order renderings of the rules in R′ : e.g., the translation of the system of introduction rules for ∨ should simply be the conjunction ∀A, B, G: ∀w(G(w) → A(w)) → ∀w(G(w) → Disn (A, B)(w)) ∧ ∀A, B, G: ∀w(G(w) → B(w)) → ∀w(G(w) → Disn (A, B)(w)) which is indeed logically derivable from Definition 1. To determine that kind of translation T ′ in general, drop T1 and T10, let T3′ = T3, T4′ = T4, T5′ = T5, T6′ = T6, T7′ = T7, T9′ = T9, and change T2 and T8 into: T2′ Replace each schematic expression (in the sense of propositional rule systems in general) that is a formula by changing o1 , . . . , om into O1 , . . . , Om , respectively, and by adding ‘(w)’ at the very end of the result. T8′ Universally quantify the resulting replacement of each rule by universal secondorder quantifier expressions for the replacements of metavariables for sequences in that rule and by universal second-order quantifier expressions for the replacements of all metavariables for formulas in that rule. Applying T2′ –T9′ to the system of introduction rules for ∨ leads to the second-order conjunction above. And more generally we can define: Metadef. 10 Let R be an arbitrary propositional rule system for o1 , . . . , om that defines o1 , . . . , om . Let R′ be an arbitrary propositional rule system for o1 , . . . , om : R analytically entails R′ if and only if T [R] ⊢ T ′ [R′ ]. That is, R analytically entails R′ just in case from the sequence T [R] of second-order definitions of O1 , . . . , Om that result from applying T1–T10 to R one can logically derive (in the deductive system of second-order logic) the second-order statement T ′ [R′ ] that results from applying T2′ –T9′ to R′ . Equivalently, we will also say: R′ is analytic (with respect to R). Thus, as desired, the definitional system of natural deduction rules for ∨ analytically entails the system of introduction rules for ∨ and hence the latter is analytic (with respect to the former). Of course, every definitional system is trivially analytic (with respect to itself), but not necessarily the other way round: e.g. the system of introduction rules for ∨ is not definitional, that is, does not define ∨. 33 By unpacking all defined terms and using the deduction theorem, the question whether R analytically entails R′ boils down to the question whether a certain second-order material implication statement is provable in the deductive system of second-order logic. E.g., in the case above, where the relevant definition was Def. 1 (. . . Disn (A, B) = X ↔ Definiens[A, B, X]), the question reduces to whether Definiens[A, B, X] → ∀G: ∀w(G(w) → A(w)) → ∀w(G(w) → X(w)) ∧ ∀G: ∀w(G(w) → B(w)) → ∀w(G(w) → X(w)) is provable logically. (If the rules of R′ involved applications of ∨ to several different constructions on metavariables, the antecedent of that material implication would have to be a conjunction of the form Definiens[A, B, X] ∧ Definiens[A′ , B ′ , X ′ ] ∧ . . .) And since that material implication statement belongs again to the language of monadic second-order logic without function terms, we can once more invoke the decidability of that fragment of secondorder logic (recall Section 4) to conclude: Fact 11 It is decidable whether a propositional rule system R analytically entails a propositional rule system R′ . The next section will exhibit non-trivial examples of rule systems that are analytic with respect to a given system of definitional rules but which are not deductively derivable from that system of definitional rules. Turning to the standard natural deduction and sequent calculus rule systems for the usual logical operators, and applying the general Translation Criterion and the notion of analyticity (where analyticity is always with respect to the intuitionistic systems), we get the following results: 34 Propositional rule systems defining a classical operator and/or being analytic: Rule Format Rule System Operator Defines Op. Analytic ∧ ✓ ✓ Natural Deduction Minimal ∨ ✓ ✓ → ✓ ✓ ⊥ X ✓ ¬ X ✓ ∧ ✓ ✓ Intuitionistic ∨ ✓ ✓ → ✓ ✓ ⊥ ✓ ✓ ¬ ✓ ✓ ∧ ✓ ✓ Classical ∨ ✓ ✓ → ✓ ✓ ⊥ X ✓ ¬ X ✓ ∧ ✓ ✓ Sequent Calculus Minimal ∨ ✓ ✓ → ✓ ✓ ⊥ X ✓ ¬ X ✓ Intuitionistic/Classical All ✓ ✓ Table 1: The Main Outcomes for Standard Propositional Operators A selection of these results will be discussed and proven in the next section. The results from Section 3 concerning disjunction correspond to those checkmark (✓) cells that mark that the minimal/intuitionistic/classical natural deduction rules and the minimal/intuitionistic/classical sequent calculus rules for ∨ manage to define ∨. The ‘X’ symbol marks failure. 5 The Rules for →, ⊥, ¬ and Distinguishing Expressive and Deductive Completeness The general translation manual from the previous section is ready to be applied to all traditional rule systems of propositional logical operators in minimal, intuitionistic, and classical logic. For instance, consider the natural deduction rule system R→ for →, stated immediately in sequent notation: (→ I) Γ, A ⊢ B Γ⊢A→B (→ E) Γ⊢A→B ∆⊢A Γ, ∆ ⊢ B R→ is yet another simple propositional rule system in the sense of Metadef. 5. Its translation yields the following definition T [R→ ]: 35 Def. 12 ∀A, B, X: Impn (A, B) = X ↔ (→∗ I) ∀G: ∀w(G(w) ∧ A(w) → B(w)) → ∀w(G(w) → X(w)), (→∗ E) ∀G, D: ∀w(G(w) → X(w)) ∧ ∀w(D(w) → A(w)) → ∀w(G(w) ∧ D(w) → B(w)). That this is a definition can be shown by proving U EImpn again logically: for arbitrary A and B, the existence of the required X follows from the instance of Comprehension that postulates the (with Extensionality, unique) existence of the material implication proposition [{w | w = w} \ A] ∪ B, ∀A, B ∃X∀w(X(w) ↔ ¬A(w) ∨ B(w)), for which the deductive system of second-order logic proves that it satisfies (→∗ I) and (→∗ E). Uniqueness follows from Comprehension for A, B, the negation proposition {w | w = w} \ A, and [{w | w = w} \ A] ∪ B again: consider an arbitrary X that satisfies (→∗ I) and (→∗ E). With G = [{w | w = w} \ A], it follows from (→∗ I) and second-order logic that [{w | w = w} \ A] ⊆ X. With G = B it follows from (→∗ I) and second-order logic that B ⊆ X; hence, by second-order logic, [{w | w = w} \ A] ∪ B ⊆ X. Furthermore, for G = X and D = A, it follows from (→∗ E) that X ∩ A ⊆ B. Now assume that X ̸⊆ [{w | w = w} \ A] ∪ B: then, by second-order logic, X ∩ A ∩ [{w | w = w} \ B] ̸= ∅, which would contradict X ∩ A ⊆ B. Therefore, X ⊆ [{w | w = w} \ A] ∪ B, which entails with Extensionality and what was shown before that X = [{w | w = w} \ A] ∪ B. What this demonstrates is not just that the natural deduction rule system R→ defines → according to the Translation Criterion (Metadef. 6), but that its second-order translation T [R→ ] actually pins down the semantic meaning of → to be that of classical material implication. Which, at least prima facie, may sound surprising: after all, the natural deduction rules for → above are not just employed in classical logic, but they are also used in intuitionistic and even minimal logic in which the standard conditional is of course not provably equivalent to material implication. And Peirce’s law, ((A → B) → A) → A, is a famous instance of a formula that is provable in (full) classical logic without being provable by the natural deduction rules for → alone. So how 36 come the Translation Criterion regards these natural deduction rules as defining classical material →? Doesn’t that undermine the Criterion? In what follows, I will argue that this worry is unjustified. Here are two comparable cases. The deductive system of second-order logic proves the (internal) categoricity of the second-order Dedekind-Peano axioms of arithmetic (see Väänänen and Wang 2015) and thus determines the meaning of arithmetical terms up to isomorphism, while the same system is of course deductively arithmetically incomplete in view of the incompleteness theorems. And in a first-order context, Gödel taught us how to define (up to coding) a provability predicate for first-order Peano arithmetic (PA) within the language of PA, such that the arithmetical definition of P rov gets the semantic extension of provability right and allows for the provability of some salient arithmetical facts concerning P rov in PA. But that does not mean that every arithmetically true statement including P rov is derivable in PA: e.g., the consistency statement ¬P rov(⌜⊥⌝) is true but not derivable in PA (assuming PA is consistent). So PA is expressive enough to define P rov, without being deductively strong enough to prove all arithmetically true statements involving P rov. Translated mutatis mutandis into the present context: the natural deduction rules for → are expressively complete in defining →, without being deductively strong enough to prove all logically true statements involving →, such as Peirce’s law. The rules get the semantic meaning of → right, as demonstrated in the proof above, even though they are deductively incomplete with respect to →-statements. And the reason they get the semantic meaning of → right is that they involve metavariables or open-ended schematic letters that may be understood to express arbitrary propositions, including negation propositions like {w | w = w}\A and material implication propositions like [{w | w = w} \ A] ∪ B.24 It is such propositions over which the second-order variable X ranges in the proof of U EImpn above. In fact, the proof is not so different that of U EDisn in the last section, except that the propositions required would typically be expressed linguistically with the help of an operator (negation) that does not occur in the rules for →. But, from a classical point of view, these propositions exist independently of whether and how they are expressed linguistically. The role of second-order logic in the proof above is merely to allow us to quantify over these propositions and 24 Compare McGee (2015) who argues that schematic letters need to be understood in that way for the purpose of deriving his categoricity results for classical logical operators. 37 to prove the existence of such negation propositions and material implication propositions with the help of the Comprehension Scheme. In order for the deductive strength of the rules to catch up, it would indeed be necessary to add further rules, such as those for ⊥ or ¬, so that the required propositions and their truth-conditional relationships would be captured by →/⊥/¬-formulas and their rules, and further logical truths would become derivable, such as Peirce’s law. But the expressive strength of the natural deduction rules for → is already sufficient to determine the classical meaning of →, so long as one understands the metavariables in these rules to express arbitrary sets of worlds or at least propositions with a Boolean structure in which classical negation and material implication propositions exist.25 In short: the natural deduction rules for → are expressively complete but (classically) deductively incomplete.26 The point can be driven home by invoking the notions of analytic entailment/analyticity from the last section (recall Metadef. 10): the simple propositional rule system R→ of natural deduction rules for → defines → and hence is definitional. While R→ does not derive the propositional rule system RP ei for → that only consists of Peirce’s law stated in the form ⊢ ((A → B) → A) → A it does hold that R→ analytically entails RP ei (or in other words, RP ei is analytic with respect to R→ ). The proof of that analyticity claim consists in deriving the second-order translation T ′ [RP ei ] of RP ei , ∀A, B(∀w(w = w) → ∀w(w = w → Impn (Impn (Impn (A, B), A), A)(w))), 25 Here we deviate from Woods’ (unpublished) requirement that “applying a method for specifying the meaning of a connective to the implicational fragment of classical logic [as given by the natural deduction rules for →] should not yield the full classical meaning of →.” He says so because he thinks that →’s classical meaning outstrips its inferential role in these rules; but that is not the case if one takes these rules to govern strict implications between arbitrary propositions in the sense of classical intensional semantics. 26 Section 7 will suggest an extension of the present approach in which changing both the underlying structure of propositions and the second-order logic by which that structure is described would let the rules of → translate into a second-order definition that would deliver a non-classical meaning for → through quantification over non-classical propositions and non-classical worlds or states. Depending on what that non-classical structure and logic are like, this might also yield a way of realigning inferential content and truthconditional meaning. I am grateful to an anonymous reviewer for suggesting this possibility of realignment. 38 or equivalently, ∀A, B∀w Impn (Impn (Impn (A, B), A), A)(w), from T [R→ ], that is, from Definition 12, in the deductive system of secondorder logic. To do so, one uses that the definition entails ∀A, B(Impn (A, B) = [{w | w = w} \ A] ∪ B), as shown before. I hope this makes clear why the deductive weakness of the natural deduction rules for → does not undermine the conclusion that these rules determine the classical truth conditions of → even in the absence of the rules of ⊥ and ¬. Hence, the Translation Criterion, from which that conclusion was derived, is not undermined either. And note that none of the considerations above need to be invoked in the case of the classical sequent calculus rules for →: they turn out to define → according to the Translation Criterion and, by exploiting the admissibility of multiple conclusions to the right of the turnstile, they are also deductively complete and derive Peirce’s law. Once again, second-order logic derives the equivalence of the definition of Impn above with the definition of Imps from the sequence calculus rules: ∀A, B: Impn (A, B) = Imps (A, B). So we can drop the indices and just write Imp again. Let us consider negation now. The case of the classical sequent calculus rules for ¬, (L¬) Γ ⊢ A, ∆ Γ, ¬A ⊢ ∆ (R¬) Γ, A ⊢ ∆ Γ ⊢ ¬A, ∆ is again straightforward: they constitute a simple propositional rule system, and the deductive system of second-order logic proves its translation by T1–T10 to be a definition of N egs . So let us focus again on the more interesting case of natural deduction. In contrast with the sequent calculus, the standard way of introducing negation by classical natural deduction rules that do not involve other logical operators (see, e.g., Halbach 2015, pp. 25f) leads to a propositional rule system that is not simple: for the system Rcn , Γ, ¬A ⊢ B ∆, ¬A ⊢ ¬B Γ, ∆ ⊢ A Γ, A ⊢ B ∆, A ⊢ ¬B Γ, ∆ ⊢ ¬A includes different applications of ¬ to different metavariables (A, B) within one and the same rule. Accordingly, there would not be a uniquely defined 39 way of replacing “the” occurrence of ¬ . . . by the second-order variable X. By the Translation Criterion, the propositional rule system Rcn for classical negation is therefore not definitional, as it is not simple. A similar problem would emerge if the rule of double negation elimination Rdn (considered by Gentzen 1935), ¬¬A ⊢ A were combined with rules for ⊥ and other rules for negation, even if ⊥ had already been defined by rules that would not involve ¬ (such rules for ⊥ will be considered below): for the double-negation-elimination rule Rdn involves ¬¬A and hence an application of ¬ to a complex expression, which is ruled out again from simple propositional rule systems. If the rule system were formulated in yet another typical classical manner to the effect that the supposedly defining rules for ¬ involved ⊥ and those for ⊥ involved ¬, as holds for Gentzen (1935) in which rules for ¬ and ⊥27 were combined with the excluded-middle rule Rem , ⊢ A ∨ ¬A this would not constitute a simple propositional rule system either, since simplicity excludes any kind of circularity or any attempts of defining two logical operators simultaneously. The same applies to the combined system for ⊥ and ¬ in Chiswell and Hodges (2007, Section 2.6). Since all of these rule systems for classical negations do not conform to the syntactic constraints of simple propositional rule systems, and since these syntactic constraints had been introduced to match those of explicit definitions in normal form, the rules for ¬ considered so far should be regarded as problematic from the inferentialist point of view as explicated by the Translation Criterion. However, just as the intuitionistic rules for → sufficed for defining classical →, it turns out that it is possible to define classical negation intuitionistically: by defining some other operators using the standard intuitionistic rules first and then defining negation from these operators in an intuitionistic manner. For instance, one may follow the standard intuitionistic path towards ¬ via → and ⊥: Def. 12 of classical Imp (corresponding to →) is already in 27 Though Gentzen (1935) did not actually present ⊥ as a logical symbol. 40 place. And the translation of the intuitionistic elimination rule for ⊥, (⊥E) Γ⊢⊥ Γ⊢A is sufficient for defining classical ⊥: Def. 13 ∀X: F aln = X ↔ (⊥∗ E) ∀G, A: ∀w(G(w) → X(w)) → ∀w(G(w) → A(w)). Existence follows from Comprehension with X = ∅, and uniqueness follows from assuming the definiens for X, instantiating Comprehension with G = X and A = ∅, and concluding that X = ∅. (The sequent calculus rules for ⊥ lead again to an equivalent definition, which is why we can just say: F al.) The classical elimination rule Rcf for ⊥, ¬A, Γ ⊢ ⊥ Γ⊢A is therefore not required to define ⊥ classically. Intuitionists would now define negation using → and ⊥: ¬A =df A → ⊥ In our context, we can present this metalinguistic abbreviation of A → ⊥ by ¬A in the form of the rules (¬1) ¬A ⊢ A → ⊥ (¬2) A → ⊥ ⊢ ¬A that extend the previous rules of → and ⊥ to a simple propositional rule system for →, ⊥, ¬. Translating this system into a sequence of second-order definitions leads to the following definition of N egn : Def. 14 ∀A, X: N egn (A) = X ↔ (¬∗ 1) ∀w(w = w) → ∀w(X(w) → Imp(A, F al)(w)), (¬∗ 2) ∀w(w = w) → ∀w(Imp(A, F al)(w) → X(w)). Or with Extensionality: N egn (X) = Imp(A, F al). (Since N egn = N egs is provable again, one may just write N eg.) Thus, the simple propositional rule system for →, ⊥, ¬ that follows the intuitionistic natural deduction understanding of these three operators defines the classical →, ⊥, ¬. 41 Of course, that rule system is deductively incomplete again from the classical point of view, but we have already seen that this does not rule out its expressive completeness. And it is easy to show that the same system analytically entails the natural deduction rule systems Rcf for classical ⊥, Rcn for classical ¬, Rdn for double negation elimination, and Rem for the excluded middle that were considered above. Hence, even though the usual classical natural deduction rule systems for ¬ are not definitional, they are still analytic (with respect to the intuitionistic rule system for →, ⊥, ¬).28 This completes our study of usual logical propositional operators: in the sense afforded by our Translation Criterion, all of them turn out to be definable by fairly common sequent calculus and natural deduction rule systems.29 6 Tonk, Conservativeness, and Consistency It is time to reconsider Prior’s (1960) rules for the binary tonk operator, which constitute the simple propositional rule system Rtonk : (L tonk ) A tonk B ⊢ B (R tonk ) A ⊢ A tonk B Applying our translation rules to it yields the following pseudo-definition: Pseudo-Definition 15 ∀A, B, X: Tonk (A, B) = X ↔ (L tonk) ∀w (w = w) → ∀w(X(w) → B(w)), (R tonk) ∀w (w = w) → ∀w(A(w) → X(w)). 28 A different way of understanding these results concerning negation is through Popper’s (1948) observation that, when the classical rules for a negation symbol are combined with the intuitionistic rules for another negation symbol, the two negations become provably equivalent. To some extent, that is what happens here, too, when the rules for intuitionistic negation get translated into the language of classical second-order language that already includes classical negation. However, unlike Popper’s result, this happens via a detour through the second-order comprehension scheme in which the substitution of classical negation formulas yields the proof of the existence of classical negation propositions. (I am grateful to an anonymous reviewer for pointing out the resemblance with Popper’s result.) 29 They would also be definable in the same sense by less common formulations of natural deduction rules, such as e.g. those proposed by Milne (2015). 42 Or equivalently: ∀A, B, X: Tonk (A, B) = X ↔ ∀w(X(w) → B(w)) ∧ ∀w(A(w) → X(w). This is a pseudo-definition, since the deductive system of second-order logic does not prove ∀A, B ∃!X T onk(X, A, B). It does not even prove ∀A, B ∃X Tonk (X, A, B). In fact, second-order logic proves: ¬∀A, B ∃X Tonk (X, A, B). So the above is not a definition according to the standard theory of definitions and thus, according to the Translation Criterion: Fact 16 The rule system Rtonk does not define tonk. The proof is immediate: let A = W and B = ∅ and suppose there is an X, such that the definiens is satisfied. Then, by (R tonk) and (L tonk), {w: w = w} ⊆ C ⊆ ∅, which is a contradiction, since ∃w w = w is a logical truth. Similarly, one can show that none of the following rule systems is definitional either: first, McGee’s (̸ c1) A⊢B (̸ c2) B ⊬ cA ̸ cA ⊢ A See McGee (2015, p. 179), who effectively proves the system not to be definitional. In his terminology: “there isn’t any operator ̸ cP ROP that satisfies the propositional analogues of the rules for ̸ c”. Secondly, consider Belnap’s (plonk) B ⊢ A plonk B See Belnap (1962, p. 132). Here existence can be proven logically, but uniqueness cannot. Finally: (L∗) A⊢C B⊢C A⊢C B⊢C (R∗) A∗B ⊢C C ⊢A∗B This is a new operator, which I am calling ‘schtonk’, and which is loosely inspired by Suppes’ (1957, p. 152) example of a failed arithmetical “definition”. Assume existence: by instantiating (L∗) with A = B = C = ∅, it follows that ∅ ∗ ∅ ⊆ ∅. But instantiating (R∗) with A = B = ∅ and 43 C = {w: w = w} yields {w: w = w} ⊆ ∅∗∅. This implies {w: w = w} ⊆ ∅, contradicting the logical truth ∃w w = w again. In contrast, consider Read’s 0-ary bullet operator •, the meaning of which is meant to be given by the introduction rule: (•) A⊢•→⊥ A⊢• See Read (2000, p. 141, 2010, p. 571). If an elimination rule is added to (•) on general grounds of harmony, the resulting pair of rules can be show to lead to inconsistency (Read 2000, p. 141). But given the Translation Criterion, this does not show that the introduction rule (•) itself would be defective, as (•) does succeed in defining •. Here is why: translated into second-order terms terms, (•) expresses that if A ⊆ [{w: w = w} \ Bul] then A ⊆ Bul (where Bul is the second-order translation of •). Existence follows from identifying Bul with {w: w = w}. Uniqueness follows from instantiating the previous if-then statement with A = [{w: w = w} \ Bul], which yields that [{w: w = w} \ Bul] ⊆ Bul, which in turn entails that Bul = {w: w = w}. So (•) defines •, and what • expresses in second-order terms is the same proposition that gets expressed also by the logical verum ⊤.30 Returning to tonk : could it ever be the case that a definitional simple propositional rule system is inconsistent in the sense of deriving A ⊢ B for two distinct metavariables A and B? Equivalently: that it derives the empty sequent ⊢ ? Or that it analytically entails or ? A⊢B ⊢ Fortunately, none of that can ever happen, for the following reason: first one observes that every syntactical derivation in a simple propositional rule system for o1 , . . . , om can be translated into a corresponding logical derivation from the deductive system of second-order logic extended by the definitions of O1 , . . . , Om , where these definitions resulted from applying the translation manual T1–T10 to the system. The translation of the derivation itself proceeds by applying the translation manual T2′ –T9′ that was used to define analytic entailment in Section 4. (In fact, T7′ = T7 will not have to be used.) Let me explain this by means of an example. Here is a typical syntactical derivation in the system R→ of natural deduction rules for → (the system discussed at the beginning of Section 5): 30 I am grateful to Stephen Read for urging me to comment on this example. 44 A → (B → C) ⊢ A → (B → C) A⊢A A → (B → C), A ⊢ B → C A→B⊢A→B A⊢A A → B, A ⊢ B A → (B → C), A, A → B, A ⊢ C A → (B → C), A, A → B ⊢ C A → (B → C), A → B ⊢ A → C A → (B → C) ⊢ (A → B) → (A → C) ⊢ (A → (B → C)) → ((A → B) → (A → C)) For example, in the top-left corner of the derivation, premise-free Reflexivity gives us A → (B → C) ⊢ A → (B → C) and A ⊢ A, to which → E is applied to derive A → (B → C), A ⊢ B → C. Etc. Applying T2′ –T9′ just to the sequents in that inference step (not to the rules, which is why T7′ is not used), one moves from the logical truths ∀A, B, C: ∀w(Imp(A, Imp(B, C))(w) → Imp(A, Imp(B, C))(w)) and ∀A: ∀w(A(w) → A(w)) to the conclusion ∀A, B, C: ∀w(Imp(A, Imp(B, C))(w) ∧ A(w) → Imp(B, C)(w)) that follows logically from the previous two logical truths and from the part (→∗ E) ∀A, B, ∀G, D: ∀w(G(w) → Imp(A, B)(w)) ∧ ∀w(D(w) → A(w)) → ∀w(G(w) ∧ D(w) → B(w)) of the definiens in Def. 12 of Impn = Imp (where I have replaced X by the so-defined Imp(A, B)) in the deductive system of second-order logic. If one continues in this manner, suppresses all initial universal quantifiers that involve metavariables, and abbreviates ∀w(. . . ∧ . . . → . . .) by . . . ∩ . . . ⊆ . . ., one gets a direct translation of the original syntactical derivation in the natural deduction rule system R→ into a logical derivation in the language of second-order logic. Applications of the rules → I and → E are thereby translated into respective applications of the definitional clauses →∗ I and →∗ E from the second-order Def. 12 of Impn : Imp(A, Imp(B, C)) ⊆ Imp(A, Imp(B, C)) A⊆A Imp(A, Imp(B, C)) ∩ A ⊆ Imp(B, C) Imp(A, B) ⊆ Imp(A, B) Imp(A, B) ∩ A ⊆ B Imp(A, Imp(B, C)) ∩ A ∩ Imp(A, B) ∩ A ⊆ C Imp(A, Imp(B, C)) ∩ A ∩ Imp(A, B) ⊆ C Imp(A, Imp(B, C)) ∩ Imp(A, B) ⊆ Imp(A, C) Imp(A, Imp(B, C)) ⊆ Imp(Imp(A, B), Imp(A, C)) {w: w = w} ⊆ Imp(Imp(A, Imp(B, C)), Imp(Imp(A, B), Imp(A, C))) 45 A⊆A The same holds for all other syntactical derivations in R→ . From this one can conclude: if R→ were inconsistent, that is, were to derive the sequent A ⊢ B, this would imply that the second-order translation of that sequent, ∀A, B: ∀w(A(w) → B(w)), would have to be logically derivable from Def. 12 of Impn in the deductive system of second-order-logic. But ∀A, B: ∀w(A(w) → B(w)) is a logical contradiction that is of course not provable in second-order logic, and since Def. 12 is a standard definition and hence non-creative and conservative, such a logical contradiction could not follow from Def. 12 in second-order logic either. Indeed, since standard definitions are both proof-theoretically and semantically conservative (see Gupta 2021, Section 2.3), such a logical contraction could neither be derivable from Def. 12 in the deductive system of second-order logic nor be logically implied by that definition in full second-order logic. Therefore, it cannot be the case that R→ is inconsistent. The same point generalizes to all simple propositional systems that are definitional: Fact 17 • Every syntactical derivation in a definitional propositional rule system R for operators o1 , . . . , om translates into a corresponding logical derivation, in the deductive system of second-order logic, from the sequence T [R] of second-order definitions that corresponds to R. • Definitional conservativeness: In a definitional propositional rule system R for operators o1 , . . . , om , the rules for oi are not necessarily prooftheoretically conservative over the rules for the operators oj with j < i (recall Section 5 on Peirce’s Law). But the second-order definition that corresponds to the rules for oi is proof-theoretically conservative over the deductive system of second-order logic extended by the second-order definitions that correspond to the rules for oj with j < i. And it is also semantically conservative over full second-order logic so extended. • Every definitional propositional rule system is consistent. Analogous points can be made about rule systems that are analytically entailed by a definitional simple propositional rule system R. In particular: Fact 18 Every propositional rule system that is analytically entailed by a definitional propositional rule system is consistent. 46 E.g., since Rtonk is inconsistent (assuming, as always, Cut), it follows that Rtonk could not be analytically entailed by any definitional simple propositional rule system either. 7 Conclusions and Possible Extensions The aim of this paper was to explicate what it means for rule systems to define logical operators, and to determine for some of these rule systems whether they define logical operators and, if so, which operators. For these purposes, I introduced the Translation Criterion (Metadef. 6), formulated for suitable systems of rules for propositional operators (Metadef. 4 and 5), and argued that it constitutes a plausible criterion for when a system of rules defines a logical operator: for it seems intrinsically plausible and leads to the right consequences. The Criterion implements logical inferentialism by translating rules of inference into sentences in the language of pure second-order logic in a way that preserves the inferential role of the relevant propositional operators. The resulting second-order sentences may then be checked for whether they constitute explicit definitions in the standard sense of the theory of definitions. In the case of the intuitionistic natural deduction rules and the intuitionistic and classical sequent calculus rules for the usual logical operators, the translation yields proper definitions (see Table 1 at the end of Section 4), whereas in the case of the rules of Prior’s tonk and other “defective” rule systems it does not (Section 6). Whenever explicit definitions result from the translation, they determine the meaning of the logical operators uniquely, simply by the nature of explicit definitions of function symbols. Every syntactic derivation in the rule system can be mimicked by a second-order logical derivation from the definitions, and the conservativeness of the definitions entails that the rule systems from which they resulted are consistent (Fact 17). The check for whether rules define the operator is local (Fact 7) and, in the present case of propositional operators, decidable (Fact 8). The operators that are definable by rule systems in that manner turn out to be precisely those the semantic meaning of which can be determined by classical truth tables (Fact 9). Some rule systems happen to be definitional but deductively incomplete (e.g. the natural deduction rules for implication in Section 5), which does not speak against the Translation Criterion for the same reasons for which expressive completeness needs to be distinguished from deductive completeness more generally. 47 The typical natural deduction systems for classical negation are not definitional, but they are analytically entailed (Metadef. 10) by the definitional intuitionistic natural deduction rules for → and ⊥ and the definition of ¬ from them (Section 5). Analytic entailment of rule systems for propositional operators is decidable again (Fact 11). The fact that the standard natural deduction systems for classical negation are not definitional at least partially confirms antirealist suspicions that there is something problematic about these systems. However, no serious metaphysics is necessary to bridge the gap between the definitional intuitionistic systems and the deductively complete classical rule systems: a combination of inferential meaning and second-order analytic entailment is sufficient for that. Unless, of course, one regards already second-order logic as “metaphysical”: but if so, the ontological commitment is just to “thin” logical objects, such as propositions. In effect, part of the paper may be viewed as an example of “reverse logic” (in analogy with reverse mathematics): how much comprehension is required in order to be able to understand systems of rules as defining classical logical operators? And the answer is not much: disjunctive propositions, material implication propositions, and the like—propositions the existence of which can be proven by presupposing only predicative instances of Comprehension (no second-order quantifiers are involved in the defining clauses for these propositions).31 From this point of view, classical-logical inferentialism does come with some ontological commitment, but the commitment is modest. One of the messages emerging from this paper is: not every rule system defines its operators, just as not every statement involving a function constant counts as an explicit definition of that function constant. In particular, Prior’s rules for tonk do not define tonk . Another message is: so far as the usual classical-logical propositional operators are concerned, their inferential meaning does fix their semantic meaning. In the case of natural deduction, both Introduction and Elimination rules are indispensable for that (recall Section 3), and the rules need to be understood in an open-ended manner by which metavariables are interpreted as expressing arbitrary classical propositions with a Boolean structure. And yet another message is: the classical-logical propositional operators are defined by the intuitionistic rule systems. The resulting inferentialist reconstruction of classical rule systems is that, at first, one defines the classical 31 I am grateful to Greg Restall for suggesting to me to comment on this predicativity feature. 48 operators by rule systems that are already intuitionistically acceptable. Then one observes that certain classical rules are analytically entailed by these rule systems without being syntactically derivable from them. Finally, one adds the relevant rules until expressive and deductive power are in balance again. But the inferentialist task of determining the meaning of the classical-logical propositional operators is already carried out by the intuitionistic rule systems for these operators. There is no doubt that the results in this paper partially reflect the choice of pure classical second-order logic as background framework. This relativity to a background framework does not mean that no progress has been made: e.g., the approach clearly has bite in so far as it rules out the rules for tonk as non-definitional, and the same applies to other inferentialistically deficient rule systems, as explained in Section 6. Instead, I want to suggest that the choice of the background framework—of the language and logic into which rules are being translated—makes some of the inferentialist presuppositions explicit that might remain merely tacit otherwise. In a nutshell: if a logical inferentalist wants to argue that the usual logical rules for the logical operators determine the meaning of these operators, they must already have in mind some conception of meaning: a conception of what it is that ought to be determined by the rules. In the case of the present paper, by choosing the language of pure classical extensional second-order logic to be the target of translation, the schematic letters in rules of inference are being translated into second-order set variables and hence become interpretable as sets of, say, possible worlds, in line with a classical conception of meaning as intension. This explicit relativity of the Translation Criterion to a background framework may even turn into an asset once one realizes that there is more than one way of choosing the background framework: the target language and logic of pure classical second-order logic of the present paper might be exchanged for a non-classical version thereof. This leads to the following questions about future extensions of the approach: • If rules of inference are translated into the language of pure intuitionistic second-order logic,32 does the accordingly reformulated Translation Criterion vindicate the usual intuitionistic rule system as defining their operators? (The hypothesis is: yes, it does.) And of course analogous questions may be raised about other non-classical 32 See e.g. Chapter 11 of Troelstra and Schwichtenberg (2000). 49 logics, too, such as relevant, many-valued, and substructural logics. So the hope is: once classical second-order logic has been replaced by intuitionistic second-order logic with quantifiers ranging over a space of propositions with a Heyting-algebra-like structure, it becomes possible to achieve results analogous to the present ones also for the rules of intuitionistic logic. Or with relevantist second-order logic and propositions occupying a De-Morgan-algebralike structure, the rules of relevantist logic(s) will define their operators; and so forth. Work along these lines will require an extension of the standard theory of definitions to non-classical contexts; and it may be hoped to throw more light on how features of the Translation approach match, or do not match, salient metalogical properties of proof systems (such as conservativity). If one retains the classical background framework of the present paper but turns to the translation of rule systems for first-order quantifiers into sentences of pure classical polyadic second-order logic, the obvious question to be addressed in future work is: • Which first-order quantifiers are definable by rule systems according to the Translation Criterion? (The results in Feferman 2015 suggest: those quantifiers that are definable in the language of first-order logic.) In any case, it is easy to see that the standard first-order universal and existential quantifier are indeed defined by their the standard natural deduction and sequent calculus rule systems. However, the translation of rule systems for quantifiers is a bit more complicated than for propositional operators, since rules need to be translated into schemes of second-order statements with relation variables of arbitrary arity. Similarly: • What does the Translation Criterion entail for rule systems for firstorder identity (x = y)? (The hypothesis is: the standard rule systems define identity.) With the source and target languages of translation being suitably expanded, one may ask analogous questions about modal sentential operators (□A), higher-order operators (∀X etc.), and perhaps even mathematical operators: • Which modal-logical rule systems for □ define □? 50 • Which higher-order logical rule systems for higher-order operators defines these higher-order operators? • Which (if any) mathematical rule systems for mathematical operators define these operators?33 Furthermore: could and should the Translation Criterion be relaxed to allow for translations into definitions by second-order Hilbertian epsilon terms (as in C(A, B) = ϵXS[A, B, X]) by which the requirement of X satisfying S[A, B, X] uniquely could be dropped?34 And: is it possible to extend the notion of simple propositional rule system from Section 4 so that also higher-level rules (which allow for the assumption of inference rules)35 may belong to a rule system? Finally: does the approach throw new light on the explication of the logicality of concepts? As mentioned before, every concept defined in higherorder logic is known to conform to Tarski’s permutation criterion for logicality (further developed by Sher 1991), but not every such definition will be the translation image of a suitable rule system for an operator. Is there a philosophically substantiated way of sharpening the Tarski-Sher criterion by a combined inferentialist-higher-order characterization of logical concepts (in the spirit of Feferman 2015 and Bonnay and Speitel 2021) to be those that are defined by higher-order definitions that result from suitable translations of suitably restricted rule systems? References [1] Ackermann, W. 1968: Solvable Cases of the Decision Problem, Amsterdam: North-Holland. [2] Behmann, H. 1922: “Beiträge zur Algebra der Logik, inbesondere zum Entscheidungsproblem”, Mathematische Annalen 86, 163–229. [3] Bell, J. and M. Machover. 1997: A Course in Mathematical Logic, Fourth Impression, Amsterdam: Elsevier. 33 I am very grateful to Neil Tennant and Ed Zalta for raising this possibility. General considerations from semantic indeterminacy would seem to motivate dropping the uniqueness requirement: see e.g. Leitgeb (2023). 35 See Schroeder-Heister (1984) and Murzi (2020). 34 51 [4] Belnap, N. D. 1962: “Tonk, Plonk and Plink”, Analysis 22/6, 130–4. [5] Binder, D., T. Piecha, and P. Schroeder-Heister (Eds.). 2022: The Logical Writing of Karl Popper, Cham: Springer. [6] Bonnay, D. and S. Speitel. 2021: “The Ways of Logicality: Invariance and Categoricity”, in: G. Sagi and J. Woods (eds), The Semantic Conception of Logic. Essays on Consequence, Invariance, and Meaning, Cambridge: Cambridge University Press, 55–79. [7] Bonnay, D. and D. Westerståhl. 2016: “Compositionality Solves Carnap’s Problem”, Erkenntnis 81/4, 721–39. [8] Brandom, R. 1994: Making it Explicit, Cambridge, Mass.: Harvard University Press. [9] Brandom, R. 2000: Articulating Reasons, Cambridge, Mass.: Harvard University Press. [10] Brandom, R. 2018: “From Logical Expressivism to Expressivist Logic: Sketch of a Program and Some Implementations”, Philosophical Issues 28/1, 70–88. [11] Carnap, R. 1934/1937: Logische Syntax der Sprache, Vienna: Springer. Translated by Amethe Smeaton as The Logical Syntax of Language, London: Routledge, 1937. [12] Carnap, R. 1959: “Theoretical Concepts in Science” (edited by Stathis Psillos), Studies in History and Philosophy of Science 31, 151–72. [13] Chiswell, I. and W. Hodges. 2007: Mathematical Logic, Oxford: Oxford University Press. [14] Cook, R. T. 2005: “What Wrong with Tonk(?)”, Journal of Philosophical Logic 34/2, 217–26. [15] De Benedetto, M. and E. La Rosa. 2024: “Patches, Patchworks, and Epsilon Terms: A Neo-Carnapian Account of Theoretical Terms in Science”, Journal of Philosophical Logic 53, 1495–517. [16] Dummett, M. 1991: The Logical Basis of Metaphysics, Cambridge, Mass.: Harvard University Press. 52 [17] Feferman, S. 2015: “Which Quantifiers Are Logical? A Combined Semantical and Inferential Criterion”, in: A. Torza (ed.), Quantifiers, Quantifiers, and Quantifiers: Themes in Logic, Metaphysics and Language, Cham: Springer, 19–31. [18] Ferreira, F. and G. Ferreira. 2009: “Commuting Conversions vs. the Standard Conversions of the ‘Good’ Connectives”, Studia Logica 92: 62–84. [19] Garson, J. W. 2013: What Logics Mean. From Proof Theory to ModelTheoretic Semantics, Cambridge: Cambridge University Press. [20] Gentzen, G. 1934/1935: “Untersuchungen über das logische Schließen. I”, Mathematische Zeitschrift 39, 176–210, 405–31. [21] Gupta, A. 2021: “Definitions”, The Stanford Encyclopedia of Philosophy (Winter 2021 Edition), E. N. Zalta (ed.), ⟨https://plato.stanford.edu/archives/win2021/entries/definitions/⟩. [22] Halbach, V. 2015: The Logic Manual, Oxford: Oxford University Press. [23] Harris, J. H. 1982: “What’s So Logical About The “Logical” Axioms?”, Studia Logica 41/2–3, 159–71. [24] Henkin, L., A. Tarski, I. Németi, J. D. Monk, H. Andréka. 1981: Cylindric Set Algebras, Berlin: Springer. [25] Hilbert, D. and P. Bernays. 1968: Grundlagen der Mathematik I, Second Edition, Berlin: Springer. [26] Hlobil, H. and R. Brandom. 2024: Reasons for Logic, Logic for Reasons: Pragmatics, Semantics, and Conceptual Roles, London: Routledge. [27] Humberstone, L. 2011: The Connectives, Cambridge, Mass.: The MIT Press. [28] Incurvati, L. and J. J. Schlöder. 2023: Reasoning with Attitude. Foundations and Applications of Inferential Expressivism, Oxford: Oxford University Press. [29] Jacinto, B. and S. Read. 2017: “General-Elimination Stability”, Studia Logica 105, 361–405. [30] Koslow, A. 1992: A Structuralist Theory of Logic, Cambridge: Cambridge University Press. 53 [31] Leitgeb, H. 2023: “Ramsification and Semantic Indeterminacy”, Review of Symbolic Logic 16/3, 900–50. [32] Leitgeb, H., E. N. Zalta, and U. Nodelman. 2025: “A Defense of Logicism”, The Bulletin of Symbolic Logic 31/1, 88–152. [33] Lewis, D. 1970: “How to Define Theoretical Terms”, The Journal of Philosophy 67/13, 427-46. [34] Löwenheim, L. 1915: “Über Möglichkeiten im Relativkalkül”, Mathematische Annalen 76/4, 447–70. [35] McGee, V. 2015: “The Categoricity of Logic”, in: C. R. Caret and O. T. Hjortland (eds.), Foundations of Logical Consequence, Oxford: Oxford University Press, 160-85. [36] Milne, P. 2015: “Inversion Principles and Introduction Rules”, in: H. Wansing (ed.), Dag Prawitz on Proofs and Meaning, Outstanding Contributions to Logic, Vol 7. Cham: Springer, 189–224. [37] Murzi, J. 2020: “Classical Harmony and Separability”, Erkenntnis 85, 391– 415. [38] Murzi, J. and O. T. Hjortland. 2009: “Inferentialism and the Categoricity Problem: Reply to Raatikainen”, Analysis 69/3, 480–8. [39] Murzi, J. and F. Steinberger. 2017: “Inferentialism”, in: B. Hale, C. Wright, and A. Miller (eds.), A Companion to the Philosophy of Language, Wiley Blackwell, 197–224. [40] Murzi, J. and B. Topey. 2021: “Categoricity by Convention”, Philosophical Studies 178/10, 3391–420. [41] Popper, K. R. 1946–1947: “Logic without Assumptions”, Proceedings of the Aristotelian Society 47, 251–92. Reprinted in Binder, Piecha, and SchroederHeister (2022), 83–112. [42] Popper, K. R. 1948: “On the Theory of Deduction, Part II. The Definitions of Classical and Intuitionist Negation”, in: Koninklijke Nederlandse Akademie van Wetenschappen, Proceedings of the Section of Sciences 51, 322–31. Reprinted in Binder, Piecha, and Schroeder-Heister (2022), 181–92. [43] Prawitz, D. 1965: Natural Deduction: A Proof-Theoretical Study, Mineola, N.Y.: Dover Publications. 54 [44] Prior, A. N. 1960: “The Runabout Inference-Ticket”, Analysis 21/2, 38–9. [45] Raatikainen, P. 2008: “On Rules of Inference and the Meanings of Logical Constants”, Analysis 68/4, 282-.7. [46] Read, S. 2000: “Harmony and Autonomy in Classical Logic”, Journal of Philosophical Logic 28, 123–54. [47] Read, S. 2010: “General-Elimination Harmony and the Meaning of the Logical Constants”, Journal of Philosophical Logic 39, 557–76. [48] Read, S. 2015: “Proof-Theoretic Validity”, in: C. Caret and O. Hjortland (eds.), Foundations of Logical Consequence, Oxford: Oxford University Press, 136–58. [49] Ripley, D. 2015: “Anything Goes”, Topoi 34, 25–36. [50] Rumfitt, I. 2017: “Against Harmony”. In: B. Hale, C. Wright, and A. Miller (eds.), The Blackwell’s Companion to the Philosophy of Language, 2nd edition, Vol. I, Oxford: Wiley Blackwell, 225–49. [51] Russell, B. 1903: The Principles of Mathematics, Cambridge: Cambridge University Press. [52] Schroeder-Heister, P. 1984: “A Natural Extension of Natural Deduction”, Journal of Symbolic Logic 49, 1284–99. [53] Schroeder-Heister, P. 1991: “Uniform Proof-Theoretic Semantics for Logical Constants (Abstract)”, Journal of Symbolic Logic 56, 1142. [54] Schroeder-Heister, P. 2007: “Generalized Definitional Reflection and the Inversion Principle”, Logica Universalis 1, 355–76. [55] Schroeder-Heister, P. 2024: “Proof-Theoretic Semantics”, The Stanford Encyclopedia of Philosophy (Spring 2024 Edition), E. N. Zalta and U. Nodelman (eds.), ⟨https://plato.stanford.edu/archives/spr2024/entries/proof-theoreticsemantics/⟩. [56] Shapiro, S. 1991: Foundations without Foundationalism, Oxford: Oxford University Press. [57] Sher, G. 1991: The Bounds of Logic. A Generalized Viewpoint, Cambridge, MA: The MIT Press. 55 [58] Skolem, T. 1919: “Untersuchungen über die Axiome des Klassenkalküls”, Vid. Skrifter I, Math.-nat. Klasse Nr 3. [59] Steinberger, F. 2011: “What Harmony Could and Could Not Be”, Australasian Journal of Philosophy 89/4: 617–39. [60] Steinberger, F. and J. Murzi. 2017: “Inferentialism”, in: B. Hale, C. Wright, and A. Miller (eds.) Blackwell Companion to Philosophy of Language, Oxford: Wiley Blackwell, Vol. 1, Second Edition, 197–224. [61] Suppes, P. 1957: Introduction to Logic, New York: Van Nostrand Reinhold Company. [62] Tarski, A. 1944: “The Semantic Conception of Truth: And the Foundations of Semantics”, Philosophy and Phenomenological Research 4/3: 341–76. [63] Tennant, N. 2020: “Inferentialism, Logicism, Harmony, and a Counterpoint”, in: A. Miller (ed.), Logic, Language and Mathematics: Themes from the Philosophy of Crispin Wright Oxford: Oxford University Press, 223-47. [64] Tharp, L. H. 1973: “The Characterization of Monadic Logic”, The Journal of Symbolic Logic 38/3, 481–88. [65] Tranchini, L., P. Pistone, and M. Petrolo. 2019: “The Naturality of Natural Deduction”, Studia Logica 107, 195–231. [66] Troelstra, A. S. and H. Schwichtenberg. 2000: Basic Proof Theory, Second Edition, Cambridge: Cambridge University Press. [67] Väänänen, J. and T. Wang. 2015: “Internal Categoricity in Arithmetic and Set Theory”, Notre Dame Journal of Formal Logic 56/1, 121–34. [68] Väänänen, J. 2021: “Second-Order and Higher-Order Logic”, in: E. N. Zalta (ed.), The Stanford Encyclopedia of Philosophy (Fall 2021 Edition), ⟨https://plato.stanford.edu/archives/fall2021/entries/logic-higher-order/⟩. [69] Van Benthem, J. 1989: “Logical Constants Across Varying Types”, Notre Dame Journal of Formal Logic 30/3, 315–342. [70] Van Benthem, J. 2017: “Logical Constants: The Variable Fortunes of an Elusive Notion”, in: W. Sieg, R. Sommer, and C. Talcott (Eds.), Reflections on the Foundations of Mathematics. Essays in Honor of Sol Feferman, Lecture Notes in Logic 15, Cambridge: Cambridge University Press, 426–46. 56 [71] Van Dalen, D. 2013: Logic and Structure, Fifth Edition, London: Springer. [72] Woods, J. Unpublished: “Modest Inferentialism for Classical Logic”, unpublished draft. [73] Zalta, E. N. 2020: “Typed Object Theory”, in: J. L. Falguera and C. Martı́nez-Vidal (eds.), Abstract Objects: For and Against, Synthese Library Vol. 422, Cham: Springer, 59–88. [74] Zucker, J. I. and R. S. Tragesser. 1978: “The Adequacy Problem for Inferential Logic”, Journal of Philosophical Logic 7, 501–16. 8 Appendix: Rule Systems as Third-Order Definitions The translation of rule systems into second-order definitions that has been the focus of this paper could be generalized by allowing translation images to be third-order statements. In this way, classical rules systems that are analytic but do not define their operators according to the second-order Translation Criterion from Section 3 could end up defining their operators after all. For instance, let us reconsider the classical natural deduction system Rcn for negation (recall Section 5): Γ, ¬A ⊢ B ∆, ¬A ⊢ ¬B Γ, ∆ ⊢ A Γ, A ⊢ B ∆, A ⊢ ¬B Γ, ∆ ⊢ ¬A This system was found to be not definitional as it is not simple: one and the same rule includes different applications of ¬ to different metavariables (¬A, ¬B), which contrasts with an explicit definition including just one X to be characterized by its definiens. In the present case, that X could either be N eg(A) or N eg(B) but not both of them simultaneously. However, if the relevant X is no longer assumed to be a second-order proposition N eg(A) (as in: N eg(A) = X ↔ . . .) but rather a third -order function N eg (as in: N eg = X ↔ . . .), applications of the same function variable X to different second-order variables in the definiens become unproblematic from the viewpoint of the standard theory of definitions. Hence, Rcn from above may be translated into the following third -order explicit definition of N eg that involves third -order quantification over functions X from propositions to propositions: 57 Def. 19 ∀X : N eg = X ↔ 1. ∀A, B, G, D: ∀w(G(w) ∧ A(w) → B(w)) ∧ ∀w(D(w) ∧ A(w) → X (B)(w)) → ∀w(G(w) ∧ D(w) → X (A)(w)), 2. ∀A, B, G, D: ∀w(G(w) ∧ X (A)(w) → B(w)) ∧ ∀w(D(w) ∧ X (A)(w) → X (B)(w)) → ∀w(G(w) ∧ D(w) → A(w)). This follows to be a definition again by its corresponding unique-existence claim being logically true, the only difference being that the relevant notion of logical truth is now that of third -order logic. However, this rise of complexity comes with a price, and not just logically (with the commitment to third-order logic) and ontologically (with the commitment to functions of propositions rather than just propositions) but also conceptually: where the second-order definition N eg(A) = X ↔ . . . only requires one to understand N eg(A) to be the very proposition that matches the inferential role of ¬A, the third-order definition N eg = X ↔ . . . requires one to understand N eg to be the very function that maps propositions to propositions in a manner that matches the inferential role of ¬. While the second-order definition of negation only involves one step “downwards” from propositions to worlds, the third-order definition of negation also involves a step “upwards” to functions over propositions. Although the Translation Criterion is obviously not in the business of describing or explaining how the meaning of logical operators is actually understood from their use, it is still meant to be a rational reconstruction thereof, and as such it ought to bear some similarity, to some extent, to what it reconstructs. And it seems at least doubtful that one actually needs to grasp the notion of an arbitrary function X on propositions in order to understand a propositional logical operator, such as negation. Indeed, the previous sections demonstrated that it is possible to define the (second-order counterparts of the) usual operators of classical first-order logic by strictly second-order means. Furthermore, the reconstruction of logical inferentialism in terms of the translation of rules into third-order definitions would simply gloss over all subtle differences between definitional intuitionistic rule systems and analytic classical ones, such as for negation. For these reasons, I submit that the more plausible rational reconstruction of first-order logical operators is by second-order definition, 58 since it remains closer to our pre-theoretic understanding of these operators, and it stays in line with other attempts at second-order characterizations of first-order theoretical concepts from mathematics and science (see e.g. Carnap 1959, Lewis 1970, Leitgeb 2023, De Benedetto and La Rosa. 2024, and Leitgeb, Nodelman, and Zalta 2025). 59