On relating strong type theories and set theories
1 hour 7 mins,
122.62 MB,
MP3
44100 Hz,
249.87 kbits/sec
Share this media item:
Embed this media item:
Embed this media item:
About this item
| Description: |
Rathjen, M (University of Leeds)
Tuesday 15th December 2015 - 10:00 to 11:00 |
|---|
| Created: | 2015-12-21 16:53 |
|---|---|
| Collection: | Mathematical, Foundational and Computational Aspects of the Higher Infinite |
| Publisher: | Isaac Newton Institute |
| Copyright: | Rathjen, M |
| Language: | eng (English) |
| Distribution: |
World
(downloadable)
|
| Explicit content: | No |
| Aspect Ratio: | 16:9 |
| Screencast: | No |
| Bumper: | UCS Default |
| Trailer: | UCS Default |
| Abstract: | There exists a fairly tight fit between type theories à la Martin-Löf and constructive set theories such as CZF and its extension, and there are connections to classical Kripke-Platek set theory and extensions thereof, too. The technology for determining the (exact) proof-theoretic strength of such theories was developed in the late 20th century. The situation is rather different when it comes to type theories (with universes) having the impredicative type of propositions Prop from the Calculus of Constructions that features in some powerful proof assistants. Aczel's sets-as-types interpretation into these type theories gives rise to rather unusual set-theoretic axioms: negative power set and negative separation. But it is not known how to determine the consistency strength of intuitionistic set theories with such axioms via familiar classical set theories (though it is not difficult to see that ZFC plus infinitely many inaccessibles provides an upper bound). The first part of the talk will be a survey of known results from this area. The second part will be concerned with the rather special computational and proof-theoretic behavior of such theories. |
|---|---|
Available Formats
| Format | Quality | Bitrate | Size | |||
|---|---|---|---|---|---|---|
| MPEG-4 Video | 640x360 | 1.96 Mbits/sec | 974.01 MB | View | Download | |
| WebM | 640x360 | 558.32 kbits/sec | 269.90 MB | View | Download | |
| iPod Video | 480x270 | 529.74 kbits/sec | 256.08 MB | View | Download | |
| MP3 * | 44100 Hz | 249.87 kbits/sec | 122.62 MB | Listen | Download | |
| Auto | (Allows browser to choose a format it supports) | |||||