On the interpretation of non-finitist proofs–Part II
From MaRDI portal
Publication:5809142
DOI10.2307/2267457zbMath0046.00701OpenAlexW4206658284MaRDI QIDQ5809142
Publication date: 1952
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2267457
Related Items
On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem, How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study, THE COLLAPSE OF THE HILBERT PROGRAM: A VARIATION ON THE GÖDELIAN THEME, Dependent choice, `quote' and the clock, Nonlinearity of Davenport-Schinzel sequences and of generalized path compression schemes, The mathematical significance of proof theory, Herbrand analyses, Computability and Analysis, a Historical Approach, On extracting variable Herbrand disjunctions, Investigations on slow versus fast growing: How to majorize slow growing functions nontrivially by fast growing ones, Epsilon substitution method for elementary analysis, Hierarchies of number-theoretic functions. I, Slow reflection, A Combinatorial Approach to Complexity Theory via Ordinal Hierarchies, On the computational content of convergence proofs via Banach limits, Effective metastability for modified Halpern iterations in CAT(0) spaces, Nested recursion, A classification of the ordinal recursive functions, Informal versus formal mathematics, A universal algorithm for Krull's theorem, A UNIFORM QUANTITATIVE FORM OF SEQUENTIAL WEAK COMPACTNESS AND BAILLON'S NONLINEAR ERGODIC THEOREM, 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, Functorial Fast-Growing Hierarchies, Realizability algebras III: some examples, Mining the surface: witnessing the low complexity theorems of arithmetic, Classical realizability and arithmetical formulæ, On modified Halpern and Tikhonov-Mann iterations, Beweistheoretische Charakterisierung einer Erweiterung der Grzegorczyk-Hierarchie, Proof-theoretical analysis: Weak systems of functions and classes, Effective results on nonlinear ergodic averages in CAT spaces, 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, Well Quasi-orders and the Functional Interpretation, Verificationism and Classical Realizability, Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs, Fifty years of the spectrum problem: survey and new results, On the quantitative asymptotic behavior of strongly nonexpansive mappings in Banach and geodesic spaces, Fast growing functions based on Ramsey theorems, Subsystems of true arithmetic and hierarchies of functions, Proof lengths for instances of the Paris-Harrington principle, The computational content of arithmetical proofs, A constructive interpretation of Ramsey's theorem via the product of selection functions, On the asymptotic behavior of odd operators, A complexity analysis of functional interpretations, Effective metastability of Halpern iterates in \(CAT(0)\) spaces, On the No-Counterexample Interpretation, Unnamed Item, A new application for explanation-based generalisation within automated deduction, On Herbrand's theorem, A method of epsilon substitution for the predicate logic with equality, The Gödelian Inferences, A note on inverses of elementary permutations, Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\), Finite notations for infinite terms, Unnamed Item, Strong termination for the epsilon substitution method, Classifying the Provably Total Functions of PA, On preserving the computational content of mathematical proofs: toy examples for a formalising strategy, The epsilon calculus and Herbrand complexity
