We consider a logic which is semantically dual (in some precise sense of the term) to intuitionistic. This logic can be labeled as “falsification logic”: it embodies the Popperian methodology of scientific discovery. Whereas intuitionistic logic deals with constructive truth and non-constructive falsity, and Nelson's logic takes both truth and falsity as constructive notions, in the falsification logic truth is essentially non-constructive as opposed to falsity that is conceived constructively. We also briefly clarify the relationships of our falsification logic to (...) some other logical systems. (shrink)

Gentzen’s and Jaśkowski’s formulations of natural deduction are logically equivalent in the normal sense of those words. However, Gentzen’s formulation more straightforwardly lends itself both to a normalization theorem and to a theory of “meaning” for connectives . The present paper investigates cases where Jaskowski’s formulation seems better suited. These cases range from the phenomenology and epistemology of proof construction to the ways to incorporate novel logical connectives into the language. We close with a demonstration of this latter aspect by (...) considering a Sheffer function for intuitionistic logic. (shrink)

How do people make deductions? The orthodox view in psychology is that they use formal rules of inference like those of a “natural deduction” system.Deductionargues that their logical competence depends, not on formal rules, but on mental models. They construct models of the situation described by the premises, using their linguistic knowledge and their general knowledge. They try to formulate a conclusion based on these models that maintains semantic information, that expresses it parsimoniously, and that makes explicit something not directly (...) stated by any premise. They then test the validity of the conclusion by searching for alternative models that might refute the conclusion. The theory also resolves long-standing puzzles about reasoning, including how nonmonotonic reasoning occurs in daily life. The book reports experiments on all the main domains of deduction, including inferences based on prepositional connectives such as “if” and “or,” inferences based on relations such as “in the same place as,” inferences based on quantifiers such as “none,” “any,” and “only,” and metalogical inferences based on assertions about the true and the false. Where the two theories make opposite predictions, the results confirm the model theory and run counter to the formal rule theories. Without exception, all of the experiments corroborate the two main predictions of the model theory: inferences requiring only one model are easier than those requiring multiple models, and erroneous conclusions are usually the result of constructing only one of the possible models of the premises. (shrink)

We prove a completeness theorem for Kmath image, the infinitary extension of the graded version K0 of the minimal normal logic K, allowing conjunctions and disjunctions of countable sets of formulas. This goal is achieved using both the usual tools of the normal logics with graded modalities and the machinery of the predicate infinitary logics in a version adapted to modal logic.

This is primarily a conceptual paper. The goal of the paper is to put into perspective the proof-theory of hybrid logic and in particular, try to give an answer to the following question: Why does the proof-theory of hybrid logic work so well compared to the proof-theory of ordinary modal logic?Roughly, there are two different kinds of proof systems for modal logic: Systems where the formulas involved in the rules are formulas of the object language, that is, ordinary modal-logical formulas, (...) and systems where the formulas involved in the rules are metalingustic formulas obtained by attaching labels representing possible worlds to ordinary modal-logical formulas. Systems of the second kind often also involve an explicit representation of the accessibility relation. From a proof-theoretic point of view, modal-logical systems of the first kind are less well-behaved than systems of the second kind.It turns out that this can be remedied by hybridization, that is, hybridization of modal logics enables the formulation of well-behaved proof systems without involving metalinguistic machinery. What has happened is that the metalinguistic machinery has been internalized in the object language. This gives an answer to the initial question, which is that the proof-theory of hybrid logic works so well because the metalinguistic semantic machinery has been internalized in the object language. (shrink)

Sambin [6] proved the normalization theorem for GL, the modal logic of provability, in a sequent calculus version called by him GLS. His proof does not take into account the concept of reduction, commonly used in normalization proofs. Bellini [1], on the other hand, gave a normalization proof for GL using reductions. Indeed, Sambin's proof is a decision procedure which builds cut-free proofs. In this work we formalize this procedure as a recursive function and prove its recursiveness in an arithmetically (...) formalizable way, concluding that the normalization of GL can be formalized in PA. MSC: 03F05, 03B35, 03B45. (shrink)

This book explores the interplay between logic and science, describing new trends, new issues and potential research developments.

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.

This paper presents an outline of a new theory of relevant deduction which arose from the purpose of solving paradoxes in various fields of analytic philosophy. In distinction to relevance logics, this approach does not replace classical logic by a new one, but distinguishes between relevance and validity. It is argued that irrelevant arguments are, although formally valid, nonsensical and even harmful in practical applications. The basic idea is this: a valid deduction is relevant iff no subformula of the conclusion (...) is replaceable on some of its occurrences by any other formula salva validitate of the deduction. The paper first motivates the approach by showing that four paradoxes seemingly very distant from each other have a common source. Then the exact definition of relevant deduction is given and its logical properties are investigated. An extension to relevance of premises is discussed. Finally the paper presents an overview of its applications in philosophy of science, ethics, cognitive psychology and artificial intelligence. (shrink)

We investigate sequent calculi for the weak modal (propositional) system reduced to the equivalence rule and extensions of it up to the full Kripke system containing monotonicity, conjunction and necessitation rules. The calculi have cut elimination and we concentrate on the inversion of rules to give in each case an effective procedure which for every sequent either furnishes a proof or a finite countermodel of it. Applications to the cardinality of countermodels, the inversion of rules and the derivability of Löb (...) rules are given. (shrink)

In this paper we provide cut-free tableau calculi for the intuitionistic modal logics IK, ID, IT, i.e. the intuitionistic analogues of the classical modal systems K, D and T. Further, we analyse the necessity of duplicating formulas to which rules are applied. In order to develop these calculi we extend to the modal case some ideas presented by Miglioli, Moscato and Ornaghi for intuitionistic logic. Specifically, we enlarge the language with the new signs Fc and CR near to the usual (...) signs T and F. In this work we establish the soundness and completeness theorems for these calculi with respect to the Kripke semantics proposed by Fischer Servi. (shrink)

In this paper, we compare several cut-free sequent systems for propositional intuitionistic logic Intwith respect to polynomial simulations. Such calculi can be divided into two classes, namely single-succedent calculi (like Gentzen's LJ) and multi-succedent calculi. We show that the latter allow for more compact proofs than the former. Moreover, for some classes of formulae, the same is true if proofs in single-succedent calculi are directed acyclic graphs (dags) instead of trees. Additionally, we investigate the effect of weakening rules on the (...) structure and length of dag proofs.The second topic of this paper is the effect of different embeddings from Int to S4. We select two different embeddings from the literature and show that translated (propositional) intuitionistic formulae have sometimes exponentially shorter minimal proofs in a cut-free Gentzen system for S4than the original formula in a cut-free single-succedent Gentzen system for Int. Moreover, the length and the structure of proofs of translated formulae crucially depend on the chosen embedding. (shrink)

In previous work we gave an approach, based on labelled natural deduction, for formalizing proof systems for a large class of propositional modal logics that includes K, D, T, B, S4, S4.2, KD45, and S5. Here we extend this approach to quantified modal logics, providing formalizations for logics with varying, increasing, decreasing, or constant domains. The result is modular with respect to both properties of the accessibility relation in the Kripke frame and the way domains of individuals change between worlds. (...) Our approach has a modular metatheory too; soundness, completeness and normalization are proved uniformly for every logic in our class. Finally, our work leads to a simple implementation of a modal logic theorem prover in a standard logical framework. (shrink)

Bilateral proof systems, which provide rules for both affirming and denying sentences, have been prominent in the development of proof-theoretic semantics for classical logic in recent years. However, such systems provide a substantial amount of freedom in the formulation of the rules, and, as a result, a number of different sets of rules have been put forward as definitive of the meanings of the classical connectives. In this paper, I argue that a single general schema for bilateral proof rules has (...) a reasonable claim to inferentially articulating the core meaning of all of the classical connectives. I propose this schema in the context of a bilateral sequent calculus in which each connective is given exactly two rules: a rule for affirmation and a rule for denial. Positive and negative rules for all of the classical connectives are given by a single rule schema, harmony between these positive and negative rules is established at the schematic level by a pair of elimination theorems, and the truth-conditions for all of the classical connectives are read off at once from the schema itself. (shrink)

We present a rooted hypersequent calculus for modal propositional logic S5. We show that all rules of this calculus are invertible and that the rules of weakening, contraction, and cut are admissible. Soundness and completeness are established as well.

This chapter contains sections titled: Introduction Modal propositional Logics (MPLs) Modal Quantificational Logics(QMLs).

This is the first book-length treatment of hybrid logic and its proof-theory. Hybrid logic is an extension of ordinary modal logic which allows explicit reference to individual points in a model. This is useful for many applications, for example when reasoning about time one often wants to formulate a series of statements about what happens at specific times. There is little consensus about proof-theory for ordinary modal logic. Many modal-logical proof systems lack important properties and the relationships between proof systems (...) for different modal logics are often unclear. In the present book we demonstrate that hybrid-logical proof-theory remedies these deficiencies by giving a spectrum of well-behaved proof systems for a spectrum of different hybrid logics. (shrink)

We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into a special form that is translatable to (...) a derivation in the associated display calculus. A key insight in this converse translation is a canonical representation of display sequents as labeled polytrees. Labeled polytrees, which represent equivalence classes of display sequents modulo display postulates, also shed light on related correspondence results for tense logics. (shrink)

This paper investigates and develops generalizations of two-dimensional modal logics to any finite dimension. These logics are natural extensions of multidimensional systems known from the literature on logics for a priori knowledge. We prove a completeness theorem for propositional n-dimensional modal logics and show them to be decidable by means of a systematic tableau construction.

Epistemic logic is usually employed to model two aspects of a situation: the factual and the epistemic aspects. Truth, however, is not always attainable, and in many cases we are forced to reason only with whatever information is available to us. In this paper, we will explore a four-valued epistemic logic designed to deal with these situations, where agents have only knowledge about the available information, which can be incomplete or conflicting, but not explicitly about facts. This layer of available (...) information or evidence, which is the object of the agents’ knowledge, can be seen as a database. By adopting this sceptical posture in our semantics, we prepare the ground for logics where the notion of knowledge—or more appropriately, belief—is entirely based on evidence. The technical results include a set of reduction axioms for public announcements, correspondence proofs, and a complete tableau system. In summary, our contributions are twofold: on the one hand we present an intuition and possible application for many-valued modal logics, and on the other hand we develop a logic that models the dynamics of evidence in a simple and intuitively clear fashion. (shrink)

In the paper a decision procedure for S5 is presented which uses a cut-free sequent calculus with additional rules allowing a reduction to normal modal forms. It utilizes the fact that in S5 every formula is equivalent to some 1-degree formula, i.e. a modally-flat formula with modal functors having only boolean formulas in its scope. In contrast to many sequent calculi for S5 the presented system does not introduce any extra devices. Thus it is a standard version of SC but (...) with some additional simple rewrite rules. The procedure combines the proces of saturation of sequents with reduction of their elements to some normal modal form. (shrink)

We prove a completeness theorem for Kf, an extension of K by the operator ⋄f that means “there exists a finite number of accessible worlds such that … is true, plus suitable axioms to rule it. This is done by an application of the method of consistency properties for modal systems as in [4] with suitable adaptations. Despite no graded modality is invoked here, we consider this work as pertaining to that area both because ⋄f is a definable operator in (...) the graded infinitary system Kω10, and because this idea was the original source for the development of graded modalities. (shrink)

In Paradoxa Stoicorum, the Roman philosopher Cicero defends six important Stoic theses. Since these theses seem counterintuitive, and it is not likely that the average person would agree with them, they were generally called "paradoxes". According to the third paradox, (P3), (all) transgressions (wrong actions) are equal and (all) right actions are equal. According to one interpretation of this principle, which I will call (P3′), it means that if it is forbidden that A and it is forbidden that B, then (...) not-A is as good as not-B; and if it is permitted that A and it is permitted that B, then A is as good as B. In this paper, I show how it is possible to prove this thesis in dyadic deontic logic. I also try to defend (P3′) against some philosophical counterarguments. Furthermore, I address the claim that (P3′) is not a correct interpretation of Cicero’s third paradox and the assertion that it does not matter whether (P3′) is true or not. I argue that it does matter whether (P3′) is true or not, but acknowledge that (P3′) is perhaps a slightly different principle than Cicero’s thesis. The upshot is that (P3′) seems to be a plausible principle, and that at least one part of paradox III in Cicero’s Paradoxa Stoicorum appears to be defensible. (shrink)

In this paper we introduce and compare four different syntactic methods for generating sequent calculi for the main systems of modal logic: the multiple sequents method, the higher-arity sequents method, the tree-hypersequents method and the display method. More precisely we show how the first three methods can all be translated in the fourth one. This result sheds new light on these generalisations of the sequent calculus and raises issues that will be examined in the last section.

A number of significant contributions in the last four decades show that non-normal modal logics can be fruitfully employed in several applied fields. Well-known domains are epistemic logic, deontic logic, and systems capturing different aspects of action and agency such as the modal logic of agency, concurrent propositional dynamic logic, game logic, and coalition logic. Semantics for such logics are traditionally based on neighbourhood models. However, other model-theoretic semantics can be used for this purpose. Here, we systematically study multi-relational structures, (...) whose investigation is still relatively underdeveloped. After a brief introduction to two different versions of multi-relational semantics – which we call strong and weak multi-relational semantics – we proceed to study several modal schemata. Special attention is paid to the schemata CON and D. Finally we offer completeness proofs for several systems using both strong and weak semantic tools: The proofs thus cover both classical system.. (shrink)

ABSTRACT This paper follows on previous papers which present and evaluate various decision procedures for modal logics. We consider new test sets and systems that have been recently proposed in the literature. This new experimental analysis confirm previous experimental results in showing that SAT based decision procedures, i.e., the procedures built on top of decision procedures for propositional satisfiability, are more efficient than tableau based decision procedures. They also confirm previous evidence of an easy-hard-easy pattern in the satisfiability curve for (...) modal K. Finally, on these tests, SAT based decision procedures are also more efficient than the recently proposed decision procedures based on translation methods. These results contradict some of the claims presented in previous papers by other authors. (shrink)

XML documents and, more generally, semistructured data, can be seen as labelled graphs. In this paper we set a correspondence between such graphs and the models of a language of hybrid multimodal logic. This allows us to characterize a schema for semistructured data as a formula of hybrid multimodal logic, and instances of the schema as models of this formula. We also investigate how to express in such a logic integrity constraints on semistructured data, in particular some classes of constraints (...) widely considered in the literature. The contribution of this work is twofold: 1) We generalize the notion of schema, by proposing a definition of schema were references are “well typed”. 2) We formalize semistructured data, schema for semistructured data and integrity constraints in a unique framework, namely hybrid multimodal logic. (shrink)