# Proseminar Konstruktive Analysis

Dozent:
Helmut Schwichtenberg.

## Termine

Proseminar: Di 16-18, Hörsaal 252. Beginn 12. April 2005.

Sprechstunde: Schwichtenberg Mo 14-15, Zimmer 415.
## Vorträge

1. Free algebras, recursion (mlcf 2.1-2), 19. April.

2. Languages for algebras, induction (mlcf 2.4.1-4), 26. April.

3. Constructive logic (Skript Mathematical Logic I, van Dalen), 3. Mai.
Emil Wiedemann

4. Program extraction from constructive proofs (mlcf 4.2-4.3.1), 10. Mai.

5. Examples: Binary numbers, Euclidean algorithm (numbers.scm, gcd.scm),
24. Mai. Andreas Wadhwa

6. Real numbers (constr, pp.4-10), 7. Juni. Andreas Lauer

7. Real numbers: Uncountability, completeness, limits and inequalities
(constr, pp.11-15), 14. Juni. Luba Stein

8. Continuous functions (constr, pp.25-30) (2 Termine), 21. und 28. Juni.
Aniko Öry

9. Intermediate value theorem (constr, pp.30-32), 5. Juli.
Judith Gampe

## Schriftliches Material zu den Vorträgen

1. Free algebras, recursion (ps/pdf)

2. Languages for algebras, induction (ps/pdf)

4. Program extraction from constructive proofs (ps/pdf)
## Skripten

- Constructive Analysis (ps/pdf)
- Minimal Logic for Computable Functionals (ps/pdf)
- Mathematical Logic I (ps/pdf)

## Literatur

- Bishop/Bridges, Constructive Analysis, Springer 1985. Kapitel 2
- Mints `A Short Introduction to Intuitionistic Logic', Kluwer 2000
- Troelstra/S `Basic Proof Theory', Cambridge Univ Press 2000

## 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 $a$ where the given function is zero up
to the error bound. We will treat most subjects covered in the first
year of standard calculus.

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. This amounts to something like `mathematics as
a numerical language' (a term due to Bishop).

Helmut Schwichtenberg
[Last updated 14.06.2005]