On successful completion of this module students will be able to

Construct very simple Turing machine programs.

Construct proofs of formulae in propositional and first-order
logic, including resolution, the Deduction Theorem, and derived
rules.

Determine the solvability or otherwise of various
computational problems.

Extend their knowledge of mathematical logic
or proceed to further study of the subject.

Module Content

Turing machines: the basic undecidability results.

Zero-order logic with resolution
methods and Frege's axioms. The deduction theorem.
Completeness theorems.

First-order logic, the Deduction Theorem, derived
rules, models, prenex form, Herbrand
models, and completeness.

Ultraproducts (if time permits).

Peano arithmetic, representability of semicomputable
functions, and theorems of Gödel, Tarski, and Church.

Recursive functions and Gödel's first and second
incompleteness theorems.

Module Prerequisite

None beyond SF level modules.

Assessment Detail

This module will be examined
in a 2-hour examination in Trinity term.
Fortnightly written assignments will count 10%, and
90% for the final.
Supplementals are normally not available in this module (except in the
case of JS TSM pattern A students).