Constructive Logic Project
Spring 2001

Advisor: Lars Birkedal,, 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 Information

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.
Email-list emails.txt

Course Material

This home page is at .

Other pointers:

  • lecture schedule
  • notes (course notes + additional reading material)
  • assignments (suggested exercises)
  • suggested projects

  • [ Home | Schedule | Notes | Projects ]

    Lars Birkedal