Per Martin-Löf

Per Erik Rutger Martin-Löf (* 8. Mai 1942) ist ein schwedischer mathematischer Logiker und Philosoph. Martin-Löf war 1964–1965 an der Lomonossow-Universität Student von Andrei Kolmogorow, der auch seine Dissertation an der Universität Stockholm 1970 betreute (Notes on constructive mathematics). Zuvor war er 1968/69 schon Assistant Professor an der University of Chicago bei William Alvin Howard, dessen Curry-Howard-Isomorphismus später eine der Grundlagen von Martin-Löfs Typentheorie war. Martin-Löf war Professor für Mathematik an der Universität Stockholm. In seiner Zeit in Moskau verfeinerte er auch den Begriff der Zufallsfolge. 1970 führte er seine intuitionistische Typentheorie ein (auch Martin-Löf-Typentheorie oder konstruktive Typentheorie genannt), die er aber mehrfach umformte, da die ersten Ansätze, die das „System F“ von Jean-Yves Girard verallgemeinerten, inkonsistent waren, aufgrund eines von Girard entdeckten Paradoxons. Eine Reihe von computergestützten Beweissystemen wie NuPRL, LEGO, Coq, ALF, Agda, Twelf und Epigram beruht auf Löfs Typentheorie. Später wandte er sich zunehmend philosophischen Fragen der Logik zu. Martin-Löf befasste sich auch mit Statistik, zum Beispiel mit der Suffizienz, der Exponentialfamilie, dem EM-Algorithmus, dem Problem fehlender Daten in der Statistik, Statistischen Modellen, Wahrscheinlichkeit auf Halbgruppen. Zu seinen Schülern gehört der Statistiker Rolf Sundberg. Martin-Löf ist Mitglied der Königlich Schwedischen Akademie der Wissenschaften und der Academia Europaea. 2006 war er Gödel-Lecturer (The two layers of logic), 2012 hielt er die Tarski Lectures. 2020 erhielt er gemeinsam mit Dag Prawitz den Rolf-Schock-Preis für Philosophie. Er ist der Bruder des Mathematikers Anders Martin-Löf (* 1940), Professor für Versicherungsmathematik in Stockholm. Martin-Löf war ein passionierter Ornithologe und veröffentlichte 1961 eine Arbeit, aus den Funden beringter Vögel auf deren Sterblichkeitsrate zu schließen.