 |
Universität Augsburg
|
|
|
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 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).