[Alta-Logic] Ulrich Kohlenbach to speak Dec 5?

[Richard Zach]

Hi,

Ulrich Kohlenbach is going to attend a workshop at BIRS the second week
of December, and I've explored the possibility of him coming to Calgary
before going to Banff to give us a talk on Friday, December 5. Before we
finalize plans, I'd like to get an idea how much interest there is--and
how much commitment to attend a talk on the last day of class!

Kohlenbach has done some very exciting work in "proof mining" applying
proof theoretic methods to proofs of "actual" mathematical theorems to
extract information such as bounds for forall - exists theorems in
analysis.

He has just written a book on this:

http://www.springer.com/math/book/978-3-540-77532-4

Ulrich Kohlenbach presents an applied form of proof theory that has led
in recent years to new results in number theory, approximation theory,
nonlinear analysis, geodesic geometry and ergodic theory (among others).
This applied approach is based on logical transformations (so-called
proof interpretations) and concerns the extraction of effective data
(such as bounds) from prima facie ineffective proofs as well as new
qualitative results such as independence of solutions from certain
parameters, generalizations of proofs by elimination of premises. 

The book first develops the necessary logical machinery emphasizing
novel forms of Gödel's famous functional ('Dialectica')
interpretation. It then establishes general logical metatheorems that
connect these techniques with concrete mathematics. Finally, two
extended case studies (one in approximation theory and one in fixed
point theory) show in detail how this machinery can be applied to
concrete proofs in different areas of mathematics.

Here's the second chapter that explains the approach:
http://www.springer.com/cda/content/document/cda_downloaddocument/9783540775324-c2.pdf?SGWID=0-0-45-557108-p173805804

The entire book is online here:
http://www.springerlink.com/content/978-3-540-77532-4

His website is here:
http://www.mathematik.tu-darmstadt.de/~kohlenbach/

Richard