Introduction to Formal Proof: 20172018
Lecturer 

Degrees 

Term 
Trinity Term 2018 (10 lectures) 
Learning outcomes
1. Familiarity with the idea of structured formal proof (a) in propositional logic (b) in firstorder predicate logic (c) in a familiar firstorder equational theory2. 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
• Notions of soundness and completeness
• Signatures, models, and evaluation.
• Natural Deduction rules for predicate calculus.
Syllabus
Propositional Logic
 Natural Deduction
 Semantics
 Soundness of natural deduction rules
 Definition of completeness of deduction rules
 Sequent presentations of deduction rules
First Order (Predicate) Logic
 Predicate language (including definition of free variable, substitution)
 Semantics (including signatures, domains of discourse, evaluation of quantified forms)
 Deduction rules and proofs in predicate logic
 Augmenting First Order Logic with equational theories
Reading list
 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.
 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.