On the Interpretation of Non-Finitist Proofs--Part I
From MaRDI portal
Publication:5806808
DOI10.2307/2267908zbMath0044.00302OpenAlexW4233221743MaRDI QIDQ5806808
Publication date: 1951
Published in: The Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2267908
Related Items
Hilbert's ‘Verunglückter Beweis’, the first epsilon theorem, and consistency proofs, THE COLLAPSE OF THE HILBERT PROGRAM: A VARIATION ON THE GÖDELIAN THEME, Dependent choice, `quote' and the clock, Asymptotically nonexpansive mappings in uniformly convex hyperbolic spaces, The mathematical significance of proof theory, On the metamathematics of the P vs. NP question, Understanding uniformity in Feferman's explicit mathematics, Herbrand analyses, On extracting variable Herbrand disjunctions, Epsilon substitution method for elementary analysis, Some concepts concerning formal systems of number theory, Platonism and Mathematical Intuition in Kurt Gödel's Thought, On the computational content of convergence proofs via Banach limits, Effective metastability for modified Halpern iterations in CAT(0) spaces, Informal versus formal mathematics, The substitution method, A universal algorithm for Krull's theorem, Hierarchies of number-theoretic predicates, Effectiveness and provability, Gentzen reduction revisited, Alternating (in)dependence-friendly logic, A computational study of a class of recursive inequalities, A proof‐theoretic metatheorem for tracial von Neumann algebras, On quantitative versions of theorems due to F. E. Browder and R. Wittmann, A finitization of Littlewood's Tauberian theorem and an application in Tauberian remainder theory, Stateful Realizers for Nonstandard Analysis, What can be done with PRA?, Realizability algebras III: some examples, Constructive forcing, CPS translations and witness extraction in Interactive realizability, Classical realizability and arithmetical formulæ, Consequences of an exotic definition for \(\text{P}=\text{NP}\)., On modified Halpern and Tikhonov-Mann iterations, Proof mining and effective bounds in differential polynomial rings, The finitary content of sunny nonexpansive retractions, Rates of convergence and metastability for abstract Cauchy problems generated by accretive operators, Norm convergence of multiple ergodic averages for commuting transformations, The Ω-consistency of ramified analysis, Well Quasi-orders and the Functional Interpretation, Verificationism and Classical Realizability, Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs, A new deconstructive logic: linear logic, On the quantitative asymptotic behavior of strongly nonexpansive mappings in Banach and geodesic spaces, Norm convergence of multiple ergodic averages on amenable groups, Another proof of the intuitionistic Ramsey theorem, On the asymptotic behavior of odd operators, A complexity analysis of functional interpretations, Effective metastability of Halpern iterates in \(CAT(0)\) spaces, Ackermann's substitution method (remixed), On the No-Counterexample Interpretation, The metamathematics of ergodic theory, On Herbrand's theorem, A method of epsilon substitution for the predicate logic with equality, Remarks on Herbrand normal forms and Herbrand realizations, Arithmetical Predicates and Function Quantifiers, The Gödelian Inferences, Local stability of ergodic averages, Unnamed Item, Strong termination for the epsilon substitution method, On preserving the computational content of mathematical proofs: toy examples for a formalising strategy
