Proof-theoretic semantics is an inferentialist theory of meaning originally developed in a unilateral framework. Its extension to bilateral systems opens both opportunities and problems. The problems are caused especially by Coordination Principles (a kind of rule that is not present in unilateral systems) and mismatches between rules for assertion and rules for rejection. In this paper, a solution is proposed for two major issues: the availability of a reduction procedure for tonk and the existence of harmonious rules for the paradoxical (...) zero-ary connective \(\bullet\). The solution is based on a reinterpretation of bilateral rules as complex rules, that is, rules that introduce or eliminate connectives in a subordinate position. Looking at bilateral rules from this perspective, the problems faced by bilateralism can be seen as special cases of general problems of complex systems, which have been already analyzed in the literature. In the end, a comparison with other proposed solutions underlines the need for further investigation in order to complete the picture of bilateral proof-theoretic semantics. (shrink)

The connectives of classical propositional logic are given an analysis in terms of necessary and sufficient conditions of acceptance and rejection, i.e. the connectives are analyzed within an expressivist bilateral meaning-is-use framework. It is explained how such a framework differs from standard inferentialist frameworks and it is argued that it is better suited to address the particular issues raised by the expressivist thesis that the meaning of a sentence is determined by the mental state that it is conventionally used to (...) express. Furthermore, it is shown that the classical requirements governing the connectives completely characterize classical logic, are conservative and separable, are in bilateral harmony, are structurally preservative with respect to the classical coordination requirements and resolve the categoricity problem. These results are taken to show that one can give an expressivist bilateral meaning-is-use analysis of the connectives that confer on them a determinate coherent classical interpretation. (shrink)

In this paper we will consider the existing notions of bilateralism in the context of proof-theoretic semantics and propose, based on our understanding of bilateralism, an extension to logical multilateralism. This approach differs from what has been proposed under this name before in that we do not consider multiple speech acts as the core of such a theory but rather multiple consequence relations. We will argue that for this aim the most beneficial proof-theoretical realization is to use sequent calculi with (...) multiple sequent arrows satisfying some specific conditions, which we will lay out in this paper. We will unfold our ideas with the help of a case study in logical tetralateralism and present an extension of Almukdad and Nelson’s propositional constructive four-valued logic by unary operations of meaningfulness and nonsensicality. We will argue that in sequent calculi with multiple sequent arrows it is possible to maintain certain features that are desirable if we assume an understanding of the meaning of connectives in the spirit of proof-theoretic semantics. The use of multiple sequent arrows will be justified by the presence of congruentiality-breaking unary connectives. (shrink)

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. (shrink)

Stephen Read presented harmonious inference rules for identity in classical predicate logic. I demonstrate here how this approach can be generalised to a setting where predicate logic has been extended with epistemic modals. In such a setting, identity has two uses. A rigid one, where the identity of two referents is preserved under epistemic possibility, and a non-rigid one where two identical referents may differ under epistemic modality. I give rules for both uses. Formally, I extend Quantified Epistemic Multilateral Logic (...) with two identity signs. I argue that a uniform meaning for identity tout court can be given by adopting Maria Aloni’s account of reference using conceptual covers. We obtain a harmonious set of rules for identity that is sound and complete for Aloni’s model theory. (shrink)

I explain why Fernando Ferreira's interesting formal result does not threaten the bilateralist account of the sense of the connectives.

This paper discusses proof-theoretic semantics, the project of specifying the meanings of the logical constants in terms of rules of inference governing them. I concentrate on Michael Dummett’s and Dag Prawitz’ philosophical motivations and give precise characterisations of the crucial notions of harmony and stability, placed in the context of proving normalisation results in systems of natural deduction. I point out a problem for defining the meaning of negation in this framework and prospects for an account of the meanings of (...) modal operators in terms of rules of inference. (shrink)

Ian Rumfitt has proposed systems of bilateral logic for primitive speech acts of assertion and denial, with the purpose of ‘exploring the possibility of specifying the classically intended senses for the connectives in terms of their deductive use’ : 810f). Rumfitt formalises two systems of bilateral logic and gives two arguments for their classical nature. I assess both arguments and conclude that only one system satisfies the meaning-theoretical requirements Rumfitt imposes in his arguments. I then formalise an intuitionist system of (...) bilateral logic which also meets those requirements. Thus Rumfitt cannot claim that only classical bilateral rules of inference succeed in imparting a coherent sense onto the connectives. My system can be extended to classical logic by adding the intuitionistically unacceptable half of a structural rule Rumfitt uses to codify the relation between assertion and denial. Thus there is a clear sense in which, in the bilateral framework, the difference between classicism and intuitionism is not one of the rules of inference governing negation, but rather one of the relation between assertion and denial. (shrink)

In bilateral systems for classical logic, assertion and denial occur as primitive signs on formulas. Such systems lend themselves to an inferentialist story about how truth-conditional content of connectives can be determined by inference rules. In particular, for classical logic there is a bilateral proof system which has a property that Carnap in 1943 called categoricity. We show that categorical systems can be given for any finite many-valued logic using $n$-sided sequent calculus. These systems are understood as a further development (...) of bilateralism—call it multilateralism. The overarching idea is that multilateral proof systems can incorporate the logic of a variety of denial speech acts. So against Frege we say that denial is not the negation of assertion and, with Mark Twain, that denial is more than a river in Egypt. (shrink)

In this short paper I note that a key metatheorem does not hold for the bilateralist inferential framework: harmony does not entail consistency. I conclude that the requirement of harmony will not suffice for a bilateralist to maintain a proof theoretic account of classical logic. I conclude that a proof theoretic account of meaning based on the bilateralist framework has no natural way of distinguishing legitimate definitional inference rules from illegitimate ones (such as those for tonk). Finally, as an appendix (...) to the main argument, I propose an alternative non-bilateral formal solution to the problem of providing a proof-theoretic account of classical logic. (shrink)

There is widespread agreement that while on a Dummettian theory of meaning the justified logic is intuitionist, as its constants are governed by harmonious rules of inference, the situation is reversed on Huw Price's bilateralist account, where meanings are specified in terms of primitive speech acts assertion and denial. In bilateral logics, the rules for classical negation are in harmony. However, as it is possible to construct an intuitionist bilateral logic with harmonious rules, there is no formal argument against intuitionism (...) from the bilateralist perspective. Price gives an informal argument for classical negation based on a pragmatic notion of belief, characterised in terms of the differences they make to speakers' actions. The main part of this paper puts Price's argument under close scrutiny by regimenting it and isolating principles Price is committed to. It is shown that Price should draw a distinction between A or ¬A making a difference. According to Price, if A makes a difference to us, we treat it as decidable. This material allows the intuitionist to block Price's argument. Abandoning classical logic also brings advantages, as within intuitionist logic there is a precise meaning to what it might mean to treat A as decidable: it is to assume A ∨ ¬A. (shrink)

Bilateralists hold that the meanings of the connectives are determined by rules of inference for their use in deductive reasoning with asserted and denied formulas. This paper presents two bilateral connectives comparable to Prior's tonk, for which, unlike for tonk, there are reduction steps for the removal of maximal formulas arising from introducing and eliminating formulas with those connectives as main operators. Adding either of them to bilateral classical logic results in an incoherent system. One way around this problem is (...) to count formulas as maximal that are the conclusion of reductio and major premise of an elimination rule and to require their removability from deductions. The main part of the paper consists in a proof of a normalisation theorem for bilateral logic. The closing sections address philosophical concerns whether the proof provides a satisfactory solution to the problem at hand and confronts bilateralists with the dilemma that a bilateral notion of stability sits uneasily with the core bilateral thesis. (shrink)

Bilateralism is a theory of meaning according to which assertion and denial are independent speech acts. Bilateralism also proposes two coordination principles for assertion and denial. I argue that if assertion and denial are independent speech acts, they cannot be coordinated by the bilateralist principles.