The Open Logic Project, instigated by Richard Zach (Calgary) and including Aldo Antonelli (UC Davis), Andrew Arana (UIUC), Jeremy Avigad (Carnegie Mellon), Gillian Russell (Wash U. St. Louis, soon to be UNC), Nicole Wyatt (Calgary), and Audrey Yap (Victoria), and a student assistant, has created the Open Logic Text, an open-source, collaborative logic text and all around very cool idea. From the “about ” page of the project:
The Open Logic Text is an open-source, collaborative textbook of 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, 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.
Since it is an open-source project, it is available for free to use and modify and rearrange as needed, provided that appropriate credit is given.
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 results).
You can read more about it and download it at the Open Logic Project site.
Not to be neglected is the well-designed logo:
though I can’t help but think that given the anarchical qualities of the open-source approach that this would have worked, too:
(via Richard Zach’s Logic Blog)