Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A Constructive Examination of a Russell-style Ramified Type Theory
Stockholm University, Faculty of Science, Department of Mathematics.
2017 (English)Manuscript (preprint) (Other academic)
Abstract [en]

In this paper we examine the natural interpretation of a ramified type hierarchy into Martin-Löf type theory with an infinite sequence of universes. It is shown that under this predicative interpretation some useful special cases of Russell’s reducibility axiom are valid, namely functional reducibility. This is sufficient to make the type hierarchy usable for development of constructive mathematics. We present a ramified type theory suitable for this purpose. One may regard the results of this paper as an alternative solution to the problems of Russell’s theory, which avoids impredicativity, but instead imposes constructive logic. The intuitionistic ramified type theory introduced here, also suggests that there is a natural associated notion of predicative elementary topos. 

Place, publisher, year, edition, pages
2017. , p. 14
Keyword [en]
Type theory, predicativity, Russell's type theory
National Category
Mathematics
Research subject
Mathematical Logic
Identifiers
URN: urn:nbn:se:su:diva-142058OAI: oai:DiVA.org:su-142058DiVA: diva2:1130097
Projects
Konstruktiva och kategoriteoretiska grundvalar för matematik
Funder
Swedish Research Council, 2015-03835
Available from: 2017-08-08 Created: 2017-08-08 Last updated: 2017-10-09

Open Access in DiVA

No full text in DiVA

Other links

arXiv:1704.06812

Search in DiVA

By author/editor
Palmgren, Erik
By organisation
Department of Mathematics
Mathematics

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 1 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf