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 (59)
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
This page was built for publication: On the Interpretation of Non-Finitist Proofs--Part I
