Abstract
We interpret finite types as domains over nonflat inductive base types in order to bring out the finitary core that seems to be inherent in the concept of totality. We prove a strong version of the Kreisel density theorem by providing a total compact element as a witness, a result that we cannot hope to have if we work with flat base types. To this end, we develop tools that deal adequately with possibly inconsistent finite sets of information. The classical density theorem is reestablished via a ‘finite density theorem,’ and corollaries are obtained, among them Berger's separation property.
Dokumententyp: | Zeitschriftenartikel |
---|---|
Publikationsform: | Publisher's Version |
Fakultät: | Mathematik, Informatik und Statistik > Mathematik |
Themengebiete: | 500 Naturwissenschaften und Mathematik > 510 Mathematik |
URN: | urn:nbn:de:bvb:19-epub-68928-1 |
Allianz-/Nationallizenz: | Dieser Beitrag ist mit Zustimmung des Rechteinhabers aufgrund einer (DFG-geförderten) Allianz- bzw. Nationallizenz frei zugänglich. |
Sprache: | Englisch |
Dokumenten ID: | 68928 |
Datum der Veröffentlichung auf Open Access LMU: | 26. Sep. 2019, 05:10 |
Letzte Änderungen: | 04. Nov. 2020, 13:51 |