scientific article; zbMATH DE number 1215497
From MaRDI portal
Publication:4215634
zbMath0913.03053MaRDI QIDQ4215634
Solomon Feferman, Jeremy Avigad
Publication date: 8 December 1998
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
arithmeticDialectica interpretationfunctional interpretationinductive definitionssubsystems of analysisconstructive content of arithmetic and analysisconstructive interpretationdouble negation translationsGödel functionals of higher typespredicative subsystemssecond order arithmetic and its subsystems
Constructive and recursive analysis (03F60) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) First-order arithmetic and fragments (03F30) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55)
Related Items
Proof mining in \(L_{1}\)-approximation, Countable sets versus sets that are countable in reverse mathematics, Representations and the foundations of mathematics, Measure theory and higher order arithmetic, ON THE UNCOUNTABILITY OF, Refining the taming of the reverse mathematics zoo, Reverse mathematics and parameter-free transfer, Light monotone Dialectica methods for proof mining, Betwixt Turing and Kleene, Dialectica logical principles, Term extraction and Ramsey's theorem for pairs, Bounded functional interpretation and feasible analysis, A MARRIAGE OF BROUWER’S INTUITIONISM AND HILBERT’S FINITISM I: ARITHMETIC, A parametrised functional interpretation of Heyting arithmetic, A herbrandized functional interpretation of classical first-order logic, The strength of countable saturation, Gödel's incompleteness theorems. On the occasion of Kurt Gödel's 100th anniversary on April 28, 2006, Splittings and disjunctions in reverse mathematics, Lifting proofs from countable to uncountable mathematics, Equivalence of bar induction and bar recursion for continuous functions with continuous moduli, To be or not to be constructive, that is not the question, A note on the finitization of Abelian and Tauberian theorems, Interpreting weak Kőnig's lemma in theories of nonstandard arithmetic, A note on equality in finite‐type arithmetic, Dialectica principles via Gödel doctrines, Recursion in Higher Types and Resource Bounded Turing Machines, A finitization of Littlewood's Tauberian theorem and an application in Tauberian remainder theory, The FAN principle and weak König's lemma in Herbrandized second-order arithmetic, The non-normal abyss in Kleene's computability theory, On the computational properties of the uncountability of the real numbers, Mining the surface: witnessing the low complexity theorems of arithmetic, Explorations in Subexponential Non-associative Non-commutative Linear Logic, Light Dialectica revisited, The bounded functional interpretation of bar induction, Unnamed Item, Proof mining and effective bounds in differential polynomial rings, Characterising Brouwer's continuity by bar recursion on moduli of continuity, Unnamed Item, Well Quasi-orders and the Functional Interpretation, The consistency of arithmetic, Primitive recursive selection functions for existential assertions over abstract algebras, Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs, Reverse mathematics of topology: dimension, paracompactness, and splittings, Harrington's conservation theorem redone, Herbrand's theorem as higher order recursion, Bar recursion over finite partial functions, Non-determinism in Gödel's system \(T\), Functional interpretations of linear and intuitionistic logic, Bounded functional interpretation, Categorical relationships between Goguen sets and ``two-sided categorical models of linear logic, A complexity analysis of functional interpretations, On the computational content of the Bolzano-Weierstraß Principle, Notes on constructive negation, Logical problems of functional interpretations, On uniform weak König's lemma, INTERRELATION BETWEEN WEAK FRAGMENTS OF DOUBLE NEGATION SHIFT AND RELATED PRINCIPLES, Proof interpretations with truth, COMPUTABILITY THEORY, NONSTANDARD ANALYSIS, AND THEIR CONNECTIONS, The metamathematics of ergodic theory, Injecting uniformities into Peano arithmetic, Metastability of the proximal point algorithm with multi-parameters, Weak König's lemma in Herbrandized classical second-order arithmetic, On Some Semi-constructive Theories Related to Kripke–Platek Set Theory, Complexity-theoretic hierarchies induced by fragments of Gödel's \(T\), Monoidal-closed categories of tree automata, Reverse formalism 16, An indeterminate universe of sets, Pincherle's theorem in reverse mathematics and computability theory, Functional Interpretations of Intuitionistic Linear Logic, On the mathematical and foundational significance of the uncountable, Local stability of ergodic averages, Nets and reverse mathematics, The strength of compactness in computability theory and nonstandard analysis, Functional interpretation of Aczel's constructive set theory, Light Dialectica Program Extraction from a Classical Fibonacci Proof, Nonstandardness and the bounded functional interpretation, A new model construction by making a detour via intuitionistic theories. III: Ultrafinitistic proofs of conservations of \(\Sigma_1^1\) collection, EFFECTIVE INSEPARABILITY, LATTICES, AND PREORDERING RELATIONS, Formally computing with the non-computable
