Tim Button

About Metatheory

Metatheory is an introduction to the metatheory of truth-functional logic, also known as the propositional calculus. It is the textbook for a Cambrige Part IB course on metatheory, and it continues immediately from the textbook for the first-year course in formal logic, forallx: Cambridge.

The current version of Metatheory was released on 30 September 2017.

Given the license, you can print as many copies of this as you like, or use the source code to make derivative works, provided you respect various conditions. But if you do use Metatheory, please let me know! I can be contacted at tecb2 at cam dot ac dot uk.

Available downloads

Metatheory pdf
Metatheory LaTeX source code

More about Metatheory

Metatheory does not itself contain an account of truth-functional logic, but instead assumes a prior understanding. More specifically, this book assumes a thorough understanding of the syntax, semantics and proof-system for TFL (truth-functional logic) that is presented in forallx: Cambridge. There is nothing very surprising about the syntax or semantics of TFL, and the proof-system is a fairly standard Fitch-style system.

Metatheory does not, though, presuppose any prior understanding of (meta)mathematics. Chapter 1 therefore begins by explaining induction from scratch, first with mathematical examples, and then with metatheoretical examples. Each of the remaining chapters presupposes an understanding of the material in Chapter 1.

Chapter 2 covers results relating to substitution, including Interpolation and Duality. Chapters 3 and 4 cover normal form theorems and expressive adequacy. Chapters 5 and 6 cover soundness and completeness.

One idiosycracy of Metatheory is worth mentioning: it uses no set-theoretic notation. Where I need to talk collectively, I do just that, using plural locutions.

Metatheory is released under a Creative Commons license. In brief, this means that you can use the texts free of charge. But you can also download the source files, make changes to them, and make a version of the textbook suitable for your own requirements.

About the license

Metatheory is released under a Creative Commons license (Attribution-ShareAlike 3.0).

You are free to copy this book, to distribute it, to display it, and to make derivative works, under the following conditions: (a) Attribution. You must give the original author credit. (b) Share Alike. If you alter, transform, or build upon this work, you may distribute the resulting work only under a license identical to this one.

For any reuse or distribution, you must make clear to others the license terms of this work. Any of these conditions can be waived if you get permission from the copyright holder. Your fair use and other rights are in no way affected by the above.

This is a human-readable summary of the full license, which is available on-line at creativecommons.org.

Last modified 30 Sep 2017