This module is an exploration of the metatheory of propositional and first-order logic - i.e. rather than just proving statements in these systems, we will use mathematical tools to prove facts about them from the outside.

In order to better understand how we prove things about as opposed to within a logical system, we will first study elementary set theory and inductive definitions. Along the way, we will encounter developments such as Russell's paradox and the distinction between countable and uncountable sets, both of which played a role in the crisis in the foundations of mathematics in the early 20th century.

We will then consider Tarski’s definition of truth in a model which was a key step in convincing philosophers and mathematicians that truth was not an inherently paradoxical notion. Next, we will develop a method for adding new constants symbols to a language to build models by purely linguistic means. This will enable us to prove the Completeness Theorem for first-order logic - i.e. every logically true statement is provable. After this, we will obtain the Compactness Theorem as a corollary and use it show that certain mathematical notions cannot be captured in first-order logic.