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.
Number of Authors: 12018 (English)In: Bulletin of Symbolic Logic, ISSN 1079-8986, E-ISSN 1943-5894, Vol. 24, no 1, p. 90-106Article in journal (Refereed) Published
Abstract [en]

In this article we examine the natural interpretation of a ramified type hierarchy into Martin-Lof 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 mathematical analysis in the style of Bishop. We present a ramified type theory suitable for this purpose. One may regard the results of this article as an alternative solution to the problem of the proliferation of levels of real numbers in 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
2018. Vol. 24, no 1, p. 90-106
Keywords [en]
ramified type theory, intuitionistic logic, reducibility axiom
National Category
Mathematics Computer and Information Sciences
Identifiers
URN: urn:nbn:se:su:diva-156694DOI: 10.1017/bsl.2018.4ISI: 000431008000003OAI: oai:DiVA.org:su-156694DiVA, id: diva2:1211232
Available from: 2018-05-30 Created: 2018-05-30 Last updated: 2022-02-26Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textarXiv:1704.06812

Authority records

Palmgren, Erik

Search in DiVA

By author/editor
Palmgren, Erik
By organisation
Department of Mathematics
In the same journal
Bulletin of Symbolic Logic
MathematicsComputer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 4437 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