A STRONG MULTI-TYPED INTUITIONISTIC THEORY OF FUNCTIONALS.
In this paper we describe an intuitionistic theory SLP. It is a relatively strong theory containing intuitionistic principles for functionals of many types, in particular, the theory of the “creating subject”, axioms for lawless functionals and some versions of choice axioms. We construct a Beth mod...
| Publicado en: | Journal of Symbolic Logic Vol. 80; no. 3; pp. 1035 - 1066 |
|---|---|
| Autor principal: | |
| Formato: | Artículo |
| Publicado: |
Cambridge University Press
Sep2015
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=108608240&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 108608240 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00224812 3TY jtl: Journal of Symbolic Logic issn: 00224812 maglogo: N pubinfo: dt: Sep2015 vid: 80 iid: 3 pid: 15979 pub: Cambridge University Press artinfo: ui: 108608240 10.1017/jsl.2015.21 ppf: 1035 ppct: 31 formats: tig: atl: A STRONG MULTI-TYPED INTUITIONISTIC THEORY OF FUNCTIONALS. aug: au: KACHAPOVA, FARIDA affil: SCHOOL OF COMPUTER AND MATHEMATICAL SCIENCES AUCKLAND UNIVERSITY OF TECHNOLOGY AUCKLAND, NEW ZEALAND E-mail: farida.kachapova@aut.ac.nz su: Intuitionistic mathematics Constructive mathematics Functionals Function spaces Functional analysis sug: subj: Intuitionistic mathematics Constructive mathematics Functionals Function spaces Functional analysis keyword: 03F50 03F55 Beth model consistency creating subject forcing Intuitionistic theory Kripke schema lawless sequence truth predicate ab: In this paper we describe an intuitionistic theory SLP. It is a relatively strong theory containing intuitionistic principles for functionals of many types, in particular, the theory of the “creating subject”, axioms for lawless functionals and some versions of choice axioms. We construct a Beth model for the language of intuitionistic functionals of high types and use it to prove the consistency of SLP.We also prove that the intuitionistic theory SLP is equiconsistent with a classical theory TI. TI is a typed set theory, where the comprehension axiom for sets of type n is restricted to formulas with no parameters of types > n. We show that each fragment of SLP with types ≤ s is equiconsistent with the corresponding fragment of TI and that it is stronger than the previous fragment of SLP. Thus, both SLP and TI are much stronger than the second order arithmetic. By constructing the intuitionistic theory SLP and interpreting in it the classical set theoryTI, we contribute to the program of justifying classical mathematics from the intuitionistic point of view. pubtype: Academic Journal doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2015 holdings: @attributes: islocal: N |
|---|