Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
A Constructive Examination of a Russell-style Ramified Type Theory
Stockholms universitet, Naturvetenskapliga fakulteten, Matematiska institutionen.
Rekke forfattare: 12018 (engelsk)Inngår i: Bulletin of Symbolic Logic, ISSN 1079-8986, E-ISSN 1943-5894, Vol. 24, nr 1, s. 90-106Artikkel i tidsskrift (Fagfellevurdert) 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.

sted, utgiver, år, opplag, sider
2018. Vol. 24, nr 1, s. 90-106
Emneord [en]
ramified type theory, intuitionistic logic, reducibility axiom
HSV kategori
Identifikatorer
URN: urn:nbn:se:su:diva-156694DOI: 10.1017/bsl.2018.4ISI: 000431008000003OAI: oai:DiVA.org:su-156694DiVA, id: diva2:1211232
Tilgjengelig fra: 2018-05-30 Laget: 2018-05-30 Sist oppdatert: 2022-02-26bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler i DiVA

Andre lenker

Forlagets fulltekstarXiv:1704.06812

Person

Palmgren, Erik

Søk i DiVA

Av forfatter/redaktør
Palmgren, Erik
Av organisasjonen
I samme tidsskrift
Bulletin of Symbolic Logic

Søk utenfor DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric

doi
urn-nbn
Totalt: 4458 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf