In a recent paper, under the auspices of an unorthodox variety of bilateralism, we introduced a new kind of proof-theoretic semantics for the base modal logic \(\mathbf{K}\), whose values lie in the closed interval \([0,1]\) of rational numbers [14]. In this paper, after clarifying our conception of bilateralism – dubbed “soft bilateralism” – we generalize the fractional method to encompass extensions and weakenings of \(\mathbf{K}\). Specifically, we introduce well-behaved hypersequent calculi for the deontic logic \(\mathbf{D}\) and the non-normal modal logics (...) \(\mathbf{E}\) and \(\mathbf{M}\) and thoroughly investigate their structural properties. (shrink)

The problem of negative truth is the problem of how, if everything in the world is positive, we can speak truly about the world using negative propositions. A prominent solution is to explain negation in terms of a primitive notion of metaphysical incompatibility. I argue that if this account is correct, then minimal logic is the correct logic. The negation of a proposition A is characterised as the minimal incompatible of A composed of it and the logical constant ¬. A (...) rule based account of the meanings of logical constants that appeals to the notion of incompatibility in the introduction rule for negation ensures the existence and uniqueness of the negation of every proposition. But it endows the negation operator with no more formal properties than those it has in minimal logic. (shrink)

This paper presents rules of inference for a binary quantifier I for the formalisation of sentences containing definite descriptions within intuitionist positive free logic. I binds one variable and forms a formula from two formulas. Ix[F, G] means ‘The F is G’. The system is shown to have desirable proof-theoretic properties: it is proved that deductions in it can be brought into normal form. The discussion is rounded up by comparisons between the approach to the formalisation of definite descriptions recommended (...) here and the more usual approach that uses a term-forming operator ι, where ιxF means ‘the F’. (shrink)

This paper studies a formalisation of intuitionistic logic by Negri and von Plato which has general introduction and elimination rules. The philosophical importance of the system is expounded. Definitions of ‘maximal formula’, ‘segment’ and ‘maximal segment’ suitable to the system are formulated and corresponding reduction procedures for maximal formulas and permutative reduction procedures for maximal segments given. Alternatives to the main method used are also considered. It is shown that deductions in the system convert into normal form and that deductions (...) in normal form have the subformula property. (shrink)

General-elimination harmony articulates Gentzen’s idea that the elimination-rules are justified if they infer from an assertion no more than can already be inferred from the grounds for making it. Dummett described the rules as not only harmonious but stable if the E-rules allow one to infer no more and no less than the I-rules justify. Pfenning and Davies call the rules locally complete if the E-rules are strong enough to allow one to infer the original judgement. A method is given (...) of generating harmonious general-elimination rules from a collection of I-rules. We show that the general-elimination rules satisfy Pfenning and Davies’ test for local completeness, but question whether that is enough to show that they are stable. Alternative conditions for stability are considered, including equivalence between the introduction- and elimination-meanings of a connective, and recovery of the grounds for assertion, finally generalizing the notion of local completeness to capture Dummett’s notion of stability satisfactorily. We show that the general-elimination rules meet the last of these conditions, and so are indeed not only harmonious but also stable. (shrink)

This paper deals with the question of the logicality of modal logics from a proof-theoretic perspective. It is argued that if Dos̆en’s analysis of logical constants as punctuation marks is embraced, it is possible to show that all the modalities in the cube of normal modal logics are indeed logical constants. It will be proved that the display calculus for each displayable modality admits a purely structural presentation based on double-line rules which, following Dos̆en’s analysis, allows us to claim that (...) the corresponding modal operators are logical constants. (shrink)

Arguments, the story goes, have one or more premises and only one conclusion. A contentious generalisation allows arguments with several disjunctively connected conclusions. Contentious as this generalisation may be, I will argue nevertheless that it is justified. My main claim is that multiple conclusions are epiphenomena of the logical connectives: some connectives determine, in a certain sense, multiple-conclusion derivations. Therefore, such derivations are completely natural and can safely be used in proof-theoretic semantics.

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)

This paper considers proof-theoretic semantics for necessity within Dummett's and Prawitz's framework. Inspired by a system of Pfenning's and Davies's, the language of intuitionist logic is extended by a higher order operator which captures a notion of validity. A notion of relative necessary is defined in terms of it, which expresses a necessary connection between the assumptions and the conclusion of a deduction.

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)