M05N. Constructive Arithmetic and
Analysis
Χειμερινό εξάμηνο, 2005-2006, σεμιναριακό
μάθημα.
Ημέρα και ώρες του μαθήματος: Τετάρτη, 2-4 μμ.
Αίθουσα: Α11,
Τμήμα Μαθηματικών, Ε.Κ.Π.Α.
Διδάσκουσα: Joan Moschovakis,
Γραφείο 118,
Tμήμα Μαθηματικών Πανεπιστημίου Αθηνών, joan@math.uoa.gr,
joan@math.ucla.edu
Ώρες Γραφείου: Τρίτη 4 - 4¨30,
Τετάρτη
1:30 - 2, Παρασκευή 1:30 - 2. (Also by
arrangement.)
Ιστοσελίδα του μαθήματος: http://www.math.ucla.edu/~joan/m05n
This half-course will be taught in English, from notes which will be
distributed in class and posted on the class webpage. Students
who completed M04N last year will learn much new material in this
additional half-course. Students who did not take M04N last
year will find this half-course to be self-contained, as it begins with
a brief review of intuitionistic logic using excerpts from last
year's notes.
Prerequisite: One course in mathematical logic. Some
familiarity with recursive functions will help in understanding the
realizability models for theories based on Heyting arithmetic and
Brouwer's intuitionistic analysis.
Constructive mathematical reasoning is based on intuitionistic logic,
which can be described loosely as classical logic with the
Aristotelian law [A or not A] weakened to the principle that a
contradiction implies every sentence. Restricting the logic makes
it possible to consistently assume mathematical principles which
are inconsistent with the classical interpretations of the quantifiers.
This course studies and compares some of the varieties of
constructive mathematics which result.
Topics of the course include:
1. Introduction:
a) Brouwer-Heyting-Kolmogorov
(B-H-K) interpretation of the logical connectives and
quantifiers.
b) Intuitionistic propositional
and predicate logic as sublogics of the corresponding classical logics.
c) G\"odel-Gentzen translation of
classical into intuitionistic logic. Glivenko's Theorem.
2. Mathematical applications of intuitionistic logic:
a) Heyting arithmetic.
b) Russian constructive
mathematics (including Markov's Principle and Church's Thesis).
c) Bishop's cautious
constructivism (the indispensable core).
d) Brouwer's intuitionistic
analysis (including bar induction and axioms of countable and
continuous choice).
e) Introduction to classical and
constructive hierarchy theory in extended intuitionistic analysis (if
time).
3. Introduction to realizability interpretations of
intuitionistic
theories.
Supplementary references:
1. Kleene, S. C., Introduction to Metamathematics.
2. Troelstra, A. S. and van Dalen, D., Constructivism in
Mathematics (two volumes).
3. Bridges, D. and Richman, F., Varieties of Constructive
Mathematics.
4. Troelstra, A. S., Realizability, in: Handbook of Proof
Theory, ed. S. Buss.
5. Moschovakis, J., entry on intuitionistic logic in the Stanford
On-Line Encyclopedia of Philosophy.
6. van Dalen, D., Logic and Structure, Third Edition (Chapter 5).
7. Βαφειάδου, Γαρυφαλλία, Ενορατική Ανάλυση, ΜΠΛΑ
διπλωματική εργασία (see the link below).
An excellent reference on intuitionistic
analysis, in Greek!
postscript
and pdf
8. Moschovakis, J., Analyzing realizability by Troelstra's
methods, Annals of Pure and Applied Logic 114 (2002), 203-225.
9. Βαφειάδου, Γαρυφαλλιά και Μοσχοβάκη,
Ιωάννα, Τα ενορατικά μαθηματικά και η λογική τους (Draft,
in Greek, 25 pages, postscript pdf)
Important: The 25-page draft of a
joint article on intuitionistic mathematics, in Greek, by Γαρυγαλλιά
Βαφειάδου and myself, is
available by the link above (#9 in the Supplementary
references). It gives a historical and expository
account of intuitionistic
mathematics, less technical than your course notes. (It
is for a book edited by Professor Anapolitanos, to be published by the
Greek
Mathematical Society.) Any
comments will be very much appreciated.
Check the corrected notes for
a function which realizes CT_0 (thanks to
Anastasia Beneti; sorry for the confusion) and an introduction
to
intuitionistic analysis.
You will not be asked to do Exercises 4.18 -
4.20, but Theorem 4.27 and Corollary 4.28 are important results
which help to distinguish HA
from PA so
you may want to read them. I won't take the time to prove
them in class.
Latest version of text (Notes on the
Foundations of Constructive Mathematics)
postscript
pdf
Please work from this version if possible. This is
a text in progress; corrections will be very much
appreciated!
Solutions to Exercises 4.1(a)(c) and
4.3 postscript
pdf
Solutions to Exercises 4.4* and 4.5 -
4.7 postscript pdf
Solutions to Exercises 4.12 -
4.14
postscript
pdf
Solutions to Exercises 4.15 -
4.16
postscript
pdf
Exercises
to be handed in by January 15, 2005 instead of a final
examination:
postscript
pdf
The current version of the notes is
nearly complete for this year's course.
Exercises 1, 2(a)(b) (assigned in class, corrected and returned
to you)
were due on October 12.
They are the first two problems in your final assignment.