Lectures series: Introduction to Intuitionistic Type Theory
Important Remark
In order to reduce
email traffic, in future
the lectures will no longer be announced as previously on
the email lists. If you want to get informations via email,
please send an email to Anton Setzer
, 
Thank you.
Schedule
The main time will be on Wednesday 15 - 17, but in accordance with
obligations of the audience and of the lecturer this time will be changed
on a time to time basis.
The continuation of this series will be postponed till at least November,
maybe even till January.
However, the course on Constructive
Logic and Lambda Calculus, given by myself,
covers topics which are closely related
to this course and is therefore recommended.
Lecturer
Anton Setzer, originally
Department of Mathematics,
Uppsala University, now
Department of Computer Science,
University of Wales Swansea.
Abstract
Per Marin-Löf's type theory is a constructive frame-work for carrying out
mathematical proofs. Originally defined for carrying out constructive
mathematics, it has been of growing interest in computer science, since
in it proofs and programs are the same.
Proofs are carried out by defining a program which computes an element of the
proposition to be proved. Therefore it provides a potential framework for the
development of programs together with their correctness proofs.
We will give a introduction to this theory starting from a very elementary
level. Because of the background of the lecturer, a more proof theoretic
perspective will be taken. Recent extensions like the Mahlo universe
and the general theory of inductive recursive definitions will be covered
in later lectures. The relevance of it for the foundations with
mathematics will be discussed.
Plan
- 1. History of Type Theory
- 1.1. The foundational crisis in mathematics
- 1.2. The Brouwer-Heyting-Kolmogorov interpretation of the logical
connectives
- 1.3. The Curry-Howard Isomorphism
- 2. The Principles of type theory
- 2.1. Judgments vs. propositions
- 2.2. The judgements in Type theory
- 2.3. The meaning explanations
- The meaning of A: set
- The meaning of A=B
- The meaning of a:A
- The meaning of a=b:A
- The meaning of a=b:A
- The meaning of A: prop
- The meaning of A: true
- 2.4. Hypothetical judgements with one assumption
- 2.5. Hypothetical judgements with many assumptions
- 3. The structural rules of type theory
- 3.1. The context rules
- 3.2. The assumption rules
- 3.3. The equality rules
- 3.4. The (derivable) substitution rules
- 4. The main types (sets) in type theory
- 4.1. The four kinds of rules for each set
- 4.2. The finite sets N_k
- 4.3. The disjoint union of sets
- 4.4. The Sigma type
- 4.5. The Pi type
- 4.6. Excurs: Normalization and equality rules
- 4.7. Excurs: The axiom of choice
- 4.7. The set of natural numbers
- 4.8. The universe
- The version a la Tarski
- The version a la Russell
- 4.9. The identity type
- The intensional identity type
The next lecture will start here
- The extensional identity type
- The intensional identity type a la Troelstra
- The decidable equality on N
- 4.10. The W type
- 5. The logical framework
- 6. The Meta theory of type theory
- 6.1. The naive set theoretic model
- 6.2. A term model
- 6.3. A normalization proof
- 6.4. Remarks on the proof theoretical strength
- 7. Extensions of type theory
- 7.1. The Mahlo universe
- 7.2. Inductive recursive definitions