The Open Logic Text is an open-source, modular, collaboratively authored collection of teaching materials for formal (meta)logic and formal methods, starting at an intermediate level (i.e., after an introductory formal logic course). It is aimed at a non-mathematical audience (in particular, students of philosophy and computer science), but is completely rigorous.
Currently it covers the syntax and semantics of first-order logic, sequent calculus, natural deduction, soundness and completeness theorems, rudiments of model theory, computability theory, and incompleteness. The project remains under continuous development, and we plan to improve and add to the coverage. Additional topics which we have short-term plans to cover are computability via Turing machines, additional coverage of topics in model theory, modal logic, as well as material on applications of logic in philosophy, such as on paradoxes, metaphysics, philosophy of language, and philosophy of mathematics. Some of the material is written specifically for this project, while other material is converted from existing lecture notes. We also plan to add new features throughout, such as a glossary and index, historical notes, and sections covering further reading.
The project operates in the spirit of open source. Not only is the text available for free, we provide it in source LaTeX format under a Creative Commons Attribution license, which gives anyone the right to download, use, modify, re-arrange, convert, and re-distribute our work, as long as they give appropriate credit. It is an open educational resource.
In addition, the text has the following features:
- Modular: Topics are divided into section-sized chunks, allowing users to select which topics “their” version of the text will cover, in what order, in what depth, and including which exercises.
- Configurable: Typesetting and notation are configurable as much as possible, so that individual preferences can easily be accommodated. For instance, users can choose—without having to alter the text directly—arrow or horseshoe for the conditional symbol, but also between Latin and Greek letters for formulas, and even between “formula” and “wff” as the term used throughout the text.
- Adaptable: Alternative treatments of the same topics can be substituted for each other to tailor the text to a specific audience (e.g., results can be made relative to different proof systems as students at different institutions use different introductory texts).
- Integrated: Uniform conventions in the LaTeX source and the use of stock and custom packages facilitate the seamless integration of different authors’ contributions, and the production of bibliographies, indices, etc.
- Open and Collaborative: Users can contribute their own expositions and exercises, report “bugs” (typos, errors and omissions, etc.), and request “features” (additional material). The text is hosted on the GitHub open-source development platform, which also provides the collaboration functions.
The project team consists of Andy Arana, Jeremy Avigad, Walter Dean, Gillian Russell, Nicole Wyatt, Audrey Yap, and Richard Zach.
We would like to gratefully acknowledge the support of the University of Calgary Faculty of Arts and the Campus Alberta OER Initiative.
- Download PDFs or source code.
- Learn more on the project wiki.
- Browse or download the source code from GitHub.
- Watch on GitHub
- Follow on Twitter
- Like on Facebook
- Add on Google+
- Subscribe to the site feed
- Subscribe by email