Search

In this paper we elaborate a conception of entailment based on what we call the Ackermann principle, which explicates valid entailment through a logical connection between (sets of) sentences depending on their informational content. We reconstruct Dunn’s informational semantics for entailment on the basis of Restall’s approach, with assertion and denial as two independent (primary) speech acts, by introducing the notion of a ‘position description’. We show how the machinery of position descriptions can effectively be used to define the positive and the negative information carried by sentences of a given language and to present a formalized version of the Ackermann principle as an inclusion relationship between the informational contents of the conclusions and the premises of a valid entailment. Being so interpreted, the entailment relation exhibits certain properties, including the property of transitivity (and, more generally, admissibility of the cut rule). Whereas properties such as Anderson and Belnap’s variable sharing property or Parry’s proscriptive principle are normally presented as imposing a relevance requirement on valid entailment, the suggested formalization of the Ackermann principle supports all of Gentzen’s structural rules, including weakening, a rule that is normally given up in sequent-style proof systems for relevance logics. In this way we propose an Ackermann-inspired explication of the nature of entailment as a relation between the informational contents of sentences.

In this paper, we shall consider the so-called cancellation view of negation and the inferential role of contradictions. We will discuss some of the problematic aspects of negation as cancellation, such as its original presentation by Richard and Valery Routley and its role in motivating connexive logic. Furthermore, we will show that the idea of inferential ineffectiveness of contradictions can be conceptually separated from the cancellation model of negation by developing a system we call qLPm, a combination of Graham Priest’s minimally inconsistent Logic of Paradox with q-entailment (quasi-entailment) as introduced by Grzegorz Malinowski.

In this paper we consider logical inference as an activity that results in proofs and hence produces knowledge. We suggest to merge the semantical analysis of deliberatively seeing-to-it-that from stit theory (Belnap et al. in Facing the future: agents and choices in our indeterminist world, Oxford University Press, New York, 2001) and the semantics of the epistemic logic with justification from (Artemov and Nogina in Journal of Logic and Computation 15:1059–1073, 2005). The general idea is to understand proving that A as seeing to it that a proof of A is (publicly) available. We introduce a semantics of various notions of proving as an activity and present a number of valid principles that relate the various notions of proving to each other and to notions of justified knowledge, implicit knowledge, and possibility. We also point out and comment upon certain principles our semantics fails to validate.

Justification stit logic is a logic for reasoning about proving as a certain kind of activity, namely seeing to it that a proof is publicly available. It merges the semantical analysis of deliberatively seeing-to-it-that from stit theory (Belnap, Perloff, Xu 2001) and the semantics of the epistemic logic with justification from (Artemov and Nogina 2005). In this paper, after recalling its language and basic semantical definitions, various ramifications and refinements of justification stit logic are presented and discussed: imposing natural restrictions upon the class of models under consideration, making use of modalities that assert the existence of a proof, introducing a variant of justification stit logic based on a semantics introduced by M. Fitting, and adding variable-binding operators and extending the set of proof polynomials.

In this paper it is suggested to generalize our understanding of general (structural) proof theory and to consider it as a general theory of two kinds of derivations, namely proofs and dual proofs. The proposal is substantiated by (i) considerations on assertion, denial, and bi-lateralism, (ii) remarks on compositionality in proof-theoretic semantics, and (iii) comments on falsification and co-implication. The main formal result of the paper is a normal form theorem for the natural deduction proof system N2Int of the bi-intuitionistic logic 2Int. The proof makes use of the faithful embedding of 2Int into intuitionistic logic with respect to validity and shows that conversions of dual proofs can be sidestepped.

In this paper it is suggested to generalize our understanding of general (structural) proof theory and to consider it as a general theory of two kinds of derivations, namely proofs and dual proofs. The proposal is substantiated by (i) considerations on assertion, denial, and bi-lateralism, (ii) remarks on compositionality in proof-theoretic semantics, and (iii) comments on falsification and co-implication. The main formal result of the paper is a normal form theorem for the natural deduction proof system N2Int of the bi-intuitionistic logic 2Int. The proof makes use of the faithful embedding of 2Int into intuitionistic logic with respect to validity and shows that conversions of dual proofs can be sidestepped.

In this introduction, we offer an overview of main systems developed in the growing literature on connexive logic, and also point to a few topics that seem to be collecting attention of many of those interested in connexive logic. We will also make clear the context to which the papers in this special issue belong and contribute.

In this paper, first some propositional conditional logics based on Belnap and Dunn’s useful four-valued logic of first-degree entailment are introduced semantically, which are then turned into systems of weakly and unrestrictedly connexive conditional logic. The general frame semantics for these logics makes use of a set of allowable (or admissible) extension/antiextension pairs. Next, sound and complete tableau calculi for these logics are presented. Moreover, an expansion of the basic conditional connexive logics by a constructive implication is considered, which gives an opportunity to discuss recent related work, motivated by the combination of indicative and counterfactual conditionals. Tableau calculi for the basic constructive connexive conditional logics are defined and shown to be sound and complete with respect to their semantics. This semantics has to ensure a persistence property with respect to the preorder that is used to interpret the constructive implication.

The present note contains a critical discussion of the methodology of paraconsistent logic in general and “the central optimisation problem of paraconsistent logics” in particular. It is argued that there exist several reasons not to consider classical logic as the reference logic for developing systems of paraconsistent logic, and it is suggested to weaken a certain maximality condition that may be seen as essential for “optimisation”, which is a methodology in the tradition of Newton da Costa. It is argued that the guiding motivation for the development of paraconsistent logics should be neither epistemological nor ontological, but informational. Moreover, it is pointed out that there are other notions of maximality and other methodologies. A methodology due to Graham Priest and Richard Routley and another methodology that focuses on a minimal shrinkage of expressiveness relative to a given reference logic are considered in some detail.

In this paper, three systems of constructive and inconsistency-tolerant description logic are motivated and defined semantically. Moreover, sound and complete tableau calculi for these systems are presented.

Building on work by Schild, De Giacomo and Lenzerini, we establish a tight connection between description logics and hybrid logics. The main aim of the paper is to provide a modal perspective on some of the distinguishing features of description logic. In particular, by working in a hybrid logic setting we are able to develop a model-theoretic understanding of both assertional and terminological information. We also show how to use the connection between description and hybrid logics to transfer results on complexity and expressive power from one to the other.

This chapter surveys the application of various kinds of sequent systems to modal and temporal logic, also called tense logic. The starting point are ordinary Gentzen sequents and their limitations both technically and philosophically. The rest of the chapter is devoted to generalizations of the ordinary notion of sequent. These considerations are restricted to formalisms that do not make explicit use of semantic parameters like possible worlds or truth values, thereby excluding, for instance, Gabbay’s labelled deductive systems, indexed tableau calculi, and Kanger-style proof systems from being dealt with. Readers interested in these types of proof systems are referred to [Gabbay, 1996], [Gore, 1999] and [Pliuskeviene, 1998]. Also Orlowska’s [1988; 1996] Rasiowa-Sikorski-style relational proof systems for normal modal logics will not be considered in the present chapter. In relational proof systems the logical object language is associated with a language of relational terms. These terms may contain subterms representing the accessibility relation in possible-worlds models, so that semantic information is available at the same level as syntactic information. The derivation rules in relational proof systems manipulate finite sequences of relational formulas constructed from relational terms and relational operations. An overview of ordinary sequent systems for non-classical logics is given in [Ono, 1998], and for a general background on proof theory the reader may consult [Troelstra and Schwichtenberg, 2000].

In the present chapter it is shown that every displayable logic enjoys strong cut-elimination. This result sharpens Belnap’s very general cut-elimination theorem for Display Logic [16]. Moreover, Kracht’s characterization of the properly displayable modal and tense logics is presented, together with complete and cut-free display sequent systems for various axiomatic extensions of the basic intensional systems K and Kt.

The aim of this chapter is twofold. First of all, we shall take a closer look at the strong, constructive negation ~ introduced in Chapter 8. We shall consider ~ from the point of view of a proof-theoretic characterization of negation and argue that negation may be seen as a connecting link between provability and disprovability (refutability). This notion of negation as falsity will be developed against the background of N. Tennant’s [165] considerations of negation in intuitionistic relevant logic, where Tennant also attends to disproofs in addition to proofs. It is shown that negation in intuitionistic relevant logic is a negation as syntactical inconsistency in the sense of Gabbay [66], and that every such negation as inconsistency is a negation as falsity, while the converse is not true. Secondly, we shall consider semantics-based nonmonotonic reasoning as introduced by, again, Gabbay [65]. In this approach, nonmonotonic inference is defined using a modal consistency operator that is interpreted as possibility with respect to the information order in semantical models of a monotonic base logic. It will be shown that certain anomalies of Gabbay’s approach can very naturally be avoided using David Nelson’s constructive three-valued system N3 [119] as the monotonic base system instead of intuitionistic logic, IPL or Kleene’s three-valued logic, 3. The counterintuitive features of semantics-based nonmonotonic reasoning based on IPL or on 3 also disappear if certain properties of the information order in Kripke models for IPL and model structures for 3 are given up. In the case of IPL this leads to subintuitionistic logics. In this way, the present chapter prepares the ground for Chapter 10. Whereas Chapter 10 is devoted to display sequent calculi for subintuitionistic logics, [195] solves the problem of providing a sound and complete proof-system for the modal logic of consistency over Nelson’s four-valued logic N4.

As we have seen in Chapter 2, the study of nonclassical and modal logics has led to the development of many generalizations of the ordinary notion of sequent. In view of the diversity of these types of proof systems it becomes increasingly important to investigate their interrelations and their advantages and disadvantages. In this chapter, we shall consider the relation between display logic and the method of hypersequents independently introduced by G. Pottinger [134] and A. Avron [7]. It will be shown that hypersequents can be simulated by display sequents. Whereas hypersequents are finite sequences of ordinary sequents, display sequents are obtained by enriching the structural language of sequents, thus turning the antecedent and the succedent of a sequent into ‘Gentzen terms’, see also [41]. As Avron [12, p. 3] points out, “although a hypersequent is certainly a more complex data structure than an ordinary sequent, it is not much more complicated, and goes in fact just one step further”. The translation of hypersequents into display sequents illuminates how display sequents generalize ordinary sequents still further than hypersequents. In contradistinction to the application of hypersequents to modal logics, the modal display calculus comprises introduction rules for the modal and tense logical operators which can arguably be interpreted as meaning assignments; see Chapter 1. Therefore the translation of hypersequents into display sequents has something to recommend preferring display logic over the hypersequential formalism. We shall consider three case-studies of translating hypersequents into display sequents, corresponding with three different interpretations of hypersequents in [12].

In what follows we shall use display logic to define a proof-theoretic semantics in terms of general introduction schemata. It will be shown that with respect to this semantics the set of connectives {[F], [P], ∧, ¬} is functionally complete for every displayable normal propositional tense logic and the set of connectives {[F], ∧, ¬} is functionally complete for every displayable normal propositional modal logic. It seems that there exists no other proof-theoretic characterization of modal operators (apart from intuitionistic implication ⊃ h ) in the literature.

In this paper we discuss Gabbay's idea of basing nonmonotonic deduction on semantic consequence in intuitionistic logic extended by a consistency operator and Turner's suggestion of replacing the intuitionistic base system by Kleene's three-valued logic. It is shown that a certain counterintuitive feature of these approaches can be avoided by using Nelson's constructive logic N instead of intuitionistic logic or Kleene's system. Moreover, in N a more general notion of consistency can be defined and nonmonotonic deduction can thus be based on a logical system satisfying the Deduction Theorem.