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
 
um
 
15:45 Uhr
 
im
 
Raum 1005 (L1)
 
über das Thema:
 

»Type theory as a foundation of mathematics«

Abstract:
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