|
Instructors: Prof. Dr. phil. nat. Ulrich Kohlenbach
Event type:
Lecture & Exercise
Org-unit: Dept. 04 - Mathematics
Displayed in timetable as:
Ang. Bew.th.
Subject:
Crediting for:
Hours per week:
6
Credits:
9,0
Language of instruction:
Englisch
Min. | Max. participants:
- | -
Course Contents:
Proof Theory has its historical origin in D. Hilbert's foundational program around the consistency problem for mathematics. Since the 50's, G. Kreisel initiated a shift of emphasis resulting in a new applied form of proof theory.
This course develops the major techniques of applied proof theory,
namely so-called proof interpretations together with applications to
various areas of mathematics such as approximation theory, nonlinear
analysis and ergodic theory. These applications are concerned with the
extraction of effective bounds and new qualitative uniformity results
from prima facie ineffective proofs. The main techniques studied are:
Herbrand theory, nocounterexample interpretation (Kreisel), modified
realizability (Kreisel), Gödel’s functional (‘Dialectica’)
interpretation, negative translation (Gödel), functional interpretation
of full analysis (Spector), monotone interpretations and their
extensions to systems based on classes of abstract (nonseparable)
metric, hyperbolic and normed spaces.
Literature:
Preconditions:
Expected Number of Participants:
Further Grading Information:
Official Course Description:
This course develops the major techniques of applied proof theory, namely so-called proof interpretations together with applications to various areas of mathematics such as approximation theory, nonlinear analysis and ergodic theory. These applications are concerned with the extraction of effective bounds and new qualitative uniformity results from prima facie ineffective proofs. The main techniques studied are: Herbrand theory, nocounterexample interpretation (Kreisel), modified realizability (Kreisel), Gödel’s functional (‘Dialectica’) interpretation, negative translation (Gödel), functional interpretation of full analysis (Spector), monotone interpretations and their extensions to systems based on classes of abstract (nonseparable) metric, hyperbolic and normed spaces.
|
