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 set theory, the syntax and semantics of propositional and first-order logic, proof systems (axiomatic derivations, sequent calculus, natural deduction, and tableaux), soundness and completeness theorems, model theory, computability theory (recursive functions, Turing machines, lambda calculus), Gödel’s incompleteness theorems, modal logic, intuitionistic logic, counterfactuals, and second-order logic. The project remains under continuous development, and we plan to improve and add to the coverage.
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. A selection of textbooks covering specific topics is available as well.
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.
- If you use the material in a class, please fill out the Adoptions Form.