| Advisor: | Lars Birkedal, birkedal@it-c.dk, Glentevej 67, Room 2.21, 3816 8868 |
The aim of this project is to acquaint students with aspects of constructive logic. We plan to cover: natural deduction, Hilber style system, truth-value semantics of constructive logic, embedding classical into constructive logic, constructive arithmetic and analysis, constructive real numbers, basic recursion theory in HA, Kleene's number realizability, Markov's principle, Kleene's function realizability, higher type arithmetic, modified realizability, Goedel's functional interpretation.
| Project format | We have a common project meeting each week, where we discuss the reading material. Project participants have to write a report, on a topic of their own choice related to the reading material. The reports must be written in groups with minimum 2, preferably 3, persons in each group. |
|---|---|
| Project period | February 1 - April 26, 2001. |
| Project meetings | Fridays, Glentevej, Room: 2.55, 3:00 PM - 4:00 PM. |
| Prerequisites | This is an introductory graduate course with no formal pre-requisites; however, some basic acquaintance with naive set theory and the formalism of first order logic as usally acquired in undergraduate computer science or math is assumed. |
| Notes | Introduction to Constructive Logic and Mathematics by Thomas Streicher. The notes can be bought at the first project meeting. |
| Credits | 7.5 ECTS |
| Grading | Will be based on written project report. The grade will be Passed or Not-Passed. |
| Home | http://www.it-c.dk/~birkedal/teaching/logic-Spring-2001/ |
| Email-list | emails.txt |
http://www.it-c.dk/~birkedal/teaching/logic-Spring-2001/
.
Other pointers: