Online research in philosophy

This is a first course in propositional modal logic, suitable for mathematicians, computer scientists and philosophers. Emphasis is placed on semantic aspects, in the form of labelled transition structures, rather than on proof theory. The book covers all the basic material - propositional languages, semantics and correspondence results, proof systems and completeness results - as well as some topics not usually covered in a modal logic course. It is written from a mathematical standpoint. To help the reader, the material is covered in short chapters, each concentrating on one topic. These are arranged into five parts, each with a common theme. An important feature of the book is the many exercises and an extensive set of solutions is provided.

This article is oriented toward the use of modality in artificial intelligence (AI). An agent must reason about what it or other agents know, believe, want, intend or owe. Referentially opaque modalities are needed and must be formalized correctly. Unfortunately, modal logics seem too limited for many important purposes. This article contains examples of uses of modality for which modal logic seems inadequate.I have no proof that modal logic is inadequate, so I hope modal logicians will take the examples as challenges.

This book, written by one of the most distinguished of contemporary philosophers of mathematics, is a fully rewritten and updated successor to the author's earlier The Unprovability of Consistency (CUP, 1979). Modal logic is concerned with the notions of necessity and possibility. What George Boolos does is to show how the concepts, techniques and methods of modal logic shed brilliant light on the most important logical discovery of the twentieth century: the incompleteness theorems of Kurt Godel and the 'self referential' sentences constructed in their proof. The book explores the effects of reinterpreting the notions of necessity and possibility to near probability and consistency. It contains the first application of quantified modal logic to formal probability, and shows the results of applying modal logic to formal provability.

This volume examines the notion of an analytic proof as a natural deduction, suggesting that the proof's value may be understood as its normal form--a concept with significant implications to proof-theoretic semantics.

It is well known that the modal logic S5 can be embedded in the classical predicate logic by interpreting the modal operator in terms of a quantifier. Wajsberg [10] proved this fact in a syntactic way. Mints [7] extended this result to the quantified version of S5; using a purely proof-theoretic method he showed that the quantified S5 corresponds to the classical predicate logic with one-sorted variable. In this paper we extend Mints' result to the basic modal logic S4; we investigate the correspondence between the quantified versions of S4 (with and without the Barcan formula) and the classical predicate logic (with one-sorted variable). We present a purely proof-theoretic proof-transformation method, reducing an LK-proof of an interpreted formula to a modal proof.

The title reflects my conviction that, viewed semantically,modal logic is fundamentally dialogical; this conviction is based on the key role played by the notion of bisimulation in modal model theory. But this dialogical conception of modal logic does not seem to apply to modal proof theory, which is notoriously messy. Nonetheless, by making use of ideas which trace back to Arthur Prior (notably the use of nominals, special proposition symbols which name worlds) I will show how to lift the dialogical conception to modal proof theory. I argue that this shift to hybrid logic has consequences for both modal and dialogical logic, and I discuss these in detail.

Goal Directed Proof Theory presents a uniform and coherent methodology for automated deduction in non-classical logics, the relevance of which to computer science is now widely acknowledged. The methodology is based on goal-directed provability. It is a generalization of the logic programming style of deduction, and it is particularly favourable for proof search. The methodology is applied for the first time in a uniform way to a wide range of non-classical systems, covering intuitionistic, intermediate, modal and substructural logics. The book can also be used as an introduction to these logical systems form a procedural perspective. Readership: Computer scientists, mathematicians and philosophers, and anyone interested in the automation of reasoning based on non-classical logics. The book is suitable for self study, its only prerequisite being some elementary knowledge of logic and proof theory.

We give an exponential lower bound on number of proof-lines in the proof system K of modal logic, i.e., we give an example of K-tautologies ψ1,ψ2,… s.t. every K-proof of ψi must have a number of proof-lines exponential in terms of the size of ψi. The result extends, for the same sequence of K-tautologies, to the systems K4, Gödel—Löb’s logic, S and S4. We also determine some speed-up relations between different systems of modal logic on formulas of modal-depth one.

Machine generated contents note: Prologue: Hilbert's Last Problem; 1. Introduction; Part I. Proof Systems Based on Natural Deduction: 2. Rules of proof: natural deduction; 3. Axiomatic systems; 4. Order and lattice theory; 5. Theories with existence axioms; Part II. Proof Systems Based on Sequent Calculus: 6. Rules of proof: sequent calculus; 7. Linear order; Part III. Proof Systems for Geometric Theories: 8. Geometric theories; 9. Classical and intuitionistic axiomatics; 10. Proof analysis in elementary geometry; Part IV. Proof Systems for Nonclassical Logics: 11. Modal logic; 12. Quantified modal logic, provability logic, and so on; Bibliography; Index of names; Index of subjects.

The Unprovability of Consistency is concerned with connections between two branches of logic: proof theory and modal logic. Modal logic is the study of the principles that govern the concepts of necessity and possibility; proof theory is, in part, the study of those that govern provability and consistency. In this book, George Boolos looks at the principles of provability from the standpoint of modal logic. In doing so, he provides two perspectives on a debate in modal logic that has persisted for at least thirty years between the followers of C. I. Lewis and W. V. O. Quine. The author employs semantic methods developed by Saul Kripke in his analysis of modal logical systems. The book will be of interest to advanced undergraduate and graduate students in logic, mathematics and philosophy, as well as to specialists in those fields.