Vortrag von Chad Brow (Tschechische Technische Universität in Prag): Formalisierung der Mathematik in der Mengenlehre höherer Ordnung (Mi, 16. November, 14:15-15:45)

Titel: Formalisierung der Mathematik in der Mengenlehre höherer Ordnung

Referent: Chad Brown (Tschechische Technische Universität in Prag)

Zusammenfassung: Die einfache Typentheorie von Church ist eine Formulierung der Logik höherer Ordnung, auf der viele interaktive Theorembeweiser beruhen. Ein Vorteil der Verwendung von Churchs Typentheorie ist, dass es für viele Theorien, die keine endliche Axiomatisierung erster Ordnung haben, entsprechende Theorien gibt, die eine endliche Axiomatisierung höherer Ordnung haben. Ich werde die Churchsche Typentheorie vorstellen und eine endliche Axiomatisierung einer Mengenlehre skizzieren, mit der man Mathematik formalisieren kann. In diesem Zusammenhang werde ich auch das Zusammenspiel von interaktivem Theorembeweisen und automatisiertem Theorembeweisen diskutieren.

Wann: Mi, 16. November, 14:15-15:45

Wo: Erba, Raum WE5/04.004