ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
From MaRDI portal
Publication:3262780
DOI10.1111/j.1746-8361.1958.tb01464.xzbMath0090.01003OpenAlexW1525064220WikidataQ55897078 ScholiaQ55897078MaRDI QIDQ3262780
Publication date: 1958
Published in: Dialectica (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1111/j.1746-8361.1958.tb01464.x
Related Items
Proof mining in \(L_{1}\)-approximation ⋮ Automatic synthesis of typed \(\Lambda\)-programs on term algebras ⋮ Representations and the foundations of mathematics ⋮ The intuitionistic fragment of computability logic at the propositional level ⋮ Parametric Church's thesis: synthetic computability without choice ⋮ Dialectica logical principles ⋮ On extracting variable Herbrand disjunctions ⋮ Binary refinement implies discrete exponentiation ⋮ Investigations on slow versus fast growing: How to majorize slow growing functions nontrivially by fast growing ones ⋮ Bounded functional interpretation and feasible analysis ⋮ A parametrised functional interpretation of Heyting arithmetic ⋮ A herbrandized functional interpretation of classical first-order logic ⋮ A decidable theory of type assignment ⋮ On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory ⋮ Gödel's incompleteness theorems. On the occasion of Kurt Gödel's 100th anniversary on April 28, 2006 ⋮ Polymorphic extensions of simple type structures. With an application to a bar recursive minimization ⋮ The machinery of consistency proofs ⋮ Book review of: R. Kahle (ed.) and M. Rathjen (ed.), Gentzen's centenary. The quest for consistency ⋮ Human rationality challenges universal logic ⋮ Beweistheoretische Abgrenzung von Teilsystemen der Analysis ⋮ To be or not to be constructive, that is not the question ⋮ Canonicity and normalization for dependent type theory ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ On quantitative versions of theorems due to F. E. Browder and R. Wittmann ⋮ Dialectica principles via Gödel doctrines ⋮ A finitization of Littlewood's Tauberian theorem and an application in Tauberian remainder theory ⋮ Jean van Heijenoort's contributions to proof theory and its history ⋮ Intuitionist type theory and the free topos ⋮ On bounded functional interpretations ⋮ On the computational complexity of cut-reduction ⋮ Light Dialectica revisited ⋮ Identity and intensionality in univalent foundations and philosophy ⋮ The bounded functional interpretation of bar induction ⋮ Proofs and programs: A naïve approach to program extraction ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ Proof mining and effective bounds in differential polynomial rings ⋮ Gödel functional interpretation and weak compactness ⋮ Pre-recursive categories ⋮ Fatal Heyting algebras and forcing persistent sentences ⋮ Binary trees as a computational framework ⋮ Things that can and things that cannot be done in PRA ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting) ⋮ Explicit Provability and Constructive Semantics ⋮ Extraction of expansion trees ⋮ Book review of: K. Gödel, Collected works. Vol. IV: Correspondence, A--G; Collected works. Vol. V: Correspondence, H--Z ⋮ A game semantics for linear logic ⋮ Herbrand's theorem as higher order recursion ⋮ On the concept of finitism ⋮ Bar recursion over finite partial functions ⋮ Functional interpretations of feasibly constructive arithmetic ⋮ Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation ⋮ Subrecursive hierarchies on Scott domains ⋮ The scope of Gödel's first incompleteness theorem ⋮ Functional interpretations of linear and intuitionistic logic ⋮ Programs from proofs using classical dependent choice ⋮ The undecidability of pattern matching in calculi where primitive recursive functions are representable ⋮ The computational content of arithmetical proofs ⋮ Extracting Herbrand disjunctions by functional interpretation ⋮ Non-classical propositional calculi in relation to methodological patterns of scientific investigation ⋮ Bounded functional interpretation ⋮ Consistency, models, and soundness ⋮ A complexity analysis of functional interpretations ⋮ Continuous normalization for the lambda-calculus and Gödel's T ⋮ Uniform Heyting arithmetic ⋮ On the form of witness terms ⋮ Effective metastability of Halpern iterates in \(CAT(0)\) spaces ⋮ An arithmetic for polynomial-time computation ⋮ Computability in higher types, P\(\omega\) and the completeness of type assignment ⋮ A survey of predicate realizability logic ⋮ On the Cantor–Bendixson rank of a set that is searchable in Gödel’s T ⋮ On paradoxes in normal form ⋮ Kurt Gödel's intellectual development. [In memoriam Kurt Gödel (28 April 1906 -- 14 January 1978).] ⋮ The metamathematics of ergodic theory ⋮ Injecting uniformities into Peano arithmetic ⋮ Metastability of the proximal point algorithm with multi-parameters ⋮ Georg Cantor as the author of constructions playing fundamental roles in constructive mathematics ⋮ Realizability interpretation of proofs in constructive analysis ⋮ Reverse formalism 16 ⋮ An indeterminate universe of sets ⋮ A unary representation result for system \(T\) ⋮ Ptykes in Gödels T und Definierbarkeit von Ordinalzahlen. (Ptykes in Gödel's T and definability of ordinal numbers) ⋮ An arithmetic for non-size-increasing polynomial-time computation ⋮ On the removal of weak compactness arguments in proof mining ⋮ Induction, Coinduction, and Adjoints ⋮ Feasible functionals and intersection of ramified types ⋮ Higher type recursion, ramification and polynomial time ⋮ Functional interpretation of Aczel's constructive set theory ⋮ Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\) ⋮ A common axiom set for classical and intuitionistic plane geometry ⋮ On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness ⋮ Ramified recurrence and computational complexity. III: Higher type recurrence and elementary complexity ⋮ An equational variant of Lawvere's natural numbers object ⋮ Realizability and intuitionistic logic ⋮ A proof description language and its reduction system ⋮ ``Gaisi Takeuti's finitist standpoint and its mathematical embodiment ⋮ Studies in constructive mathematics and mathematical logic. Part IX ⋮ Propositions and specifications of programs in Martin-Löf's type theory ⋮ Nonstandardness and the bounded functional interpretation ⋮ Pointwise hereditary majorization and some applications ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction ⋮ Stateful Realizers for Nonstandard Analysis ⋮ On computational properties of Cauchy problems generated by accretive operators ⋮ CHAD for expressive total languages ⋮ Platonism and the Proto-ontology of Mathematics: Learning from the Axiom of Choice ⋮ Relative constructivity ⋮ How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study ⋮ Intensional interpretations of functionals of finite type I ⋮ AFFINE LOGIC FOR CONSTRUCTIVE MATHEMATICS ⋮ A survey of proof theory ⋮ Measure theory and higher order arithmetic ⋮ Programming and Proving with Classical Types ⋮ NON-PRINCIPAL ULTRAFILTERS, PROGRAM EXTRACTION AND HIGHER-ORDER REVERSE MATHEMATICS ⋮ On Spector's bar recursion ⋮ Light monotone Dialectica methods for proof mining ⋮ Gentzen's Proof Systems: Byproducts in a Work of Genius ⋮ Term extraction and Ramsey's theorem for pairs ⋮ Unnamed Item ⋮ Some logical metatheorems with applications in functional analysis ⋮ A NEW COMPUTATION OF THE Σ-ORDINAL OF KPω ⋮ Strong normalization of barrecursive terms without using infinite terms ⋮ New effective moduli of uniqueness and uniform a priori estimates for constants of strong unicity by logical analysis of known proofs in best approximation theory ⋮ Ein Henkin-Vollständigkeitsbeweis für die intuitionistische Prädikatelogik bezüglich der Kripke-Semantik ⋮ Global quantification in Zermelo-Fraenkel set theory ⋮ Simultane Rekursionen in der Theorie der Funktionale endlicher Typen ⋮ THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY ⋮ Platonism and Mathematical Intuition in Kurt Gödel's Thought ⋮ Size-based termination of higher-order rewriting ⋮ A classification of the ordinal recursive functions ⋮ Computational Complexity Via Finite Types ⋮ A dialectica-like model of linear logic ⋮ Hardwiring truth in functional interpretations ⋮ A UNIFORM QUANTITATIVE FORM OF SEQUENTIAL WEAK COMPACTNESS AND BAILLON'S NONLINEAR ERGODIC THEOREM ⋮ A user's friendly syntax to define recursive functions as typed λ-terms ⋮ Intrinsic theories and computational complexity ⋮ Provably total functions of intuitionistic bounded arithmetic ⋮ Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization ⋮ Extending the Curry-Howard interpretation to linear, relevant and other resource logics ⋮ A proof‐theoretic metatheorem for tracial von Neumann algebras ⋮ A Formal Proof of the Strong Normalization Theorem for System T in Agda ⋮ On the Herbrand functional interpretation ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A system of abstract constructive ordinals ⋮ Unnamed Item ⋮ The finitary content of sunny nonexpansive retractions ⋮ Computability and Recursion ⋮ Well Quasi-orders and the Functional Interpretation ⋮ Well-Partial Orderings and their Maximal Order Types ⋮ NOMINALISTIC ORDINALS, RECURSION ON HIGHER TYPES, AND FINITISM ⋮ A DIRECT PROOF OF SCHWICHTENBERG’S BAR RECURSION CLOSURE THEOREM ⋮ Objectivity and Truth in Mathematics: A Sober Non-platonist Perspective ⋮ From Mathesis Universalis to Provability, Computability, and Constructivity ⋮ Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs ⋮ On Relating Theories: Proof-Theoretical Reduction ⋮ Structural recursion with locally scoped names ⋮ The bounded functional interpretation of the double negation shift ⋮ On weak completeness of intuitionistic predicate logic ⋮ Dialectica Interpretation with Fine Computational Control ⋮ Spielquantorinterpretation unstetiger Funktionale der höheren Analysis ⋮ Interactive Realizability for second-order Heyting arithmetic with EM1 and SK1 ⋮ A constructive interpretation of Ramsey's theorem via the product of selection functions ⋮ Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen ⋮ Unnamed Item ⋮ The work of Kurt Gödel ⋮ A sequent calculus for type assignment ⋮ Unnamed Item ⋮ On the computational content of the Bolzano-Weierstraß Principle ⋮ Unnamed Item ⋮ General logical metatheorems for functional analysis ⋮ XI Latin American Symposium on Mathematical Logic ⋮ On the No-Counterexample Interpretation ⋮ Logical problems of functional interpretations ⋮ Proof theory in the abstract ⋮ On uniform weak König's lemma ⋮ Intrinsic reasoning about functional programs. I: First order theories ⋮ Finite methods in 1-order formalisms ⋮ INTERRELATION BETWEEN WEAK FRAGMENTS OF DOUBLE NEGATION SHIFT AND RELATED PRINCIPLES ⋮ Least and Greatest Fixpoints in Game Semantics ⋮ On the Computability of the Fan Functional ⋮ Extensions of the Finitist Point of View ⋮ On the non-confluence of cut-elimination ⋮ Mathematical and Technological Computability ⋮ Functional Interpretations of Intuitionistic Linear Logic ⋮ Complexity of Gödel’s T in λ-Formulation ⋮ THE HERBRAND FUNCTIONAL INTERPRETATION OF THE DOUBLE NEGATION SHIFT ⋮ Bounded modified realizability ⋮ Interpretationen der Heyting-Arithmetik endlicher Typen ⋮ Local stability of ergodic averages ⋮ Sequential games and optimal strategies ⋮ Functional interpretation and inductive definitions ⋮ Logical aspects of rates of convergence in metric spaces ⋮ Proof-Theoretic Semantics and Feasibility ⋮ Gödel and Intuitionism ⋮ BAR RECURSION AND PRODUCTS OF SELECTION FUNCTIONS ⋮ ON IDEMPOTENT ULTRAFILTERS IN HIGHER-ORDER REVERSE MATHEMATICS ⋮ Primitive Recursive Arithmetic and Its Role in the Foundations of Arithmetic: Historical and Philosophical Reflections ⋮ Program Testing and the Meaning Explanations of Intuitionistic Type Theory ⋮ Classifying the Provably Total Functions of PA ⋮ A Glimpse of $$ \sum_{3} $$-elementarity ⋮ Aspects of Categorical Recursion Theory ⋮ Light Dialectica Program Extraction from a Classical Fibonacci Proof ⋮ Higher order functions and Brouwer’s thesis ⋮ Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
