The abstract type of the real numbers

DOI10.1007/S00153-021-00772-9MaRDI QIDQ2238151zbMATH OpenOpenAlexFDO

Authors Yanyan Li

Publication date 29 October 2021

Published in Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00153-021-00772-9

zbMATH Keywords

abstract typesbounded functional interpretationfinite type arithmeticproof theoryreal numbers

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) Functionals in proof theory (03F10) Relative consistency and interpretations (03F25) Second- and higher-order arithmetic and fragments (03F35) Continua and generalizations (54F15)

Review text

The author provides an axiomatization for finite type arithmetic appending an abstract type for the real numbers. Typically, finite type arithmetic encodes reals with rapidly converging Cauchy sequences of rationals. The introduction of the abstract type sidesteps this translation. The principles associated with the added type facilitate applications of the bounded functional interpretation as described in the appendix. For more detail on abstract types within the bounded functional interpretation see the work of [\textit{P. Engrácia} and \textit{F. Ferreira}, Landsc. Log. 1, 87--112 (2020; Zbl 1505.03126)].

Recommendations

• Abstract datatypes for real numbers in type theory
• An abstract data type for real numbers
• scientific article; zbMATH DE number 7377974
• Constructive analysis, types and exact real numbers
• An abstract data type for real numbers

Cites work

• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Bounded functional interpretation
• General logical metatheorems for functional analysis
• scientific article; zbMATH DE number 956475 (Why is no real title available?)
• scientific article; zbMATH DE number 1226875 (Why is no real title available?)
• scientific article; zbMATH DE number 7377974 (Why is no real title available?)
• scientific article; zbMATH DE number 3231083 (Why is no real title available?)
• scientific article; zbMATH DE number 3248792 (Why is no real title available?)
• scientific article; zbMATH DE number 3291139 (Why is no real title available?)
• Injecting uniformities into Peano arithmetic
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Nicht konstruktiv beweisbare Sätze der Analysis
• On the removal of weak compactness arguments in proof mining
• PROOF-THEORETIC METHODS IN NONLINEAR ANALYSIS
• Some logical metatheorems with applications in functional analysis
• Spector’s Proof of the Consistency of Analysis
• Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals

Cited in

(4)

• An abstract data type for real numbers
• Abstract datatypes for real numbers in type theory
• Proof mining and the convex feasibility problem: the curious case of Dykstra's algorithm
• A concrete model of the real numbers

This page was built for publication: The abstract type of the real numbers

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