Introduction to Proof Systems: 20242025
Lecturer  
Degrees  Preliminary Examinations — Computer Science and Philosophy 
Term  Trinity Term 2025 (12 lectures) 
Overview
Logic plays an important role in many disciplines, including Philosophy and Mathematics, but it is particularly central to Computer Science and sometimes referred to as the calculus of Computer Science. The central problem in logic is to determine whether a given statement is true, and to provide proofs for true statements.This course is an introduction to mathematical and computational logic, with a particular emphasis on formal proof systems. Its goal is to provide a broad introduction to the subject and to equip students with the knowledge and skills required for subsequent courses heavily relying on Logic in Parts AC, such as "Logic and Proof", "Computational Complexity", "ComputerAided Formal Verification", "Automata Logic and Games", and "Knowledge Representation and Reasoning". We will specifically focus on the syntax and semantics of propositional logic, firstorder logic, and secondorder logic; various different proof systems for those logics; and how to translate problems formulated in natural language into logical formulas.
Syllabus
 Syntax and semantics of propositional logic, firstorder logic, and secondorder logic
 Expressing mathematical and computational problems in logic
 Normal forms of logical formulal
 Truth tables
 The satisfiability problem
 Axiomatisation
 Equational reasoning
 Natural deduction
 Sequent calculus
 Resolution
 Compactness
 Herbrand's theorem
 The downward and upward Löwenheim–Skolem theorems
 Lambda calculus
Reading list
Primary texts and resources:
 Schöning, U., 2008. Logic for computer scientists. Springer Science & Business Media
 Mancosu, P., Galvan, S. and Zach, R., 2021. An introduction to proof theory: Normalization, cutelimination, and consistency proofs. Oxford University Press.
Freely available online from inside the University network: https://academic.oup.com/book/4213  The Stanford Encyclopedia of Philosophy. URL: https://plato.stanford.edu/
Leisure texts:

Hofstadter, D.R., 1999. Gödel, Escher, Bach: an eternal golden braid. Basic books.

Doxiadis, A., Papadimitriou, C., Papadatos, A. and Di Donna, A., 2022. Logicomix. Vuibert.
Taking our courses
This form is not to be used by students studying for a degree in the Department of Computer Science, or for Visiting Students who are registered for Computer Science courses
Other matriculated University of Oxford students who are interested in taking this, or other, courses in the Department of Computer Science, must complete this online form by 17.00 on Friday of 0th week of term in which the course is taught. Late requests, and requests sent by email, will not be considered. All requests must be approved by the relevant Computer Science departmental committee and can only be submitted using this form.