ProofTheory of Modal Logic is devoted to a thorough study of proof systems for modal logics, that is, logics of necessity, possibility, knowledge, belief, time, computations etc. It contains many new technical results and presentations of novel proof procedures. The volume is of immense importance for the interdisciplinary fields of logic, knowledge representation, and automated deduction.
Goal Directed ProofTheory 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 prooftheory. (shrink)
The division between theory and pedagogy is an example of the more traditional division between theory and practice. The paper deals with the artificiality inherent in the institutional separation of those scholars who study within a subject area and those who study the pedagogy of the subject. The paper discusses various theoretical accounts of the nature of English to make the case that theory is imbued with pedagogy. That is, theory is not neutral about (...)teaching. How we teach is driven by our theoretical commitments to our subject. (shrink)
This introduction to the basic ideas of structural prooftheory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic (intuitionistic as well as classical); the theory of logic programming; category theory; modal logic; linear logic; first-order arithmetic and second-order logic. In each case the aim is to illustrate the methods in relatively simple situations and then apply (...) them elsewhere in much more complex settings. There are numerous exercises throughout the text. In general, the only prerequisite is a standard course in first-order logic, making the book ideal for graduate students and beginning researchers in mathematical logic, theoretical computer science and artificial intelligence. For the new edition, many sections have been rewritten to improve clarity, new sections have been added on cut elimination, and solutions to selected exercises have been included. (shrink)
Proof-theoretical notions and techniques, developed on the basis of sentential/symbolic representations of formal proofs, are applied to Euler diagrams. A translation of an Euler diagrammatic system into a natural deduction system is given, and the soundness and faithfulness of the translation are proved. Some consequences of the translation are discussed in view of the notion of free ride, which is mainly discussed in the literature of cognitive science as an account of inferential efficacy of diagrams. The translation enables us (...) to formalize and analyze free ride in terms of prooftheory. The notion of normal form of Euler diagrammatic proofs is investigated, and a normalization theorem is proved. Some consequences of the theorem are further discussed: in particular, an analysis of the structure of normal diagrammatic proofs; a diagrammatic counterpart of the usual subformula property; and a characterization of diagrammatic proofs compared with natural deduction proofs. (shrink)
This volume contains articles covering a broad spectrum of prooftheory, with an emphasis on its mathematical aspects. The articles should not only be interesting to specialists of prooftheory, but should also be accessible to a diverse audience, including logicians, mathematicians, computer scientists and philosophers. Many of the central topics of prooftheory have been included in a self-contained expository of articles, covered in great detail and depth. The chapters are arranged so that (...) the two introductory articles come first; these are then followed by articles from core classical areas of prooftheory; the handbook concludes with articles that deal with topics closely related to computer science. (shrink)
This work is derived from the SERC "Logic for IT" Summer School Conference on ProofTheory held at Leeds University. The contributions come from acknowledged experts and comprise expository and research articles which form an invaluable introduction to prooftheory aimed at both mathematicians and computer scientists.
Jean van Heijenoort was best known for his editorial work in the history of mathematical logic. I survey his contributions to model-theoretic prooftheory, and in particular to the falsifiability tree method. This work of van Heijenoort’s is not widely known, and much of it remains unpublished. A complete list of van Heijenoort’s unpublished writings on tableaux methods and related work in prooftheory is appended.
Feminist theory is a central strand of cultural studies. This book explores the history of feminist cultural studies from the early work of Mary Wollstonecraft, Charlotte Perkins Gilman, Virginia Woolf, Simone de Beauvoir, through the 1970s Women's Liberation Movement. It also provides a comprehensive introduction to the contemporary key approaches, theories and debates of feminist theory within cultural studies, offering a major re-mapping of the field. It will be an essential text for students taking courses within both cultural (...) studies and women's studies departments. (shrink)
Families of types are fundamental objects in Martin-Löf type theory. When extending the notion of setoid (type with an equivalence relation) to families of setoids, a choice between proof-relevant or proof-irrelevant indexing appears. It is shown that a family of types may be canonically extended to a proof-relevant family of setoids via the identity types, but that such a family is in general proof-irrelevant if, and only if, the proof-objects of identity types are unique. (...) A similar result is shown for fibre representations of families. The ubiquitous role of proof-irrelevant families is discussed. (shrink)
This book is a specialized monograph on the development of the mathematical and computational metatheory of reductive logic and proof-search including proof-theoretic, semantic/model-theoretic and algorithmic aspects. The scope ranges from the conceptual background to reductive logic, through its mathematical metatheory, to its modern applications in the computational sciences.
In this paper, we show the equivalence between the provability of a proof system of basic hybrid logic and that of translated formulas of the classical predicate logic with equality and explicit substitution by a purely proof–theoretic method. Then we show the equivalence of two groups of proof systems of hybrid logic: the group of labelled deduction systems and the group of modal logic-based systems.
A combination of epistemic logic and dynamic logic of programs is presented. Although rich enough to formalize some simple game-theoretic scenarios, its axiomatization is problematic as it leads to the paradoxical conclusion that agents are omniscient. A cut-free labelled Gentzen-style proof system is then introduced where knowledge and action, as well as their combinations, are formulated as rules of inference, rather than axioms. This provides a logical framework for reasoning about games in a modular and systematic way, and to (...) give a step-by-step reconstruction of agents omniscience. In particular, its semantic assumptions are made explicit and a possible solution can be found in weakening the properties of the knowledge operator. (shrink)
In the last decade the concept of context has been extensivelyexploited in many research areas, e.g., distributed artificialintelligence, multi agent systems, distributed databases, informationintegration, cognitive science, and epistemology. Three alternative approaches to the formalization of the notion ofcontext have been proposed: Giunchiglia and Serafini's Multi LanguageSystems (ML systems), McCarthy's modal logics of contexts, andGabbay's Labelled Deductive Systems.Previous papers have argued in favor of ML systems with respect to theother approaches. Our aim in this paper is to support these arguments froma (...) theoretical perspective. We provide a very general definition of ML systems, which covers allthe ML systems used in the literature, and we develop a proof theoryfor an important subclass of them: the MR systems. We prove variousimportant results; among other things, we prove a normal form theorem,the sub-formula property, and the decidability of an importantinstance of the class of the MR systems. The paper concludes with a detailed comparison among the alternativeapproaches. (shrink)
Aim of this work is to investigate from a proof-theoretic viewpoint a propositional and a predicate sequent calculus with an ω–type schema of inference that naturally interpret the propositional and the predicate until–free fragments of Linear Time Logic LTL respectively. The two calculi are based on a natural extension of ordinary sequents and of standard modal rules. We examine the pure propositional case (no extralogical axioms), the propositional and the first order predicate cases (both with a possibly infinite set (...) of extralogical axioms). For each system we provide a syntactic proof of cut elimination and a proof of completeness. (shrink)
The ability to reason and think in a logical manner forms the basis of learning for most mathematics, computer science, philosophy and logic students. Based on the author's teaching notes at the University of Maryland and aimed at a broad audience, this text covers the fundamental topics in classical logic in an extremely clear, thorough and accurate style that is accessible to all the above. Covering propositional logic, first-order logic, and second-order logic, as well as prooftheory, (...) computability theory, and model theory, the text also contains numerous carefully graded exercises and is ideal for a first or refresher course. (shrink)
Paul Cohen’s method of forcing, together with Saul Kripke’s related semantics for modal and intuitionistic logic, has had profound eﬀects on a number of branches of mathematical logic, from set theory and model theory to constructive and categorical logic. Here, I argue that forcing also has a place in traditional Hilbert-style prooftheory, where the goal is to formalize portions of ordinary mathematics in restricted axiomatic theories, and study those theories in constructive or syntactic terms. (...) I will discuss the aspects of forcing that are useful in this respect, and some sample applications. The latter include ways of obtaining conservation results for classical and intuitionistic theories, interpreting classical theories in constructive ones, and constructivizing model-theoretic arguments. (shrink)
Our first aim is to make the study of informal notions of proof plausible. Put differently, since the raison d'étre of anything like existing prooftheory seems to rest on such notions, the aim is nothing else but to make a case for prooftheory; ...
A general definition theory should serve as a foundation for the mathematical study of definitional structures. The central notion of such a theory is a precise explication of the intuitively given notion of a definitional structure. The purpose of this paper is to discuss the prooftheory of partial inductive definitions as a foundation for this kind of a more general definition theory. Among the examples discussed is a suggestion for a more abstract definition (...) of lambda-terms (derivations in natural deduction) that could provide a basis for a more systematic definitional approach to general prooftheory. (shrink)
The purpose of this study was to establish the usage of research and theory in the teaching of English language in secondary schools in Botswana. Altogether 100 questionnaires were administered in 19 secondary schools. The results of this study indicate that teachers rarely ever refer to language research in their teaching. Less value was also placed on the theoretical information acquired during training. The respondents indicated that their teaching is essentially based on utilizing their (...)teaching experience and individual creativity. (shrink)
There is now substantial agreement about the representational component of a normative theory of causal reasoning: Causal Bayes Nets. There is less agreement about a normative theory of causal discovery from data, either computationally or cognitively, and almost no work investigating how teaching the Causal Bayes Nets representational apparatus might help individuals faced with a causal learning task. Psychologists working to describe how naïve participants represent and learn causal structure from data have focused primarily on learning from (...) single trials under a variety of conditions. In contrast, one component of the normative theory focuses on learning from a sample drawn from a population under some experimental or observational study regime. Through a virtual Causality Lab that embodies the normative theory of causal reasoning and which allows us to record student behavior, we have begun to systematically explore how best to teach the normative theory. In this paper we explain the overall project and report on pilot studies which suggest that students can quickly be taught to (appear to) be quite rational. (shrink)
Senior lecturers/lecturers in mental health nursing (11 in round one, nine in round two, and eight in the final round) participated in a three-round Delphi study into the teaching of health care ethics (HCE) to students of nursing. The participants were drawn from six (round one) and four (round three) UK universities. Information was gathered on the organization, methods used and content of HCE modules. Questionnaire responses were transcribed and the content analysed for patterns of interest and areas (...) of convergence or divergence. Findings include: the majority (72.8%) of the sample believed that insufficient time was allocated to the teaching of HCE; case studies were considered a popular, although problematic, teaching method; the ‘four principles’ approach was less than dominant in the teaching of HCE; and virtue ethics was taught by only 36.4% of the participants. The Delphi technique proved adequate and worth while for the purposes of this study. Further empirical research could aim to replicate or contradict these findings, using a larger sample and recruiting more university departments. Reflection is required on several issues, including the depth and breadth to which ethics theory and, more controversially, meta-ethics, are taught to nursing students. (shrink)
There are many algorithm texts that provide lots of well-polished code and proofs of correctness. Instead, this book presents insights, notations, and analogies to help the novice describe and think about algorithms like an expert. By looking at both the big picture and easy step-by-step methods for developing algorithms, the author helps students avoid the common pitfalls. He stresses paradigms such as loop invariants and recursion to unify a huge range of algorithms into a few meta-algorithms. Part of the goal (...) is to teach the students to think abstractly. Without getting bogged with formal proofs, the book fosters a deeper understanding of how and why each algorithm works. These insights are presented in a slow and clear manner accessible to second- or third-year students of computer science, preparing them to find their own innovative ways to solve problems. (shrink)
I present an account of truth values for classical logic, intuitionistic logic, and the modal logic S5, in which truth values are not a fundamental category from which the logic is defined, but rather, an idealisation of more fundamental logical features in the prooftheory for each system. The result is not a new set of semantic structures, but a new understanding of how the existing semantic structures may be understood in terms of a more fundamental notion of (...) logical consequence. (shrink)
The need to make young scientists aware of their social responsibilities is widely acknowledged, although the question of how to actually do it has so far gained limited attention. A 2-day workshop entitled “Prepared for social responsibility?” attended by doctoral students from multiple disciplines in climate science, was targeted at the perceived needs of the participants and employed a format that took them through three stages of ethics education: sensitization, information and empowerment. The workshop aimed at preparing doctoral students to (...) manage ethical dilemmas that emerge when climate science meets the public sphere (e.g., to identify and balance legitimate perspectives on particular types of geo-engineering), and is an example of how to include social responsibility in doctoral education. The paper describes the workshop from the three different perspectives of the authors: the course teacher, the head of the graduate school, and a graduate student. The elements that contributed to the success of the workshop, and thus make it an example to follow, are (1) the involvement of participating students, (2) the introduction of external expertise and role models in climate science, and (3) a workshop design that focused on ethical analyses of examples from the climate sciences. (shrink)
This latest volume in the Oxford Readings in Feminism series consists of an exciting collection of articles addressing key questions for feminism and cultural studies. Encompassing both classic articles and challenging new work, Feminism and Cultural Studies is organized thematically and addresses commodification, women and labor, mass culture, fantasy and ideas of home.
The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in prooftheory and computational calculi as found in type theory. For instance, minimal propositional logic corresponds to simply typed lambda-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, sequent calculus is related to explicit substitution, etc. The isomorphism has many aspects, even at the syntactic level: formulas correspond to types, proofs correspond to terms, provability corresponds to inhabitation, (...) class='Hi'>proof normalization corresponds to term reduction, etc. But there is more to the isomorphism than this. For instance, it is an old idea---due to Brouwer, Kolmogorov, and Heyting---that a constructive proof of an implication is a procedure that transforms proofs of the antecedent into proofs of the succedent; the Curry-Howard isomorphism gives syntactic representations of such procedures. The Curry-Howard isomorphism also provides theoretical foundations for many modern proof-assistant systems (e.g. Coq). This book give an introduction to parts of prooftheory and related aspects of type theory relevant for the Curry-Howard isomorphism. It can serve as an introduction to any or both of typed lambda-calculus and intuitionistic logic. Key features - The Curry-Howard Isomorphism treated as common theme - Reader-friendly introduction to two complementary subjects: Lambda-calculus and constructive logics - Thorough study of the connection between calculi and logics - Elaborate study of classical logics and control operators - Account of dialogue games for classical and intuitionistic logic - Theoretical foundations of computer-assisted reasoning · The Curry-Howard Isomorphism treated as the common theme. · Reader-friendly introduction to two complementary subjects: lambda-calculus and constructive logics · Thorough study of the connection between calculi and logics. · Elaborate study of classical logics and control operators. · Account of dialogue games for classical and intuitionistic logic. · Theoretical foundations of computer-assisted reasoning. (shrink)
Proof-theory has traditionally been developed based on linguistic (symbolic) representations of logical proofs. Recently, however, logical reasoning based on diagrammatic or graphical representations has been investigated by logicians. Euler diagrams were introduced in the eighteenth century. But it is quite recent (more precisely, in the 1990s) that logicians started to study them from a formal logical viewpoint. We propose a novel approach to the formalization of Euler diagrammatic reasoning, in which diagrams are defined not in terms of (...) regions as in the standard approach, but in terms of topological relations between diagrammatic objects. We formalize the unification rule, which plays a central role in Euler diagrammatic reasoning, in a style of natural deduction. We prove the soundness and completeness theorems with respect to a formal set-theoretical semantics. We also investigate structure of diagrammatic proofs and prove a normal form theorem. (shrink)
Linear Logic is a branch of prooftheory which provides refined tools for the study of the computational aspects of proofs. These tools include a duality-based categorical semantics, an intrinsic graphical representation of proofs, the introduction of well-behaved non-commutative logical connectives, and the concepts of polarity and focalisation. These various aspects are illustrated here through introductory tutorials as well as more specialised contributions, with a particular emphasis on applications to computer science: denotational semantics, lambda-calculus, logic programming and (...) concurrency theory. The volume is rounded-off by two invited contributions on new topics rooted in recent developments of linear logic. The book derives from a summer school that was the climax of the EU Training and Mobility of Researchers project 'Linear Logic in Computer Science'. It is an excellent introduction to some of the most active research topics in the area. (shrink)
The Unprovability of Consistency is concerned with connections between two branches of logic: prooftheory and modal logic. Modal logic is the study of the principles that govern the concepts of necessity and possibility; prooftheory 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. (shrink)
A variety of projects in prooftheory of relevance to the philosophy of mathematics are surveyed, including Gödel's incompleteness theorems, conservation results, independence results, ordinal analysis, predicativity, reverse mathematics, speed-up results, and provability logics.
1. Pohlers and The Problem. I first met Wolfram Pohlers at a workshop on prooftheory organized by Walter Felscher that was held in Tübingen in early April, 1973. Among others at that workshop relevant to the work surveyed here were Kurt Schütte, Wolfram’s teacher in Munich, and Wolfram’s fellow student Wilfried Buchholz. This is not meant to slight in the least the many other fine logicians who participated there.2 In Tübingen I gave a couple of survey (...) lectures on results and problems in prooftheory that had been occupying much of my attention during the previous decade. The following was the central problem that I emphasized there: The need for an ordinally informative, conceptually clear, proof-theoretic reduction of classical theories of iterated arithmetical inductive definitions to corresponding constructive systems. As will be explained below, meeting that need would be significant for the then ongoing efforts at establishing the constructive foundation for and proof-theoretic ordinal analysis of certain impredicative subsystems of classical analysis. I also spoke in Tübingen about.. (shrink)