Universität Augsburg

Andrej Bauer
Universität Ljubljana
spricht am
Dienstag, 23. Mai 2017
um
15:45 Uhr
im
Raum 1005 (L1)
über das Thema:
Abstract: 
The standard foundation of modern mathematics has two layers. At the bottom there is firstorder 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).