Takeuti Gaisi

Takeuti Gaisi (jap. 竹内 外史, Takeuchi Gaishi; * 25. Januar 1926 in Kizu, Präfektur Ishikawa, Japan; † 10. Mai 2017) war ein japanischer mathematischer Logiker, bekannt für Beiträge zur Beweistheorie. Takeuti wurde 1956 an der Universität Tokio in mathematischer Logik promoviert. Er war ab 1950 zuerst Assistenzprofessor, später Professor an der Pädagogischen Universität Tokio und ab 1966 Professor an der University of Illinois at Urbana-Champaign. 1996 wurde er emeritiert. Takeutis Ziel in den 1950er Jahren war es, Widerspruchsfreiheitsbeweise für formale Systeme zu gewinnen, die die Analysis umfassen. Hierzu entwickelte er Methoden von Gerhard Gentzen weiter (unter anderem führte er ordinal diagrams ein). Takeuti gelang 1967 der Widerspruchsfreiheitsbeweis der Π 1 1 {\displaystyle \Pi _{1}^{1}} -Analysis (der Teil der Analysis, in der die Komprehension auf beliebige Formeln mit höchstens einem Mengenquantor eingeschränkt ist). Das war nach Kurt Schütte der erste Widerspruchsfreiheitsbeweis eines wesentlich imprädikativen Teils der Mathematik und Analysis. Takeutis Vermutung von 1953 besagt, dass im Logikkalkül endlicher Stufe die Schnittregel gilt (siehe Gentzenscher Hauptsatz). Sie wurde für den Kalkül 2. Stufe von William W. Tait (1966) und Dag Prawitz (1967, für höhere Ordnung 1969) und unabhängig von Takahashi Motoo (1967, auch höhere Ordnung) und Jean-Yves Girard bewiesen. Von Takeuti stammten zwei Lehrbücher und Standardwerke, eines zur Beweistheorie und eines zur axiomatischen Mengenlehre. Anfang der 1950er Jahre befasste er sich auch mit Homotopietheorie und Knotentheorie (er hielt 1952/53 ein Seminar ab, das sein Doktorand Kunio Murasagi besuchte). 1959/60, 1966 bis 1968 und 1971 bis 1972 war er am Institute for Advanced Study bei Kurt Gödel. 2003 bis 2009 war er Präsident der Kurt Gödel Society. 1998 erhielt er die tschechische Bolzano-Medaille und er erhielt den Okawa-Preis für Veröffentlichungen. 1982 erhielt er den Asahi-Preis.