Konstruktive Analysis
Dozent:
Helmut Schwichtenberg.
Termine
Proseminar: Di 16-18, Hörsaal 251. Beginn 20. April.
Tutorium: Do 16-18, Hörsaal K 35. Beginn 22. April.
Sprechstunde: Schwichtenberg Do 15-16, Zimmer 415.
Vorträge
Helmut Schwichtenberg, Constructive Logic, 27. April.
Maximilian Niklas, Real Numbers (pp.3-6), 4. Mai.
Eckhard Maass, Uncountability, Completeness, Limits and Inequalities
(pp.9-13), 11. Mai.
Michael Lubasch, Series, Convergence Tests, Redundant Dyadic Representation
(pp.13-18), 18. Mai.
Alexander Mathis, Exponential Series, Complex Numbers (pp.18-23), 8. Juni.
Christian Reiher, Continuous Functions (pp.23-30), 15. und 22. Juni.
Alex Schreiber, Intermediate Value Theorem (pp.30-33), 29. Juni.
Thomas Nowak, Differentiation (pp.33-36), 6. Juli.
Holger Blasum, Integration (pp.37-42), 13. Juli.
Parmenides Garcia Cornejo, Sequences of Functions (pp.47-53), 19. Juli (!),
14-16, Hörsaal E27.
Richard McKnight, ODEs (pp.54-58), 20. Juli.
Skriptum
Constructive Analysis (ps/pdf)
Literature:
- Bishop/Bridges, Constructive Analysis, Springer 1985. Kapitel 2
- Mints `A Short Introduction to Intuitionistic Logic'
Kluwer 2000
- Troelstra/S `Basic Proof Theory' 2000
- Schuster/S, `Constr. sols of continuous equations'.
- The largest Automath text that was written in the seventies was
Jutting's translation of Landau's Grundlagen der Analysis. Both a
plain TeX version of Landau's book as well as Jutting's translation
are available
here.
Contents
The goal is to develop the basics of real analysis in such a
way that from a proof of an existence formula one can extract a
program. For instance, from a proof of the intermediate value theorem
we want to extract a program that, given an arbitrary error bound
$2^{-k}$, computes a rational $x$ where the given function is zero up
to the error bound. We will treat most subjects covered in the first
year of standard calculus, including existence and uniqueness proofs
of ODEs.
Why should we be interested in logic in a study of constructive
analysis? There are at least two reasons.
(1) Obviously we need to be aware of the difference of the classical
and the constructive existential quantifier, and try to prove the
stronger statements involving the latter whenever possible. Then
one is forced to give `constructive' proofs, whose algorithmic
content can be `seen' and then used as a basis to formulate a
program for computing the solution.
(2) However, one can go one step further and automatize the step from
the (formalized) constructive proof to the corresponding program.
This can be done by means of the so-called realizability
interpretation, whose existence was clear from the beginnings of
constructive logic. The desire to have `mathematics as a numerical
language' in this sense was clearly expressed by Bishop (in an
article with just that title).
Parallel there will be a separate (optional) 2 hour Praktikum, where
the students should experiment with program extraction from particular
proofs. There we will work with the Minlog
System
Minlog
For interactive generation of proofs we use the Minlog
System, written in
Scheme.
Tutorium
A protocol of what has been done is in
tut.scm.
More detailed information on the general setup is available in
numbers.scm.
Some lemmata of Chapter 1: Real Numbers of the manuscript are proved
formally in
real.scm.
Helmut Schwichtenberg
[Last updated 13.07.2004]