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

proof theoryreal numbersabstract typesbounded functional interpretationfinite type arithmetic

Mathematics Subject Classification ID

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

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

• 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?)
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Bounded functional interpretation
• General logical metatheorems for functional analysis
• 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)

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

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)