Skip to main content

Introduction to Formal Proof:  2015-2016

Lecturer

Degrees

Preliminary ExaminationsComputer Science

Term

Learning outcomes

1. Familiarity with the idea of structured formal proof (a) in propositional logic (b) in first-order predicate logic (c) in a familiar first-order equational theory

2. Familiarity with the notions of soundness and completeness as relationships between logics (presented as inference systems), and their semantics (presented as mathematical structures).

3. Familiarity with the distinction between proofs in a logic and proofs about a logic and its semantics.

4. Adeptness at finding fully formal proofs in a small number of deductive inference systems.

5. An understanding of the relationship between (on the one hand) completely formal proofs and (on the other hand) rigorous proofs of the kind that students are routinely expected to read and to present.

6. Preparedness for the second year course Logic & Proof which treats matters of soundness and completeness rigorously.

Synopsis

Note that this is not an ordered week-by-week synopsis. A synopsis of the lecture slide titles that reflects the order in which material will be presented can be found in the Course Materials.
1. Introduction to Logic and Proof
• What is a formal proof?
• Propositional language and truth-valued interpretations.
• Tautology/validity and satisfiability.
2. Propositional Natural Deduction
• Sequent presentations of natural deduction rules.
• Sequent tree presentations of ND proofs.
• Backward proof discovery.
• Theorems as derived rules.
• Notions of soundness and completeness
– Entailment.
– Statement of soundness and completeness theorems for ND.
3. First Order (Predicate) logic
• Predicate language, quantifiers and substitution.
• Signatures, models, and evaluation.
• Natural Deduction rules for predicate calculus.
4. Equational extensions to Predicate Logic
• Elementary group theory.
• Natural numbers and lists and their rules of induction.
• Function definitions as axioms.

Syllabus

Propositional Logic

  1. Natural Deduction
  2. Semantics
  3. Soundness of natural deduction rules
  4. Definition of completeness of deduction rules
  5. Sequent presentations of deduction rules

First Order (Predicate) Logic

  1. Predicate language (including definition of free variable, substitution)
  2. Semantics (including signatures, domains of discourse, evaluation of quantified forms)
  3. Deduction rules and proofs in predicate logic
  4. Augmenting First Order Logic with equational theories

Reading list

  1. Logic in Computer Science (Huth and Ryan, CUP, 2008) will suffice as a primary background text, though it is much more comprehensive than is needed in this first course, and the lectures do not follow it in detail.
  2. Another very good background text on proof is Proof and Disproof in Formal Logic (Richard Bornat, OUP, 2005). It is also the best discursive introduction to the Jape proof calculator.
    Richard's explanation of the difference between classical and intuitionistic logic will interest the philosophically minded, though it is not relevant to this course. His material on formal program proof is also very good.

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.