scientific article; zbMATH DE number 3231083

zbMath0143.25502MaRDI QIDQ5519134

Clifford Spector

Publication date: 1962

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

zbMATH Keywords

mathematical logic

Related Items (70)

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 L^p 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

This page was built for publication: