scientific article; zbMATH DE number 3231083

From MaRDI portal

zbMath0143.25502MaRDI QIDQ5519134

Clifford Spector

Publication date: 1962


Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.



Related Items

A constructive consistency proof of a fragment of set theory, Dialogues and Proofs; Yankov’s Contribution to Proof Theory, On the Performance of Axiom Systems, On Spector's bar recursion, Effective results on a fixed point algorithm for families of nonlinear mappings, Term extraction and Ramsey's theorem for pairs, Some logical metatheorems with applications in functional analysis, Strong normalization of barrecursive terms without using infinite terms, Equivalence of bar recursors in the theory of functionals of finite type, Simultane Rekursionen in der Theorie der Funktionale endlicher Typen, The strength of countable saturation, Polymorphic extensions of simple type structures. With an application to a bar recursive minimization, Hyperanalytic Predicates, A universal algorithm for Krull's theorem, Equivalence of bar induction and bar recursion for continuous functions with continuous moduli, The equivalence of bar recursion and open recursion, Beweistheoretische Abgrenzung von Teilsystemen der Analysis, The Peirce translation, On quantitative versions of theorems due to F. E. Browder and R. Wittmann, Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language, Constructive forcing, CPS translations and witness extraction in Interactive realizability, Light Dialectica revisited, The bounded functional interpretation of bar induction, Unnamed Item, Delimited control operators prove double-negation shift, Gödel functional interpretation and weak compactness, The finitary content of sunny nonexpansive retractions, Characterising Brouwer's continuity by bar recursion on moduli of continuity, An application of proof mining to nonlinear iterations, Well Quasi-orders and the Functional Interpretation, A DIRECT PROOF OF SCHWICHTENBERG’S BAR RECURSION CLOSURE THEOREM, Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs, The abstract type of the real numbers, Selection functions, bar recursion and backward induction, Bar recursion over finite partial functions, A domain model characterising strong normalisation, Unnamed Item, A Logical Uniform Boundedness Principle for Abstract Metric and Hyperbolic Spaces, Spielquantorinterpretation unstetiger Funktionale der höheren Analysis, Extracting Herbrand disjunctions by functional interpretation, Bounded functional interpretation, A complexity analysis of functional interpretations, Strongly uniform bounds from semi-constructive proofs, On the computational content of the Bolzano-Weierstraß Principle, Unnamed Item, General logical metatheorems for functional analysis, Logical problems of functional interpretations, On uniform weak König's lemma, INTERRELATION BETWEEN WEAK FRAGMENTS OF DOUBLE NEGATION SHIFT AND RELATED PRINCIPLES, PROOF MINING IN Lp SPACES, Continuous Functions on Final Coalgebras, Metastability of the proximal point algorithm with multi-parameters, A Coalgebraic View of Bar Recursion and Bar Induction, Iterated Inductive Definitions Revisited, Theory of proofs (arithmetic and analysis), Extended bar induction in applicative theories, THE HERBRAND FUNCTIONAL INTERPRETATION OF THE DOUBLE NEGATION SHIFT, Unnamed Item, A note on the monotone functional interpretation, On the removal of weak compactness arguments in proof mining, Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\), On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness, Gödel and Intuitionism, Unnamed Item, Primitive Recursive Arithmetic and Its Role in the Foundations of Arithmetic: Historical and Philosophical Reflections, Higher order functions and Brouwer’s thesis, Set recursion and \(\Pi ^ 1_ 2\)-logic, Pointwise hereditary majorization and some applications, Lorenzen and Constructive Mathematics, On false Heine/Borel compactness principles in proof mining