Intuitionistic nonstandard bounded modified realisability and functional interpretation

DOI10.1016/J.APAL.2017.12.004MaRDI QIDQ1706266zbMATH OpenOpenAlexFDO

Authors Bruno Dinis, Jaime Gaspar

Publication date 21 March 2018

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1512.07113

zbMATH Keywords

bounded functional interpretationbounded modified realisabilityintuitionismmajorisabilitynonstandard arithmetictransfer principle

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Relative consistency and interpretations (03F25) Second- and higher-order arithmetic and fragments (03F35) Nonstandard arithmetic (number-theoretic aspects) (11U10)

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.

Review text

\textit{F. Ferreira} and \textit{P. Oliva} [Ann. Pure Appl. Logic 135, No. 1--3, 73--112 (2005; Zbl 1095.03060)] introduced bounded functional interpretation for formulae of arithmetic in all finite types with equality only for the objects of type 0 with special treatment of existential statements: it does not provide precise witnesses but only bounds for the witnesses in the sense of Howard-Bezem strong majorizability. The same idea is used in bounded realizability introduced by \textit{F. Ferreira} and \textit{A. Nunes} [J. Symb. Log. 71, No. 1, 329--346 (2006; Zbl 1100.03050)]. Intuitionistic nonstandard arithmetic $\mathsf{E}\text{-}\mathsf{HA}^\omega_{\text{st}}$ was introduced by \textit{B. van den Berg} et al. [Ann. Pure Appl. Logic 163, No. 12, 1962--1994 (2012; Zbl 1270.03121)]. It is an extension of intuitionistic arithmetic in all finite types by adding the predicate $\mathrm{st}$ and appropriate standardness axioms. The same authors defined variants of realizability and functional intepretation similar to the bounded ones, where a bound is replaced by a finite set containing a witness. In the paper under review, bounded functional interpretation and bounded realizability are transferred to $\mathsf{E}\text{-}\mathsf{HA}^\omega_{\mathrm{st}}$ formulae and are used for proving various equiconsistency, conservativity, and independence results.

Recommendations

• Nonstandardness and the bounded functional interpretation
• On bounded functional interpretations
• A functional interpretation for nonstandard arithmetic
• Bounded functional interpretation
• Bounded modified realizability

Cites work

• A functional interpretation for nonstandard arithmetic
• A model for intuitionistic non-standard arithmetic
• Bounded functional interpretation
• Bounded modified realizability
• scientific article; zbMATH DE number 51556 (Why is no real title available?)
• Internal set theory: A new approach to nonstandard analysis
• Interpreting weak Kőnig's lemma in theories of nonstandard arithmetic
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Nonstandard analysis in practice
• Nonstandardness and the bounded functional interpretation
• Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals
• The syntax of nonstandard analysis
• Transfer principles in nonstandard intuitionistic arithmetic

Cited in

(9)

• A note on non-classical nonstandard arithmetic
• Nonstandard functional interpretations and categorical models
• Nonstandardness and the bounded functional interpretation
• A parametrised functional interpretation of Heyting arithmetic
• Weyl and Intuitionistic Infinitesimals
• Hardwiring truth in functional interpretations
• Stateful Realizers for Nonstandard Analysis
• Realizability with stateful computations for nonstandard analysis
• A functional interpretation for nonstandard arithmetic

This page was built for publication: Intuitionistic nonstandard bounded modified realisability and functional interpretation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1706266)