Applied Logic (Tillämpad Logik)

NOTE

• Please fill in the online course evaluation form. See instructions in the email you received recently.
• Preliminary results of the written exam 2007-12-17 are found here.
• Written exam 2007-12-17.
• Preliminary results of the written exam 2008-03-27 are found here.

  You may bring with you and use all course literature, all hand-outs and all notes from the course during the written exam.

General information

• Syllabus of course in English and in Swedish.
• Course information
• This page will be updated regularly.
• Links to earlier and shorter versions of the course can be found here: 2000, 2001, 2002, 2004, 2006.

Lectures

1. Lecture 1 (Aug. 30): Introduction. Undecidable problems: halting problem, PCP, truth in first order arithmetic.
2. Lecture 2 (Sept. 4): Completeness for first order logic (FOL). Church's theorem on undecidability of provability in FOL. Non-constructive proofs.
3. Lecture 3 (Sept. 6): Intuitionistic logic. Kolmogorov's constructive interpretation of logic as problems and solutions. A simple lambda calculus: Gödel's system T.
4.      - Exercise class 1 (Sept 13, Anton Hedin)
5. Lecture 4 (Sept. 18): Lazy operational semantics of system T. Semantic and syntactic typing in T. The BHK-interpretation. Abstract realizability of propositions.
6.      - Exercise class 2 (Sept 20, A. Hedin)
7. Lecture 5 (Sept. 24): Abstract realizability. Heyting arithmetic. Propositions-as-types.
8.      - Exercise class 3 (Sept 27, A. Hedin)
9. Lecture 6 (Oct. 1): Dependent types. Martin-Löf type theory. Introduction to the proof assistants Agda and Alfa.
10. Lecture 7 (Oct. 8): Martin-Löf type theory (cont.). Demo of Alfa.
11.      - Exercise class 4 (Oct 10, A. Hedin)
12. Lecture 8 (Oct. 16): Type universes. The proof assistant Coq. Classical vs. intuitionistic proofs. Double-negation interpretation.
13. Lecture 9 (Oct. 18) Proof search in intutionistic and classical propositional logic using sequent calculi.
14. Lecture 10 (Oct 25) Proof search in predicate logic. Gallier pp. 60-74, pp. 187-206.
15. Lecture 11 (Oct 29) Proof search using sequents (cont.). Equational logic.
16.      - Exercise class 5 (Oct. 31)
17. Lecture 12 (Nov 6) Equational logic. Term rewriting.
18. Lecture 13 (Nov 8) Unification. Resolution.
19.      - Resolution. Presentation of lab 2. Exercise class 6 (Nov 13)
20. Lecture 14 (Nov 20, A. Hedin)
21. Lecture 15 (Nov 22, A. Hedin)
22.      - Exercise class 7 (Nov 27, A. Hedin)
23. Lecture 16 (Nov 29, A. Hedin)
24. Lecture 17 (Dec 4, A. Hedin)
25.      - Exercise class 8 (Dec 6, A. Hedin)

Hand-outs

• Classical and intuitionistic proofs. (Lecture notes, E. Palmgren)
• Contraction-free sequent calculus for intuitionstic logic , R. Dyckhoff. Journal of Symbolic Logic 57(1992).
• Equational logic, unification and term rewriting. (Lecture notes, E. Palmgren)
• Some logical background to the resolution method. (Lecture notes, E. Palmgren)
• Modal logic. (Lecture notes, A. Hedin)

Supplementary reading

• Constructive Logic and Type Theory (E. Palmgren). Some may find this presentation which covers part of the material from Lectures 3-7 easier than the lectures and the hand out. It builds on a standard presentation of natural deduction. However, it does not treat semantic typing and meaning explanations.
• Undecidability in number theory (B. Poonen).
• On the meanings of the logical constants and the justifications of the logical laws. (P. Martin-Löf)
• Type Theory in Stanford Encyclopedia of Philosophy by Thierry Coquand.
• Programming in Martin-Löf type theory (B. Nordström, K. Petersson, J.M. Smith)

Exercises

• Exercises 1 --- Sept. 13
• Exercises 2 --- Sept. 20
• Exercises 3 --- Sept. 26
• Exercises 4 --- Oct. 10
• Exercises 5 --- Oct. 31
• Exercises 6 --- Nov. 13
• Exercises 7

• 20001020: 1-3,5,8
• 20011017: 1-5,8
• 20020116: 1-5,7,8
• 20021017: 1-5,7,8
• 20030115: 1-5
• 20040526: 1-7
• 20060607: 1-3, 5-7
• 20070524: 1-7

Laboratory work

• Alfa can be downloaded here and a user guide is found here.
• Some useful remarks on Alfa/Alfa in the relation to the type theory presented is found here . Example Alfa files mentioned there.
• Some hints for using Alfa
• Exercises in propositional and predicate logic using Alfa.
• Obligatory hand-in-problem 1 (Laboration 1)
  • The problems and instructions.
  • Prepared Alfa files.

2. The second obligatory exercise concerns automatic theorem proving in first order logic. You need to down load and install Prover9.

• The problems and instructions.
• Example files.

Examination

Note: You may bring along and use all course literature, all hand-outs and all notes from the course during the written exam.

Teachers

• Professor Erik Palmgren. Examiner.
• Anton Hedin, Teaching assistant, PhD student in mathematical logic.

Links

• The Stockholm-Uppsala Logic Seminar, Wednesdays at 10.00 or 10.30.
• Seminar on Theories of Proofs, Types and Computation.
• Alfa -- a graphical version of the Agda proof assistant.
• Agda - Official Web Site
• The Coq proof assistant
• Prover 9 -- an automated theorem prover for first-order and equational logic.
• Pesca -- a proof editor for sequent calculus.
• Haskell -- a purely functional language.
• Wiki pages by Emmet Caulfield for the participants of the course.