Tim Button

*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*.

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*.

*Metatheory* pdf

*Metatheory* LaTeX source code

*Metatheory* is released under a Creative Commons license (CC BY 4.0; full details are available here). The following is a human-readable summary of (and not a substitute for) that license. You are free to:

*Share*: copy and redistribute the material in any medium or format

*Adapt*: remix, transform, and build upon the material for any purpose, even commercially.

Under the following terms:

*Attribution*: You must give appropriate credit, provide a link to the license, and indicate if changes were made. You may do so in any reasonable manner, but not in any way that suggests the licensor endorses you or your use.

*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.

**2018**

License changed to CC BY 4.0

Main release uses Libertinus fonts (open source and available here)

Two rules renamed: ⊥I as ¬E, and ⊥E as X

**2017**

Main release uses XeLaTeX and Arno Pro fonts

Support for LaTeX and Computer Modern via metatheory-basic.sty

Fixed minor mistakes

**2014**

Fixed minor mistakes

**2013**

First release; license Creative Commons Attribution-ShareAlike 3.0

Last modified 31 Oct 2018