Pedro del Valle-Inclán

According to inferentialists the meaning of logical vocabulary is given by the rules of inference governing its use. In response to a challenge posed by Arthur Prior, inferentialists have typically argued that not all sets of rules can define a connective. The project of determining which sets of rules are acceptable definitions has come to be known as the project of finding a criterion of proof-theoretic harmony. One of the best-known proposals is Neil Tennant’s. His criterion of harmony relies on the notions of the strength of a proposition and the strength of a rule. In this note, I argue that Tennant’s appeal to the notion of the strength of a rule gives rise to problems that make his account unsustainable. I also argue that the sort of consideration that gets Tennant into trouble applies, more generally, to other so-called ‘local’ accounts of harmony, and casts doubts on the idea that we can uniquely determine the harmonious counterpart of a given set of rules.

In a recent paper del Valle-Inclan and Schlöder argue that bilateral calculi call for their own notion of proof-theoretic harmony, distinct from the usual (or ‘unilateral’) ones. They then put forward a specifically bilateral criterion of harmony, and present a harmonious bilateral calculus for classical logic. In this paper, I show how del Valle-Inclan and Schlöder’s criterion of harmony suggests a notion of normal form for bilateral systems, and prove normalisation for two (harmonious) bilateral calculi for classical logic, HB1 and HB2. The resulting normal derivations have the usual desirable features, like the separation and subformula properties. HB1-normal form turns out to be strictly stronger that the notion of normal form proposed by Nils Kürbis, and HB2-normal form is neither stronger nor weaker than a similar proposal by Marcello D’Agostino, Dov Gabbay, and Sanjay Modgyl.

In his Formalization of Logic (1943) Carnap pointed out that there are non-normal interpretations of classical logic: non-standard interpretations of the connectives and quantifiers that are consistent with the classical consequence relation of a language. Different ways around the problem have been proposed. In a recent paper, Bonnay and Westerståhl argue that the key to a solution is imposing restrictions on the type of interpretation we take into account. More precisely, they claim that if we restrict attention to interpretations that are (a) compositional, (b) non-trivial and (c) in the case of the quantifiers, invariant under permutations of the domain, Carnap’s Problem is avoided. This paper has two goals. The first is to show that Bonnay and Westerståhl’s solution to Carnap’s Problem doesn’t work. The second is to argue that something similar to their proposal seems to do the job. The problems with Bonnay and Westerståhl’s approach trace back to issues concerning the (un)definability of subsets of the domain of first-order structures, as well as to the compositionality of first-order languages. After expanding on these problems, I’ll propose a way to modify Bonnay and Westerståhl’s account and solve Carnap’s Problem.

Ian Rumfitt (2000) developed a bilateralist account of logic in which the meaning of the connectives is given by conditions on asserted and rejected sentences. An additional set of inference rules, the coordination principles, determines the interaction of assertion and rejection. Fernando Ferreira (2008) found this account defective, as Rumfitt must state the coordination principles for arbitrary complex sentences. Rumfitt (2008) has a reply, but we argue that the problem runs deeper than he acknowledges and is in fact related to the challenge of establishing proof-theoretic harmony. We motivate a distinctively bilateral criterion for harmony and show how the bilateralist can meet it. This also resolves Ferreira's complaint.