Mathematical logic, HT 2001 (MAN480/TMA240)
THE EXAM (omtenta) IS CORRECTED! The results will be at the notice-board in the
basement this afternoon (2 September).
The first exam with solutions can be found here.
Grades on the exam:
GU: 0-11 U, 12-19 G, 20-25 VG and CTH: 0-10 U, 11-14 3, 15-19 4, 20-25 5.
There is a Course Enquiry (kursenkät) now. Please fill it out, it
is important for us when we plan next years course. There is only a
swedish version, but you are most welcome to answer in english.
Which are the good exercises, thinking of the exam?
In general, all the exercises of the lessons are relevant, they are
included in the following list of, which also include some more.
Some more exercises will most probably be added.
1.2:1-3 1.4:1-5, 11, but there will be no difficult
derivations in ND in the exam. 1.5: 1-4, 6-11
1,6: 1, (2, 3), 4-7
- 2.2: 1, 2
2.5: 1, 4-7, 12, 14, 15
2.7: 6, 10 (the other exercises are also good but may require
knowledge of the mathematical theory involved).
- 3.1: 1-4 3.2: 7, 13
- 5.4: 9a. Also the exercises in the extra material on
- The extra material on Gödel's incompleteness theorem: 18 (p. 155).
Jan has written some extra material on Natural Deduction(pdf) and Kripke
semantics(pdf). It's a good complement to van Dalen.
There is a proof editor for Unix (developed at Chalmers) called Alfa which
handles ND perfectly well. You start the editor by the command "alfa - -norec" and a deduction starts by choosing ND Style Proof in
We have changed the literature to van Dalen: Logic
| What is included in the course?
The course is a short introduction to mathematical
logic. The two main goals are
We are going to talk about propositional and predicate
(first order) logic and do some formal proofs in a proof system called
natural deduction (ND for short). Some properties of propositional and
predicate logic will be shown; for example completeness, which says that
a sentence is true iff it can be proved in ND. We will also spend some
time with Gödels incompleteness theorem, which says that there is
no "good" set of axioms from which we can prove all arithmetical truths.
understand what a proof is and
learn to use a formal proof system.
We will use the book
Logic and Structure,
written by Dirk van Dalen (Springer Verlag). At least chapter 1-3 and
5 is included
in the course and maybe something more. Besides the book we are going to
cover Gödels incompleteness theorem (which is not in the book).
There are a lot of other good books if you want
to read more about logic. Introduction to mathematical logic by
E. Mendelson is an example of a very good book.
| What we have done so far in the lectures.
- 6 Nov. A general overview of the foundations of mathematics.
- 8 Nov. Sections 1.1 and 1.2
- 13 Nov. Section 1.3 and Natural Deduction.
- 15 Nov. Most of section 1.5.
- 20 Nov. Soundness theorem for propositional logic (section
1.5). Section 2.1, 2.2 and the beginning of 2.3 (defined the sets
TERM and FORM).
- 22 Nov. Constructive semantics for propositional logic
(pp.157-158). Section 1.5 again.
- 27 Nov. Semantics for predicate logic (Section 2.4),
examples of structures.
- 29 Nov. Natural deduction for Predicate logic. Finishing
section 1.5 (Completeness theorem).
- 4 Dec. More predicate logic. Intuitionistic logic,
section 5.2. Kripke semantics section 5.3 pp 166-172, but only
for propositional logic; all material on Kripke semantics is included in the
written by Jan.
- 6 Dec. (Fredrik) Equality in ND and most of chapter
3.1 (the completeness theorem for predicate logic).
- 11 Dec. (Fredrik) Compactness theorem, nonstandard
models of arithmetic, infinte vs. finite (chapter 3.2).
- 13 Dec. . General introduction to Gödel's incompleteness
theorem (first two pages of the extra matewrial). Gödel
numbers. Representability. There are some
comments(pdf) on the extra material.
- 18 Dec. Finished Gödel's incompleteness theorem.
- 20 Dec. Interpretations of classical logic in
intuitionistic logic. 4 theorems: Theorems 5.2.8 and 5.2.10 and
Excersices 5.4 and 5.5 in van Dalen.
- 8 and 10 Jan. Recapitulation.
| What we will do the next lecture
| Details of what is included in the course of what
we have covered so far
1.1 Induction principle and Definition by
recursion are important. You don't have to know about formation
sequence and Induction on rank-Principle. 1.2 Everything.
1.3 pp. 24-26 up to Definition 1.3.10 are not included.
Definition 1.3.10 and the rest of section 1.3 contains very
good examples of inductive definitions and proofs.
All of 2.1-2.4. Section 2.5 contains a lot
of examples which are
good to have a look at. Understand what Theorem 2.5.8 says, as
you can see the proof of this rather obvious theorem on
substitution is a bit messy. Definition 2.5.10 and Theorem 2.5.11
about prenex form are important. All of 2.6. 2.7 contains many good examples, but the only one you are
required to know about is Ex. 6 which is about arithmetic. All of
but 2.8 and 2.9 can be
replaced by the notes on Natural Deduction(pdf).
3.1:pp 105- middle of 110. Please note that we gave another
proof of Lemma 3.1.9 which is hinted in the remark after the
3.2: I did not follow the book on this material. Theorem
3.2.1 is important and also Lemma 3.2.6. See also exercise
3.3: Some bits of Application I. Non-standard Models of
Arithmetic on page 122.
Sections 5.1 and 5.2, but Kripke
semantics only for propositional logic. For the exam, it is enough to
read the extra material on Kripke
1.1: 9, 1.2: 1b,2c, 1.4: 3b, d, 5, 1.6: 1, 5
1.5: 1, 2, 3, 7, 8, 9
27 Nov. 1.4:2,4 1.6: 1,4,5,7
29 Nov.2.2:1(i)-(iii) 2.3:1, 2, 4d,f,g,h
2.4:1, 2, 4, 5, 7
2.7: 4 2.9: 4. Exercises from the notes on Kripke
semantics: 1, 2a, b. Exercises left over from 29 nov.
11 Dec. Easy examples in predicate logic of derivations
i ND: some of (17) - (26) on page 160. Jan vill take this lesson.
13 Dec. 3.1: 1,3,4 3.3:10, 17 (+definition of substructure)
20 Dec. Exercise 18 in page 155 in Hamilton, 2.5: 14
5.4: 5 + questions.
10 Jan. Examples from old exams.
Please observe that the course is rather different
this year and therefore the old exams are not really appropriate.
Last modified: Mon Sep 2 12:00:16 MEST 2002