|
|||||
|
|
Intuitionistic nonstandard bounded modified realisability and functional interpretation |
|
| Authors: | Bruno Dinis Jaime Gaspar |
| Institution: | 1. Departamento de Matemática, Faculdade de Ciências da Universidade de Lisboa, Campo Grande, Edifício C6, 1749-016 Lisboa, Portugal;2. School of Computing, University of Kent, Canterbury, Kent, CT2 7NF, United Kingdom;3. Centro de Matemática e Aplicações (CMA), FCT, UNL, Portugal |
| Abstract: | We present a bounded modified realisability and a bounded functional interpretation of intuitionistic nonstandard arithmetic with nonstandard principles.The functional interpretation is the intuitionistic counterpart of Ferreira and Gaspar's functional interpretation and has similarities with Van den Berg, Briseid and Safarik's functional interpretation but replacing finiteness by majorisability.We give a threefold contribution: constructive content and proof-theoretical properties of nonstandard arithmetic; filling a gap in the literature; being in line with nonstandard methods to analyse compactness arguments. |
| Keywords: | 03B20 03F25 03F35 11U10 Intuitionism Bounded functional interpretation Bounded modified realisability Majorisability Nonstandard arithmetic Transfer principle |
| 本文献已被 ScienceDirect 等数据库收录！ | |