Skip to main content

Introduction to Proof Systems:  2023-2024

Lecturer

Degrees

Preliminary ExaminationsComputer Science and Philosophy

Preliminary ExaminationsComputer Science

Preliminary ExaminationsMathematics and Computer Science

Term

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 A-C, such as "Logic and Proof", "Computational Complexity", "Computer-Aided Formal Verification", "Automata Logic and Games", and "Knowledge Representation and Reasoning". We will specifically focus on the syntax and semantics of propositional logic, first-order logic, and second-order 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, first-order logic, and second-order 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, cut-elimination, 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.

Feedback

Students are formally asked for feedback at the end of the course. Students can also submit feedback at any point here. Feedback received here will go to the Head of Academic Administration, and will be dealt with confidentially when being passed on further. All feedback is welcome.

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.