Gottfried Wilhelm Leibniz
an open course in logic developed by
Johan van Benthem, Hans van Ditmarsch, Jan van Eijck, Jan Jaspars
This is the homepage of the Logic in Action Open Course Project. This project was developed to provide a modern introduction to the field of logic with topics reflecting both its mathematical essentials and a broad view of its interdisciplinary role.
The material was written for elementary and intermediate courses in logic, to assist teachers and also intrepid readers engaging in self-study. All material is freely available.
For an overview of the ideas behind the course as well as some experiences of its developers and teachers, see the paper Logic in Action: An Old Discipline With a New Twist.
Below you will find the individual chapters of our self-contained introduction to logic.
Academic courses that have used and tested this material were given at:
Stanford University, USA
University of Sevilla, SP
The course is also part of the Stanford Online Highschool Curriculum.
The book is used as a course text in the Discrete Structures course at the Department of Computer Science, National University of Ireland, Maynooth, Co. Kildare.
A pdf version of the textbook can be downloaded from here.
Links to individual chapters of the manuscript are given below.
There are also slides for teaching available, in English and in Spanish (made by Fernando Velazquez Quesada).
Further exercise material for the chapters (courtesy of Dora Achourioti, AUC) can be found here.
Online exercises in modal logic (an important topic in the course) can be found here.
The development of this site is co-funded by the Center for Creation, Content and Technology, which is part of the Netherlands Network for Humanities, Social Sciences and Technology, with a subsidy from Platform Beta Techniek.
Gottfried Wilhelm Leibniz
In science, logic means "the study of valid reasoning", and for centuries it has been a philosophical discipline. Nowadays, in the information era, it is part of the scientific background assumed by researchers from a wide diversity of scientific backgrounds such as mathematics, computer science, linguistics, cognitive science and economics. In this first chapter a variety of examples of valid and invalid reasoning are presented and informally discussed. The material is presented against a historical canvas of the development of logic, both in the western and in the eastern world.
Propositional logic is a purely sentential system originating with the Stoic philosophers. The first completely formal version of propositional logic was presented around 1850 by George Boole (picture), and published in his famous 'The Laws of Thought'. Although the language of propositional logic is simple, the logic itself is very expressive and powerful. This is witnessed by the fact that all digital computation can be modeled as propositional reasoning (although, admittedly, this is a rather low-level representation).
Aristotle
In this chapter we go back to antiquity. Syllogistics is a logic of quantified expressions which was introduced by Aristotle (400BC). Syllogistics has dominated the study of logic in the western world until the 19th century. Since the second half of the 19th century syllogistics is mathematically well-understood. We introduce and explain a system which makes use of so-called Venn-diagrams (after the British mathematician John Venn). In addition to this, we discuss how syllogistics can be modeled as propositional reasoning. Syllogistics corresponds to a natural fragment of propositional logic for which validity can be computed at low computational cost. Whether an efficient validity testing method for full propositional logic exists is still unknown, although it is widely believed that this is not the case.
Gottlob Frege
In the system of predicate logic, quantification is combined with the sentential operations of propositional logic. Unlike syllogistics, predicate logic allows multiple quantification, combined with the expression of relations between objects. The German philosopher Gottlob Frege proposed this formalism in 1878, as a Begriffsschrift (concept language) in which, so he hoped, all mathematical reasoning could be represented in a precise formal manner. Nowadays, predicate logic is the most common logical system, for representing reasoning in mathematics and in many other fields.
Jaakko Hintikka
This chapter introduces the logic of knowledge, otherwise called epistemic logic. The essential difference with the classical systems of part 1 is that in epistemic logic the reasoner(s), or agent(s), are incorporated within the system. Epistemic logic allows one to formalize the reasoning of an agent about his own knowledge and ignorance, as well as about the knowledge and ignorance of other agents. Epistemic logic goes back to the work of the Finnish philosopher Jaakko Hintikka (picture) in the early 1960s. In this chapter we also discuss recent developments, culmi nating in systems that are able to model various acts of communication between agents and their effects.
Vaughan Pratt
This chapter introduces dynamic logic, a system that was introduced in computer science for reasoning about the behaviour of computer programs, by Vaughan Pratt and others, in the 1970s. Later on, it turned out that dynamic logic has other applications as well. Dynamic logic can be viewed as a general logic of actions and their effects. It allows us to not only reason about what agents know and say, but also about what they do, and what the effects of these actions are.
Ernst Zermelo
Games have always played an important role in the history of logic. Many sorts of interactive games, of two opposing players, have been used as tools for demonstrating the validity or invalidity of inferences, or for determine the truth or falsity of utterances (in so-called evaluation games). We discuss several examples of applications of games to the classical systems of part 1, as well as to the systems in this part. Next, we focus on game theory, as studied in economics and the social sciences as formal models of human social behaviour, and explain how this relates to logic games.
Evert Willem Beth
This chapter explains the so-called tableau-system of Evert Willem Beth (1955, picture). Tableaus were meant as a general method to decide validity of inferences, in propositional logic and predicate logic. We show such systems work, for propositional logic, for predicate logic, and for single agent epistemic logic. The tableau method is a systematic search and construction method for counter-models. If such a counter-model can be constructed, this demonstrates the invalidity of an inference. Validity of an inference can be demonstrated by showing that counter-models do not exist. Tableau construction is a complete method for the logics which are discussed in this chapter: for every valid inference in propositonal logic, predicate logic and single agent epistemic logic, the tableau method can demonstrate that no counter-models exist.
Gerhard Gentzen
The tableau method for deciding the validity of logical arguments is a useful analysis tool, but it is not quite faithful to the way humans reason in practice. In this chapter we introduce a system of reasoning called natural deduction, with rules that are meant to reflect the formal structure of mathematical proofs as you can find them in textbooks. These rules are also quite close to the way sound reasoning proceeds in daily life. We discuss systems for propositional logic, predicate logic and a well known system of arithmetic as an extension of predicate logic. The systems discussed in this chapter go back to the work of the influential German logician and mathematician Gerhard Gentzen (picture) in the 1930s, and were streamlined later by the Swedish logician Dag Prawitz (1960s).
Alain Colmerauer
In this chapter it is explained how predicate logic can be used for programming. The chapter gives an introduction to concepts used in automating logical theorem proving. This leads to computational tools underlying the well known logic programming language Prolog, popular in AI an in computational linguistics. The inferential mechanism behind Prolog is called SLD-resolution. This is the reasoning engine for a natural fragment of predicate logic (the so-called Horn-fragment).
Georg Cantor
This chapter explains the basics of formal set notation, and gives an introduction to relations and functions. The chapter ends with a short account of the principle of proof by mathematical induction.