Am Lehrstuhl für mathematische Logik werden vielfältige Teilgebiete dieser Disziplin gepflegt: Beweistheorie (Buchholz, Schwichtenberg), Nichtstandard-Analysis (Osswald), Mengenlehre (Donder), Rekursions- und Bereichstheorie (Schwichtenberg) und Logikprogrammierung (Buchholz, Schwichtenberg). Es bestehen zahlreiche Verbindungen zu anderen Teilgebieten der Mathematik sowie zur Informatik und theoretischen Linguistik. So sind mehrere Doktoranden am Lehrstuhl Stipendiaten des seit 1992 bestehenden Graduiertenkollegs ,,Sprache, Information, Logik``, und im April 1997 wird ein weiteres Graduiertenkolleg mit dem Thema ,,Logik in der Informatik'ßeine Arbeit aufnehmen. Begriffsbildungen und Methoden der mathematischen Logik können in der Informatik mit großem Nutzen angewendet werden; dort hat sich zunehmend die Notwendigkeit einer stärkeren theoretischen Durchdringung zentraler Fragestellungen gezeigt. Insbesondere die Beweistheorie und die Modelltheorie haben sich hier als sehr fruchtbar erwiesen, erfordern aber noch gezielteren Zuschnitt. Ein Teil der Arbeiten am Lehrstuhl zielt darauf ab, die Anwendbarkeit logischer Methoden beim Entwurf, der Spezifikation, der Verifikation und der Optimierung von Programmen, Programmsystemen und Schaltungen weiter zu verbessern und auszudehnen.
Ein Schwerpunkt unserer Arbeiten liegt auf dem Gebiet der Beweistheorie und ihrer Anwendungen. Damit wird eine Forschungsrichtung weitergeführt, die von dem früheren Lehrstuhlinhaber und heutigen Emeritus Prof. Dr. Kurt Schütte am Mathematischen Institut begründet wurde. Zusammenfassende Darstellungen des Gebiets finden sich in den Monographien [K. Schütte, Proof Theory, 1977], [W. Buchholz, S. Feferman, W. Pohlers, W. Sieg. Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, LNM 897, 1981] und [A.S. Troelstra, H. Schwichtenberg, Basic Proof Theory, erscheint bei Cambridge University Press].
Neuere Arbeiten auf dem Gebiet der Beweistheorie betreffen Themen wie die Verwendung von Beweisen als Programmen [7],[3],[4] und die Programmentwicklung durch Beweistransformation [2]. Bekanntlich lassen sich korrekte Programme dadurch herstellen, daß man sie mit einem allgemeinen Verfahren aus einem formalen konstruktiven Existenzbeweis extrahiert. Diese Art der Gewinnung von Programmen bietet außerdem den Vorteil, daß man das Programm an spezielle Situationen automatisch anpassen und dabei sogar (im Fall mehrerer Lösungen) extensional verändern kann. Neben den theoretischen Untersuchungen ist hier auch experimentelle Arbeit am Rechner notwendig, um die Brauchbarkeit der gefundenen Algorithmen beurteilen zu können. Am Lehrstuhl wurde deshalb ein auf der Minimallogik basierendes interaktives Beweissystem MINLOG entwickelt und implementiert [7]. Charakteristisch für dieses System ist die Verwendung einer ausdrucksstarken typentheoretischen Sprache zusammen mit beweistheoretisch schwachen Axiomen von der Stärke der Peano-Axiome. Durch die Implementierung von Termersetzung ist das System in der Lage, effizient mit Gleichungen umzugehen. Es hat sich herausgestellt, daß zwischen der Theorie der Termersetzung und der von K. Schütte besonders gepflegten Ordinalzahlanalyse von mathematischen Theorien enge Beziehungen bestehen. Die Ausnutzung dieser Beziehung für Terminierungsbeweise ist Gegenstand aktueller Forschungen.
Auf dem Gebiet der Rekursions- und Bereichstheorie liegt ein Schwerpunkt unserer Arbeiten auf Untersuchungen zur Berechenbarkeit von Funktionen höherer Stufe. In der Dissertation [U. Berger, Totale Objekte und Mengen in der Bereichstheorie, 1990] (siehe auch [U. Berger, Total sets and objects in domain theory, Annals of Pure and Applied Logic 60:91-117, 1993]) wurde durch eine allgemeine Fassung des Totalitätsbegriffs in der Bereichstheorie ein wesentlicher Fortschritt erzielt; diese Untersuchungen haben inzwischen Eingang in die Lehrbuchliteratur gefunden. Aktuelle Forschungen von Herrn Berger in Zusammenarbeit mit den Universitäten Oslo (Dag Normann) und Uppsala (Viggo Stoltenberg-Hansen) beschäftigen sich mit der Erweiterung seiner Resultate über totale Funktionale auf abhängige Typen, wie sie in der von P. Martin-Löf entwickelten konstruktiven Typentheorie formal beschrieben werden. Letztere erhebt den Anspruch, die Mathematik auf eine neue, konstruktive Grundlage zu stellen (als Alternative zur Mengenlehre). Die Einführung starker Beweisprinzipien wird dabei durch ein ``intuitives Verständnis'' der Schlußregeln gerechtfertigt. Wie gefährlich dies ist, hat sich durch die Postulierung vermeintlich sinnvoller, jedoch widerspruchsvoller Axiome gezeigt (Russels Paradoxien in versteckter Form). Durch eine bereichstheoretische Interpretation besteht nun die Möglichkeit, diese Typentheorie auf eine saubere semantische Grundlage zu stellen und bei der Einführung starker Prinzipien vor Inkonsistenzen geschützt zu sein. Ein aktuelles Problem ist dabei die konstruktive Interpretation von Universen mit der extrem starken Mahlo-Eigenschaft (zu jeder stetigen Funktion auf dem Universum existiert ein Sub-Universum welches abgeschlossen unter dieser Funktion ist). Eine Typentheorie mit Mahlo-Universum wurde von Herrn Setzer in Fortführung seiner Dissertation [A. Setzer, Proof Theoretical Strength of Martin-Löf Type Theory with W-Type and One Universe, 1993] beweistheoretisch analysiert.
Ein weiteres Arbeitsgebiet sind Fragen der praktischen Berechenbarkeit von Funktionen höherer Stufe. Während die Theorie subrekursiven Hierarchien im erststufigen Fall einen gewissen Abschluß erreicht hat, steht eine befriedigende Erweiterung auf Funktionen höherer Stufe noch aus. Interessante Ergebnisse zu diesem Fragenkreis sind in der Dissertation von Herrn Niggl [Karl-Heinz Niggl, Subrecursive hierarchies on the partial continuous functionals, 1994] enthalten.