Trying to overcome Dugundji’s result on uncharacterisability of modal logics by finite logical matrices, Kearns and Ivlev proposed, independently, a characterisation of some modal systems by means of four-valued multivalued truth-functions , as an alternative to Kripke semantics. This constitutes an antecedent of the non-deterministic matrices introduced by Avron and Lev . In this paper we propose a reconstruction of Kearns’s and Ivlev’s results in a uniform way, obtaining an extension to another modal systems. The first part of the paper (...) is devoted to four-valued Nmatrices, including Kearns’s and Ivlev’s. Besides proving with full details Kearns’s results for T, S4 and S5, we also obtain a characterisation of the system B by four-valued Nmatrices with level valuations. Concerning Ivlev’s results, two new modal systems are introduced and char.. (shrink)

This paper briefly overviews some of the results and research directions. In the area of substructural logics from the last couple of decades. Substructural logics are understood here to include relevance logics, linear logic, variants of Lambek calculi and some other logics that are motivated by the idea of omitting some structural rules or making other structural changes in LK, the original sequent calculus for classical logic.

In classical game theory the idea that players randomize between their actions according to a particular optimal probability distribution has always been viewed as puzzling. In this paper, we establish a fundamental connection between n-person normal form games and quantum mechanics, which eliminates the conceptual problems of these random strategies. While the two theories have been regarded as distinct, our main theorem proves that if we do not give any other piece of information to a player in a game, than (...) the payoff matrix—the axiom of “no-supplementary data” holds—then the state of mind of a rational player is algebraically isomorphic to a pure quantum state. The “no supplementary data” axiom is captured in a Lukasiewicz’s three-valued Kripke semantics wherein statements about whether a strategy or a belief of a player is rational are initially indeterminate i.e. neither true, nor false. As a corollary, we show that in a mixed Nash equilibrium, the knowledge structure of a player implies that probabilities must verify the standard “Born rule” postulate of QM. The puzzling “indifference condition” wherein each player must be rationally indifferent between all the pure actions of the support of his equilibrium strategy is resolved by his state of mind being described by a “quantum superposition” prior a player is asked to make a definite choice in a “measurement”. Finally, these results demonstrate that there is an intrinsic limitation to the predictions of game theory, on a par with the “irreducible randomness” of quantum physics. (shrink)

Dugundji proved in 1940 that most parts of standard modal systems cannot be characterized by a single finite deterministic matrix. In the eighties, Ivlev proposed a semantics of four-valued non-deterministic matrices (which he called quasi-matrices), in order to characterize a hierarchy of weak modal logics without the necessitation rule. In a previous paper, we extended some systems of Ivlev’s hierarchy, also proposing weaker six-valued systems in which the (T) axiom was replaced by the deontic (D) axiom. In this paper, we (...) propose even weaker systems, by eliminating both axioms, which are characterized by eight-valued non-deterministic matrices. In addition, we prove completeness for those new systems. It is natural to ask if a characterization by finite ordinary (deterministic) logical matrices would be possible for all those Ivlev-like systems. We will show that finite deterministic matrices do not characterize any of them. (shrink)

Counterfactuals have become an important area of interdisciplinary interest, especially in logic, philosophy of language, epistemology, metaphysics, psychology, decision theory, and even artificial intelligence. In this study, we propose a new form of analysis for counterfactuals: analysis by algorithmic complexity. Inspired by Lewis-Stalnaker's Possible Worlds Semantics, the proposed method allows for a new interpretation of the debate between David Lewis and Robert Stalnaker regarding the Limit and Singularity assumptions. Besides other results, we offer a new way to answer the problems (...) raised by Goodman and Quine regarding vagueness, context-dependence, and the non- monotonicity of counterfactuals. Engaging in a dialogue with literature, this study will seek to bring new insights and tools to this debate. We hope our method of analysis can make counterfactuals more understandable in an intuitively plausible way, and a philosophically justifiable manner, aligned with the way we usually think about counterfactual propositions and our imaginative reasoning. (shrink)

An introduction to the special issue on epistemic logic and the foundations of game theory edited by Michael Bacharach and Philippe Mongin. Contributors are Michael Bacharach, Robert Stalnaker, Salvatore Modica and Aldo Rustichini, Luc Lismont and Philippe Mongin, and Hyun-Song Shin and Timothy Williamson.

This paper charts some early history of the possible worlds semantics for modal logic, starting with the pioneering work of Prior and Meredith. The contributions of Geach, Hintikka, Kanger, Kripke, Montague, and Smiley are also discussed.

A general game player automatically learns to play arbitrary new games solely by being told their rules. For this purpose games are specified in the general Game Description Language (GDL), a variant of Datalog with function symbols that uses a few game-specific keywords. A recent extension of basic GDL allows the description of nondeterministic games with any number of players who may have incomplete, asymmetric information. In this paper, we analyse the epistemic structure and expressiveness of this language in terms (...) of modal epistemic logic and prove two main results: (1) The operational semantics of GDL entails that the situation at any stage of a game can be characterised by a multi-agent epistemic (i.e., S5-) model; (2) GDL is sufficiently expressive to model any situation that can be described by a (finite) multi-agent epistemic model. (shrink)

Max Cresswell and Hilary Putnam seem to hold the view, often shared by classical logicians, that paraconsistent logic has not been made sense of, despite its well-developed mathematics. In this paper, I examine the nature of logic in order to understand what it means to make sense of logic. I then show that, just as one can make sense of non-normal modal logics (as Cresswell demonstrates), we can make `sense' of paraconsistent logic. Finally, I turn the tables on classical logicians (...) and ask what sense can be made of explosive reasoning. While I acknowledge a bias on this issue, it is not clear that even classical logicians can answer this question. (shrink)

The tableaux-constructions have a number of properties which advantageously distinguish them from equivalent axiomatic systems . The proofs in the form of tableaux-constructions have a full accordance with semantic interpretation and subformula property in the sense of Gentzen’s Hauptsatz. Method of tatleaux-construction gives a good substitute of Gentzen’s methods and thus opens a good perspective for the investigations of theoretical as well as applied aspects of logical calculi. It should be noted that application of tableau method in modal, tense, relevant (...) and other non-classical logics is connected with serious difficulties. Tableaux variants are constructed only for a few normal modal systems. As to relevant and paraconsistent logic, the absence of its tableau variants may be considered as a question of special interest. We shall formulate the tableaux for propositional modal system S4.1, S4.2, S4.3, S4.4 and relevant R∗ and E ∗ using Beth’s tableaux construction with indexed formulas. (shrink)

Herbrand disjunctions are a means for reducing the problem ofwhether a first-oder formula is valid in an open theory T or not to theproblem whether an open formula, one of the so called Herbrand disjunctions,is T -valid or not. Nevertheless, the set of Herbrand disjunctions, which hasto be examined, is undecidable in general. Fore this reason the practicalvalue of Herbrand disjunctions has been estimated negatively .Relying on completeness proofs which are based on the algebraizationtechnique presented in [30], but taking a (...) more optimistic view, we show howHerbrand disjunctions become the base of a method for building in theoriesinto automatic theorem provers [26]. Surveying newer results we discusshow to treat heterogeneous theories [29] as well as practical implications ofdifferent normal form transformations. (shrink)

In this paper, I propose that the distinction between what is at-issue and what is not can be modeled as a distinction between two components of assertion. These two components affect the common ground in different ways. The at-issue component of an assertion, which is negotiable, is treated as a proposal to update the common ground. The not-at-issue component of an assertion, which is not negotiable, is added directly to the common ground. Evidence for this proposal comes from evidentials, which (...) I argue grammaticize this distinction. It has been observed that sentences with evidentials make both an ‘evidential’ and a ‘propositional’ contribution (Faller 2002, 2006, Matthewson et al. 2008). The evidential contribution is not directly challengeable or up for negotiation. In contrast, the propositional contribution, the ‘main point’ of the sentence, is directly challengeable and up for negotiation. I analyze these two contributions of evidentials as the not-at-issue component of assertion and the at-issue component of assertion, respectively. Supporting data comes from Cheyenne, a language with evidentials that are part of the illocutionary mood paradigm. (shrink)

Many languages grammatically mark evidentiality, i.e., the source of information. In assertions, evidentials indicate the source of information of the speaker while in questions they indicate the expected source of information of the addressee. This dissertation examines the semantics and pragmatics of evidentiality and illocutionary mood, set within formal theories of meaning and discourse. The empirical focus is the evidential system of Cheyenne (Algonquian: Montana), which is analyzed based on several years of fieldwork by the author.

In Artemovʼs Justification Logic, one can make statements interpreted as “t is evidence for the truth of formula F.” We propose a variant of this logic in which one can say “I have degree r of confidence that t is evidence for the truth of formula F.” After defining both an axiomatic approach and a semantics for this Logic of Uncertain Justifications, we will prove the usual soundness and completeness theorems.

The completeness of the modal logic S4 for all topological spaces as well as for the real line , the n-dimensional Euclidean space and the segment etc. was proved by McKinsey and Tarski in 1944. Several simplified proofs contain gaps. A new proof presented here combines the ideas published later by G. Mints and M. Aiello, J. van Benthem, G. Bezhanishvili with a further simplification. The proof strategy is to embed a finite rooted Kripke structure for S4 into a subspace (...) of the Cantor space which in turn encodes . This provides an open and continuous map from onto the topological space corresponding to . The completeness follows as S4 is complete with respect to the class of all finite rooted Kripke structures. (shrink)

Dynamic topological logic provides a context for studying the confluence of the topological semantics for S4, topological dynamics, and temporal logic. The topological semantics for S4 is based on topological spaces rather than Kripke frames. In this semantics, □ is interpreted as topological interior. Thus S4 can be understood as the logic of topological spaces, and □ can be understood as a topological modality. Topological dynamics studies the asymptotic properties of continuous maps on topological spaces. Let a dynamic topological system (...) be a topological space X together with a continuous function f. f can be thought of in temporal terms, moving the points of the topological space from one moment to the next. Dynamic topological logics are the logics of dynamic topological systems, just as S4 is the logic of topological spaces. Dynamic topological logics are defined for a trimodal language with an S4-ish topological modality □ , and two temporal modalities, ○ and * , both interpreted using the continuous function f. In particular, ○ expresses f’s action on X from one moment to the next, and * expresses the asymptotic behaviour of f. (shrink)

Modus ponens provides the central theme. There are laws, of the form A→C. A logic L collects such laws. Any datum A provides input to the laws of L. The central ternary relation R relates theories L,T and U, where U consists of all of the outputs C got by applying modus ponens to major premises from L and minor premises from T. Underlying this relation is a modus ponens product operation on theories L and T, whence RLTU iff LTU. (...) These ideas have been expressed, especially with Routley, as worlds semantics for relevant and other substructural logics.Worlds are best demythologized as theories, subject to truth-functional and other constraints. The chief constraint is that theories are taken as closed under logical entailment, which clearly begs the question if we are using the semantics to determine which theory L is Logic itself. Instead we draw the modal logicians’ conclusion—there are many substructural logics, each with its appropriate ternary relational postulates.Each logic L gives rise to a Calculus of L-theories, on which particular candidate logical axioms have the combinatorial properties expected from the well-known Curry–Howard isomorphism . We apply their bubbling lemma, updating the Fools Model of Combinatory Logic at the pure → level for the system BT. We make fusion an explicit connective, proving a combinator correspondence theorem. Having taken relevant → as a left residual for , we explore its right residual mate →r. Finally we concentrate on and prove a finite model property for the classical minimal relevant logic CB, a conservative extension of the minimal positive relevant logic B+. (shrink)

We introduce an extension of natural deduction that is suitable for dealing with modal operators and induction. We provide a proof reduction system and we prove a strong normalization theorem for an intuitionistic calculus. As a consequence we obtain a purely syntactic proof of consistency. We also present a classical calculus and we relate provability in the two calculi by means of an adequate formula translation.

Questions connected with the admissibility of rules of inference and the solvability of the substitution problem for modal and intuitionistic logic are considered in an algebraic framework. The main result is the decidability of the universal theory of the free modal algebra imageω extended in signature by adding constants for free generators. As corollaries we obtain: there exists an algorithm for the recognition of admissibility of rules with parameters in the modal system Grz, the substitution problem for Grz and for (...) the intuitionistic calculus H is decidable, intuitionistic propositional calculus H is decidable with respect to admissibility . A semantical criterion for the admissibility of rules of inference in Grz is given. (shrink)

Versions and extensions of intuitionistic and modal logic involving biHeyting and bimodal operators, the axiom of constant domains and Barcan's formula, are formulated as structured categories. Representation theorems for the resulting concepts are proved. Essentially stronger versions, requiring new methods of proof, of known completeness theorems are consequences. A new type of completeness result, with a topos theoretic character, is given for theories satisfying a condition considered by Lawvere . The completeness theorems are used to conclude results asserting that certain (...) logics are conservatively interpretable in others. (shrink)

We use formal semantic analysis based on new constructions to study abstract realizability, introduced by Läuchli in 1970, and expose its algebraic content. We claim realizability so conceived generates semantics-based intuitive confidence that the Heyting Calculus is an appropriate system of deduction for constructive reasoning.Well-known semantic formalisms have been defined by Kripke and Beth, but these have no formal concepts corresponding to constructions, and shed little intuitive light on the meanings of formulae. In particular, the completeness proofs for these semantics (...) do not generate confidence in the sufficiency of the Heyting Calculus, since we have no reason to believe that every intuitively constructive truth is valid in the formal semantics.Läuchli has proved completeness for a realizability semantics with formal concepts analogous to constructions. We argue in some detail that, in spite of a certain inherent inexactness of the analogy, every intuitively constructive truth is valid in Läuchli semantics, and therefore the Heyting Calculus is powerful enough to prove all constructive truths. Our argument is based on the postulate that a uniformly constructible object must be communicable in spite of imprecision in our language, and that the permutations in Läuchli's semantics represent conceivable imprecision in a language, while allowing a certain amount of freedom in choosing the particular structure of the language.We give a detailed generalization of Läuchli's proof of completeness for the propositional part of the Heyting Calculus, in order to make explicit constructive and algebraic content.In our treatment, we establish several new results about Läuchli models. We show how to extend the sconing and gluing constructions familiar from Kripke and Frame semantics and Topos theory, to Läuchli models, and use them to give an algebraic approach to countermodel construction. In particular, the Läuchli arguments are given without the restriction to the integers, Z, as a group of permutations, which makes much of the coding scheme used in Läuchli's original paper transparent.We also make use of a new propositions-as-types syntax for the Heyting calculus, with limited nondeterminism, in which validity of formulae can be decided without loop-detection. (shrink)

A growing number of applications of automated reasoning exhibitsthe necessity of flexible deduction systems. A deduction system should beable to execute inference rules which are appropriate to the given problem.One way to achieve this behavior is the integration of different calculi. Thisled to so called hybrid reasoning [22, 1, 10, 20] which means the integrationof a general purpose foreground reasoner with a specialized background reasoner. A typical task of a background reasoner is to perform special purposeinference rules according to a (...) built-in theory. The aim of this paper is togo a step further, i.e. to treat the background reasoner as a hybrid systemitself. The paper formulates sufficient criteria for the construction of complete calculi which enable reasoning under hybrid theories combined fromsub-theories. For this purpose we use a generic approach described in [20].This more detailed view on built-in theories is not covered by the knowngeneral approaches [1, 3, 6, 20] for building in theories into theorem provers.The approach is demonstrated by its application to the target calculi of thealgebraic translation [9] of multi-modal and extended multi-modal [7] logicto first-order logic. (shrink)

A hyperintensional semantics for natural language is proposed which is agnostic about the question of whether propositions are sets of worlds or worlds are sets of propositions. Montague’s theory of intensional senses is replaced by a weaker theory, written in standard classical higher-order logic, of fine-grained senses which are in a many-to-one correspondence with intensions; Montague’s theory can then be recovered from the proposed theory by identifying the type of propositions with the type of sets of worlds and adding an (...) axiom to the effect that each world is the set of propositions which are true there. Senses are compositionally assigned to linguistic expressions by a categorial grammar with only two rule schemas, based on the implicative fragment of intuitionistic linear propositional logic, and a fully explicit grammar fragment is provided that illustrates the compositional assignment of sense to a variety of constructions, including dummy-subject constructions, infinitive complements, predicative adjectives and nominals, raising to subject, ‘tough-movement’, and quantifier scope ambiguities. Notably, the grammar and the derivations that it licenses never make reference to either worlds or to the extensions of senses. (shrink)

Crosslinguistically, the same modal words can be used to express a wide range of interpretations. This crosslinguistic trend supports a Kratzerian analysis, where each modal has a core lexical entry and where the difference between an epistemic and a root interpretation is contextually determined. A long-standing problem for such a unified account is the equally robust crosslinguistic correlation between a modal’s interpretation and its syntactic behavior: epistemics scope high (in particular higher than tense and aspect) and roots low, a fact (...) which has led to proposals that hardwire different syntactic positions for epistemics and roots (cf. Cinque’s hierarchy). This paper argues that the range of interpretations a modal receives is even more restricted: a modal must be keyed to certain time-individual pairs, but not others. I show that this can be captured straightforwardly by minimally modifying the Kratzerian account: modals are relative to an event—rather than a world—of evaluation, which readily provides a time (the event’s running time) and (an) individual(s) (the event’s participants). I propose that this event relativity of modals can in turn explain the correlation between type of interpretation and syntactic position, without stipulation of an interpretation-specific height for modals. (shrink)

In this article, I propose a semantic account of temporally mismatched past subjunctive counterfactuals. The proposal consists of the following parts. First, I show that in cases of temporal mismatch, [past] cannot be interpreted inside the proposition where it occurs at surface structure. Instead, it must be interpreted as constraining the time argument of the accessibility relation. This has the effect of shifting the time of the evaluation of the conditional to some contextually salient past time. Second, I will propose (...) specific felicity conditions (presuppositions) for subjunctive conditionals and I will argue that there is a strict correspondence between the time of evaluation in the truth conditions of a conditional and the time relevant for the felicity conditions. In other words, if the time relevant for the accessibility relation has been shifted to the past, then the conditional's presupposition will make reference to a past context. On the other hand, if no past is constraining the time argument of the accessibility relation, the conditional's felicity will make reference to the current (main) context. Third, I will argue that the intuition that the antecedent of mismatched counterfactuals is not true is a scalar implicature arising from a competition not between assertions but between presuppositions. Finally, I will investigate the repercussions of my proposal for the general theory of modality. (shrink)

The purpose of this paper is to develop a class of semantic tableau systems for some dyadic deontic logics. We will consider 16 different pure dyadic deontic tableau systems and 32 different alethic dyadic deontic tableau systems. Possible world semantics is used to interpret our formal languages. Some relationships between our systems and well known dyadic deontic logics in the literature are pointed out and soundness results are obtained for every tableau system. Completeness results are obtained for all 16 pure (...) dyadic deontic systems and for 16 alethic dyadic deontic systems. (shrink)

The purpose of this paper is to develop a class of semantic tableau systems for some counterfactual logics. All in all I will discuss 1024 systems. Possible world semantics is used to interpret our formal languages. Soundness results are obtained for every tableau system and completeness results for a large subclass of these.

ABSTRACT In this paper it is shown that a broad class of propositional logics can be interpreted in an equational logic based on fork algebras. This interpetability enables us to develop a fork-algebraic formalization of these logics and, as a consequence, to simulate non-classical means of reasoning with equational theories algebras.

Let $\mathcal{L}$ be a propositional language with standard Boolean connectives plus two modalities: an S4-ish topological modality $\square$ and a temporal modality $\bigcirc$ , understood as ‘next’. We extend the topological semantic for S4 to a semantics for the language $\mathcal{L}$ by interpreting $\mathcal{L}$ in dynamic topological systems, i.e. ordered pairs $\langle X, f\rangle$ , where X is a topological space and f is a continuous function on X. Artemov, Davoren and Nerode have axiomatized a logic S4C, and have shown (...) that S4C is sound and complete for this semantics. Zhang and Mints have shown that S4C is complete relative to a particular topological space, Cantor space. The current paper produces an alternate proof of the Zhang-Mints result. (shrink)

In this paper we argue that hybrid logic is the deductive setting most natural for Kripke semantics. We do so by investigating hybrid axiomatics for a variety of systems, ranging from the basic hybrid language (a decidable system with the same complexity as orthodox propositional modal logic) to the strong Priorean language (which offers full first-order expressivity).We show that hybrid logic offers a genuinely first-order perspective on Kripke semantics: it is possible to define base logics which extend automatically to a (...) wide variety of frame classes and to prove completeness using the Henkin method. In the weaker languages, this requires the use of non-orthodox rules. We discuss these rules in detail and prove non-eliminability and eliminability results. We also show how another type of rule, which reflects the structure of the strong Priorean language, can be employed to give an even wider coverage of frame classes. We show that this deductive apparatus gets progressively simpler as we work our way up the expressivity hierarchy, and conclude the paper by showing that the approach transfers to first-order hybrid logic. (shrink)

This paper deals with one kind of Kripke-style semantics, which we shall call algebraic Kripke-style semantics, for relevance logics. We first recall the logic R of relevant implication and some closely related systems, their corresponding algebraic structures, and algebraic completeness results. We provide simpler algebraic completeness proofs. We then introduce various types of algebraic Kripke-style semantics for these systems and connect them with algebraic semantics.

In this article I defend that Floridi’s Theory of Strongly Semantic Information – TSSI – is correct while encompassing the Veracity Thesis, which guides the semantic information definition as “p is information if and only if p is constituted by meaningful, truth well-formed data”. I argue that the theory is not arbitrary because it deals with important philosophical conundrums, mainly by avoiding the Bar-Hillel and Carnap paradox (1953) generated from the classical theory of semantic information. First, one of the classic (...) theory’s main result is discussed: the production of “too much informative sentences to be true”. Then the motivations to elaborate a “logic of being informed” are summarized and it is shown how the KTB-IL system is built and modelled keeping the veracity axiom among its axioms – K or A4. Finally the TSSI is examined and defended by showing that it aletically restricts the extension of the classic concept of information, avoiding problems with tautologies and contradictions. The TSSI offers an original solution by capturing our modal intuitions concerning informativeness as a basic notion. (shrink)

In this paper we introduce non-normal modal extensions of the sub-classical logics CLoN, CluN and CLaN, in the same way that S0.5 0 extends classical logic. The first modal system is both paraconsistent and paracomplete, while the second one is paraconsistent and the third is paracomplete. Despite being non-normal, these systems are sound and complete for a suitable Kripke semantics. We also show that these systems are appropriate for interpreting □ as “is provable in classical logic”. This allows us to (...) recover the theorems of propositional classical logic within three sub-classical modal systems. (shrink)

This paper presents an algebraic approach of some many-valued generalizations of modal logic. The starting point is the definition of the [0, 1]-valued Kripke models, where [0, 1] denotes the well known MV-algebra. Two types of structures are used to define validity of formulas: the class of frames and the class of Ł n -valued frames. The latter structures are frames in which we specify in each world u the set (a subalgebra of Ł n ) of the allowed truth (...) values of the formulas in u. We apply and develop algebraic tools (namely, canonical and strong canonical extensions) to generate complete modal n + 1-valued logics and we obtain many-valued counterparts of Shalqvist canonicity result. (shrink)

We show that the actuality operator A is redundant in any propositional modal logic characterized by a class of Kripke models (respectively, neighborhood models). Specifically, we prove that for every formula ${\phi}$ in the propositional modal language with A, there is a formula ${\psi}$ not containing A such that ${\phi}$ and ${\psi}$ are materially equivalent at the actual world in every Kripke model (respectively, neighborhood model). Inspection of the proofs leads to corresponding proof-theoretic results concerning the eliminability of the actuality (...) operator in the actuality extension of any normal propositional modal logic and of any “classical” modal logic. As an application, we provide an alternative proof of a result of Williamson’s to the effect that the compound operator A□ behaves, in any normal logic between T and S5, like the simple necessity operator □ in S5. (shrink)

The fundamental principle of the theory of possible worlds is that a proposition p is possible if and only if there is a possible world at which p is true. In this paper we present a valid derivation of this principle from a more general theory in which possible worlds are defined rather than taken as primitive. The general theory uses a primitive modality and axiomatizes abstract objects, properties, and propositions. We then show that this general theory has very small (...) models and hence that its ontological commitments—and, therefore, those of the fundamental principle of world theory—are minimal. (shrink)

The paper is a brief survey of the most important semantic constructions founded on the concept of possible world. It is impossible to capture in one short paper the whole variety of the problems connected with manifold applications of possible worlds. Hence, after a brief explanation of some philosophical matters I take a look at possible worlds from rather technical standpoint of logic and focus on the applications in formal semantics. In particular, I would like to focus on the fruitful (...) marriage of possible world semantics and algebra and its evolution leading to very general construction of Wójcicki called referential semantics and some of its refinements. The presentation is informal and sketchy; the main purpose is to put in one place a short, and readable I hope, description of the most important constructions and to point out the main sources of these solutions. (shrink)

The axiomatic presentation of modal systems and the standard formulations of natural deduction and sequent calculus for modal logic are reviewed, together with the difficulties that emerge with these approaches. Generalizations of standard proof systems are then presented. These include, among others, display calculi, hypersequents, and labelled systems, with the latter surveyed from a closer perspective.

A proof-theoretical treatment of collectively accepted group beliefs is presented through a multi-agent sequent system for an axiomatization of the logic of acceptance. The system is based on a labelled sequent calculus for propositional multi-agent epistemic logic with labels that correspond to possible worlds and a notation for internalized accessibility relations between worlds. The system is contraction- and cut-free. Extensions of the basic system are considered, in particular with rules that allow the possibility of operative members or legislators. Completeness with (...) respect to the underlying Kripke semantics follows from a general direct and uniform argument for labelled sequent calculi extended with mathematical rules for frame properties. As an example of the use of the calculus we present an analysis of the discursive dilemma. (shrink)