Siegel der Universität Augsburg

Universität Augsburg
Institut für Mathematik

Siegel der Universität Augsburg


Oberseminar zur Algebra und Zahlentheorie


Andrej Bauer
Universität Ljubljana

spricht am
Dienstag, 23. Mai 2017
15:45 Uhr
Raum 1005 (L1)
über das Thema:

»Type theory as a foundation of mathematics«

The standard foundation of modern mathematics has two layers. At the bottom there is first-order logic, which captures the axiomatic method and rules of reasoning. On top of logic rests set theory, a second layer that supplies the raw material from which mathematicians construct structures of interest. It is possible to turn things around, and start with a theory of constructions that stands on its own, without a background logic. Constructions are taken as a primitive notion, governed by rules of construction and deconstruction, and the interactions between them. The objects so arising form a mathematical universe, and are classified into types according to their method of construction. Logic becomes a special case, for proofs are seen to be just a certain kind of constructions. The entire edifice is known as type theory. A philosopher might explain that type theory describes the mental constructions inside a mathematician's mind, a computer scientist that type theory is a programming language, and a logician that types are just good old sets in disguise. Can a mathematician provide a different, more exciting explanation?


Hierzu ergeht herzliche Einladung.

Kaffee, Tee und Gebäck eine halbe Stunde vor Vortragsbeginn im Raum 2006 (L1).

wwwadm@Math.Uni-Augsburg.DE,    Do 18-Mai-2017 12:05:06 MESZ