Syllabuses for MSc in Logic 2002-03, Department of Mathematics, Univ. of Manchester, UK

Credit Rating: 15
Level: M.Sc.
Delivery: Semester One
Lecturer: Prof. Mike Prest (Room 15.11, Telephone 55875, email:mprest@ma.man.ac.uk)

General Description
What do we mean by saying that a mathematical statement is true? What exactly is a mathematical proof? Can mathematics be reduced to computer programming? These are some of the questions which motivate the study of mathematical logic. Predicate logic provides remarkable insight into these questions by providing a precise formalism capable of expressing all ordinary mathematics. The module will lead up to a proof of the completeness theorem, a striking result of Kurt Gödel (1930), which demonstrates the equivalence of a natural notion of logical consequence with provability in a certain axiomatic system.

Aims
To introduce students to the formal notions of language, proof, semantics, and completeness with quantificational logic, in order to:
· improve their understanding and appreciation of the foundations of mathematics and
· provide the necessary background knowledge for later logic course units.

Learning Outcomes
On successful completion of the course unit the students will
· appreciate how arguments involving predicates can be formalised semantically and syntactically and how these are connected (via the Completeness Theorem)
· in simple cases be able to show that 'A follows from B' both by giving a semantic argument and by constructing a formal proof.
· in simple cases be able to show that 'A does not follow from B' by using semantics.

Prerequisites
Some familiarity with the propositional calculus. (This may be gained by study of a chapter(s) on propositional calculus up to the completeness theorem from one of the many logic textbooks, such as the ones listed below or alternatively the first 3 weeks of MT5181).

Content
Introduction. Review of propositional logic. Motivation for the study of predicate logic with examples of reasoning with quantifiers. [2]
Truth. Languages for predicate logic. Signatures and structures. Formulae, sentences and Tarski's definition of Truth. Logical consequence, logical equivalence and logical validity. Theories and models. [9]
Proof. An axiom system for predicate logic. The Soundness Thoerem. Consistency. [6]
Completeness. The completeness theorem for predicate logic. Simple applications. [7]
Models. An introduction to model theory. The compactness and Lowenheim-Skolem theorem with applications. [6]

Teaching and Learning Methods
30 lectures, 6 examples classes, and assigned reading.

**Learning hours**
Activity	Hours
Staff/student contact	36
Private study	108
Total hours	144

**Assessment**
Assessment activity	Length Required	Weighted within unit
Two take home tests		20%
End of semester examination	2½ hours	80%

Core Learning Materials
Reading Assignments
Some of the details concerning languages for predicate logic with function symbols and equality and the proof of the completeness theorem will not be covered in lectures but left as reading assignments.

Textbooks
H.B. Enderton, A Mathematical Introduction to Logic, Academic Press.
D. van Dalen, Logic and Structure, Springer-Verlag, 3rd edition 1997.
A.G. Hamilton, Logic for Mathematicians, Cambridge University Press, revised edition 1988.

Credit rating: 15
Level: M.Sc.
Delivery: Semester One
Lecturer: Dr. George Wilmers (Room 15.07, Tel: 55878, email: george@ma.man.ac.uk)

Inductive Logic has traditionally been considered the poor relation of its deductive counterpart, and in terms of the development of the subject to date, such a view may seem well justified. In terms of its intrinsic philosophical importance however, or of its potential applicability to problems of artificial intelligence, the situation is quite different. The course will give a general critical introduction to classical results on inductive logic and prior probability, including an account of the interplay of key mathematical and philosophical ideas.

Aims

To introduce the student to the principal ideas and problems of inductive logic.

Learning Objectives

The student will acquire a good understanding of classical approaches to inductive logic including Dutch book arguments, Carnap’s continuum, and de Finetti’s theorem.

Prerequisites

Some familiarity with propositional and predicate calculus; the course will be structured so that students taking MT5151 and MT5181 in parallel will acquire the necessary background knowledge, but these courses are not otherwise prerequisites. Some familiarity with the most basic concepts of probability theory and of mathematical analysis will be assumed.

Content

1.Belief as a probability function on the propositional calculus. The axioms and simple consequences. Justifications for belief as probability. Dutch book arguments. Cox’s Theorem.

4.The Johnson-Carnap principles and Carnap’s theory of confirmation. The l-continuum. The principle of instantial relevance. Criticisms.

5.Exchangeable sequences. De Finetti’s theorem and its consequences. Dirichlet priors. The problem of the prior probability of universal statements.

There is no recommended textbook covering all the material in this course, but much of the syllabus is covered in Chs. 2, 3, 11 and 12 of the Uncertain Reasoner’s Companion by J.B. Paris, Cambridge University Press.

Two take-home tests together worth 20% of the final mark, and a 2½ hour end of semester examination for the remaining 80%.

Credit rating: 15
Level: MSc/ Level 4
Delivery: Semester One
Lecturers: Andrea Schalk and Harold Simmons

General Description
This module describes some of the mathematics that is helping us to understand 'computation'. Most of this has been developed quite recently, and often for reasons unconnected with 'computation'. The module shows how different areas of mathematics can interact to enhance our understanding of the separate parts.

Aims
To describe some mathematics that has risen out of the study of computation; to show how new mathematical theories developed for one purpose can be useful for another; to compare several different theories of computation.

Learning Outcomes
At the end of this module students will understand how the notions of computation can be formalized: have seen mathematical theories modelling various aspects of computation; be able to solve problems in various mathematical areas, and write up their solutions; have carried out independent reading in the context of the above.

Prerequisites
A good grounding in mathematics. Some familiarity with parts of mathematical logic in the broad will help but this is by no means essential. Although the topics treated have some connections with Computation, Computer Science, and Numerical Analysis, no familiarity with any of these is required.

Content
The module forms an introduction to four or five different topics together with an account of how these interact. The topics will be chosen from the following list to suit the interests of the participants. Each section comprises approximately five hours of material. The remaining lectures will be spend on drawing out the connections between the topics.

Category theory: Basics, functors and natural transformations, limits and colimits, cartesian closed categories.
Various l-calculi: Untyped, simply typed, and typed specifically for the natural numbers. The syntax, reduction mechanism, and typing discipline of these. The simulation of natural number gadgetry within these systems.
Forms of recursion: The primitive recursive functions, above and below these. The extended Grzegorczyk hierarchy. Measures of complexity.
While loop programs: Basic constructs, denotational semantics, how to capture various recursion operators.
Domain theory: Recursion operators, fixed point characterization, the simple domains.
Categorical semantics: How the various syntactic calculi considered above can be modelled within appropriate categories of domains and other things.

Teaching and Learning methods:
28 lectures, 8 examples classes, and assigned reading.

**Learning Hours**
Activity	Hours
Private study	104
Assignments	10
Staff/student contact	36
Total	150

**Assessment**
Assessment Activity	Length	Weighted within unit
Two take home assignments		20
Examination	2½ hours	80

Core Learning Material:
A full set of notes for each of the sections will be available. There will also be a suggested selection of textbooks and references.

Credit Rating: 15
Level: M.Sc.
Delivery: Semester One
Lecturer: Prof. J. Paris (Room 15.09, Telephone 55880, email:jeff@ma.man.ac.uk).

General Description
Over the past fifteen years considerable effort has been put into developing computers which can reason intelligently, and come to sensible conclusions, on the basis of information which is inexact, incomplete and possibly even inconsistent, rather in the way that we seem to be able to. This has led to the development of many new ideas about reasoning in particular the development of non-monotonic logic(s) for reasoning about what is ‘usually’ true.

This course will present the mathematics of one of these approaches to reasoning and show that despite its divergence from classical, exact, reasoning they are both closely related.

Aims
Apart from providing practical knowledge of default reasoning useful for those students intending to embark on a career in Information Technology the course provides, via a number of elegant examples, insight and understanding into the way aspects of reasoning may be modelled and analysed within a logical framework.

Learning Outcomes
On successful completion of the course unit students will have a clear understanding of how reasoning (in particular default reasoning) can be modelled within a logical framework and a detailed technical knowledge of the mathematics of one such approach (rational consequence).

Teaching and Learning Methods
30 lectures, 6 examples classes, and assigned reading.

**Learning hours**
Activity	Hours
Staff/student contact	36
Private study	108
Total hours	144

**Assessment**
Assessment activity	Length	Weighted within unit
Two coursework assignments		20%
End of semester examination	2½ hours	80%

Core learning materials
Textbooks
The material in this course is drawn from a wide range of sources. I would not advise the student to buy any books for the course although the following will overlap with some of the material covered.
J. Pearl, Probabilistic Reasoning in Intelligent Systems: Networks of Plausible Inference, Morgan Kaufman, 1988.
P.Gardenfors, Knowledge in Flux, Cambridge, MIT, 1990.
D. Lehmann and M. Magidor, What does a Conditional Knowledge Base Entail? Artificial Intelligence, 68 (1992), 1-60.
H. Rott, Change, Choice and Inference: A Study of Belief Revision and Nonmonotonic Reasoning, Oxford Logic Guides, number 42, Oxford University Press, 2001.

Credit Rating: 15
Level: M.Sc.
Delivery: Semester Two
Lecturer: Jeff Paris (Room 15.09, Telephone 55880, email:jeff@ma.man.ac.uk)

General Description
Non-standard logics are logics which capture other features of arguments, or reasoning, beyond those expressible in the basic, classical, propositional and predicate calculi. As such they have always been of direct interest and relevance to Philosophers and Logicians.

However, this subject has taken off in the last 25 years or so because of the need in Computer Science (and especially in the sub-area of Information Technology) to formalise a range of patterns of reasoning for use in so called 'intelligent computers'.

In this course we shall look at three such families of (propositional) logics, modal, many valued (or 'fuzzy') and probabilistic. Our approach will, however, remain very much within the tradition of mathematical logic and philosophy, concentrating on understanding the key ideas and theorems (in particular deriving completeness theorems), rather than studying practical IT applications.

Aims
The aim of this course is to expose the students to the formal mathematical and philosophical aspects of a range of non-standard logics which are currently of importance in IT.

Learning Outcomes
On successful completion of the course unit students will be able to
· appreciate how non-standard logics can be developed and used to formalise various patterns of reasoning,
· be able to construct simple (formal) proofs within the non-standard logics studied,
· understand the proofs of the relevant completeness theorems and be able to apply these theorems to give semantic arguments for, or against, formal derivability.

A good working knowledge of the classical propositional calculus, such as that given by MT5181, will be assumed.

Content
Modal Logic: Necessity and possibility. The systems K,T,D,B,S4,S5. Examples of proofs, normal forms. Frames and semantics. Completeness Theorems of K,T,D,B,S4,S5. Epistemic Logic, multi-agent systems and common knowledge. Temporal Logic. Connection to Intuitionistic Logic. [13]
Many Valued Logic: Fuzzy Logic, degrees of truth, Truth Functionality and Ling's Theorem. Lukasiewicz, Product and Gödel Logics. McNaughton's Theorem, and the Completeness Theorem for Lukasiewicz Logic. [9]
Probability Logic: Probabilistic knowledge bases, inference processes. Common sense principles of uncertain reasoning. The formal system I. [5]

Teaching and learning methods:
24 lectures, 7 examples classes, and assigned proofs for the students to fill in for themselves.

**Learning hours**
Activity	Hours
Staff/student contact	35
Private study	112
Total hours	147

**Assessment**
Assessment activity	Length required	Weighted within unit
Two take home tests		20%
End of semester examination	2½ hours	80%

Core learning materials
Textbooks
The course is self contained and you will not be required to consult any books. However the following cover some of the same material as the course and may provide interesting complementary reading:

G.E. Hughes & M.J. Cresswell, A Companion to Modal Logic, Methuen.
G.E. Hughes & M.J. Cresswell, An Introduction to Modal Logic, Methuen.
B.F. Chellas, Modal Logic: An Introduction, Cambridge University Press.
P. Hájek, Metamathematics of Fuzzy Logic, Kluwer, 1998.
J.B. Paris, The Uncertain Reasoner's Companion, Cambridge University Press, 1994.

Credit Rating: 15
Level: M.Sc.
Delivery: Semester Two
Lecturer: George Wilmers (Room 15.07, Telephone 55878, email:george@ma.man.ac.uk).

General Description
Can a computer be programmed to generate all true statements of mathematics and no false ones? An extraordinary result, proved by Kurt Gödel in 1931, shows that even if we restrict ourselves to the most fundamental part of mathematics, namely statements about the natural numbers, the answer to the above question is no. Moreover Gödel’s method is such that given any “mechanical procedure” for generating true statements about the natural numbers we are actually able to construct a true statement of numbers which will not be generated by that procedure.

Gödel’s work stands as one of the landmarks of 20th century thought and has a significance which reaches well beyond mathematics. The course unit will be centred on proofs of Gödel’s two incompleteness theorems and will examine some of their principal applications.

Aims
To introduce the student to Gödel’s two incompleteness theorems and to their most important corollaries.

Learning Outcomes
On successful completion of the course unit students will
· be familiar with the notion of recursive function
· have developed a facility in the manipulation and application of these functions, with particular emphasis on applications to logic and decision problems.

Content
The completeness theorem for the predicate calculus: a review. First order theories. [2]
Recursive functions and relations. Basic properties. Primitive recursion. Closure under bounded quantification. [4]
Gödel’s b-function. Coding of finite sequences. Recursively enumerable sets and the arithmetic hierarchy. Church’s Thesis. [5]
Gödel numbering and the arithmetization of logic. The recursiveness of the proof predicate. Gödel’s first incompleteness theorem. Tarski’s undefinability theorem. [6]
Applications of the incompleteness theorem to show the undecidability of the predicate calculus and other axiom systems. Examples of decidable theories: Presburger arithmetic. [8]
Gödel’s second incompleteness theorem. The philosophical impact of Gödel’s work. The limitations of the axiomatic method. [2]

Teaching and learning methods
24 lectures, 7 examples classes and assigned reading.

**Learning hours**
Activity	Hours
Staff/student contact	35
Private study	112
Total hours	147

**Assessment**
Assessment activity	Length	Weighted within unit
Two take-home tests		20%
End of semester examination	2½ hours	80%

Core learning materials
Textbooks
H.B. Enderton, A Mathematical Introduction to Logic, (especially chapter 3). Academic Press.
J.R. Shoenfield, Mathematical Logic, (chapters 4 and 6). Addison-Wesley, 1967.
G.T. Kneebone, Mathematical Logic and the Foundations of Mathematics. Van Nostrand, 1963.
Hao Wang, From Mathematics to Philosophy. RKP, 1974.

Credit Rating: 15
Level: M.Sc.
Delivery: Semester Two
Lecturer: Peter Aczel (Room 2.52 of the Computer Science Department, Telephone: 56155, email: petera@cs.man.ac.uk).

General Description
Types were first used in foundational languages for mathematics, where they were used to avoid Russell's paradox and other logical paradoxes. Types have also come to play a role in programming languages as data types, where they provide a useful discipline that helps to avoid many errors in programming. Types also play a role in the formal study of proofs, particularly in connection with formal systems for constructive mathematics. In fact from a constructive perspective a mathematical assertion can be viewed as a type, the type of its proofs.

Aims
To introduce students to the key background ideas motivating the modern interest in type theories, to give students an understanding of the mathematical foundations for type theories and an appreciation of their role in programming languages and in formal languages for mathematics.

Learning Outcomes
On successful completion of the course unit students will be able to
- demonstrate facility in reasoning in the systems of untyped and typed lambda calculi
- understand some of the metaheory of those calculi
- appreciate how the calculi are related to both logic and computing.

A knowledge of the classical propositional calculus. Some familiarity with predicate logic, as studied in the course unit MT5151 would also be helpful, but not essential.

Teaching and learning methods
24 lectures, 7 examples classes, and assigned reading.

**Learning hours**
Activity	Hours
Staff/student contact	35
Private study	112
Total hours	147

**Assessment**
Assessment activity	Length	Weighted within unit
Two take home tests		20%
End of semester examination	2½ hours	80%

The two take home tests are intended to take each student about 4 hours of work to complete for each test.

Core learning materials
Reading
This will be concerned with some type-checking computer systems. There may also be an opportunity to experiment with some of them. These systems can be viewed as simultaneously functional programming languages and as proof development languages where users can develop formal machine checked mathematical proofs.
Textbooks
Simon Thompson, Type Theory and Functional Programming', Addison Wesley, 1991.
Nordstrom et al., Programming in Martin-Lof's Type Theory - An Introduction, Oxford University Press, 1990.