Ü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
No author found.
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 (only showing first 100 items - show all)
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
This page was built for publication: ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
