scientific article; zbMATH DE number 3556031
From MaRDI portal
Publication:4128540
zbMath0357.02029MaRDI QIDQ4128540
Publication date: 1975
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (81)
Realizability interpretation of generalized inductive definitions ⋮ Metamathematical properties of a constructive multi-typed theory ⋮ The effects of effects on constructivism ⋮ The strength of some Martin-Löf type theories ⋮ Realizability and recursive set theory ⋮ Formalizing non-termination of recursive programs ⋮ Totality in applicative theories ⋮ A feasible theory of truth over combinatory algebra ⋮ Partial combinatory algebra and generalized numberings ⋮ Understanding uniformity in Feferman's explicit mathematics ⋮ On the proof-theoretic strength of monotone induction in explicit mathematics ⋮ Monotone inductive definitions in a constructive theory of functions and classes ⋮ Systems of explicit mathematics with non-constructive \(\mu\)-operator. II ⋮ Semantic types and approximation for Featherweight Java ⋮ Adding proof objects and inductive definition mechanisms to frege structures ⋮ A first order logic of effects ⋮ RELATIVIZING OPERATIONAL SET THEORY ⋮ What does logic have to tell us about mathematical proofs? ⋮ Expressing computational complexity in constructive type theory ⋮ Arithmetical conservation results ⋮ EXTENSIONAL REALIZABILITY AND CHOICE FOR DEPENDENT TYPES IN INTUITIONISTIC SET THEORY ⋮ Choice and independence of premise rules in intuitionistic set theory ⋮ Embeddings between partial combinatory algebras ⋮ IN MEMORIAM: SOLOMON FEFERMAN (1928–2016) ⋮ Admissible closures of polynomial time computable arithmetic ⋮ The Suslin operator in applicative theories: its proof-theoretic analysis via ordinal theories ⋮ The provably terminating operations of the subsystem PETJ of explicit mathematics ⋮ Proof-theoretical analysis: Weak systems of functions and classes ⋮ Theories with self-application and computational complexity. ⋮ Between constructive mathematics and PROLOG ⋮ A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP ⋮ Pure Proof Theory Aims, Methods and Results: Extended Version of Talks Given at Oberwolfach and Haifa ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting) ⋮ Primitive recursive selection functions for existential assertions over abstract algebras ⋮ On Feferman's operational set theory \textsf{OST} ⋮ The Operational Perspective: Three Routes ⋮ Extending constructive operational set theory by impredicative principles ⋮ The axiom of choice and combinatory logic ⋮ A theory for program and data type specification ⋮ A type reduction from proof-conditional to dynamic semantics ⋮ Universes in explicit mathematics ⋮ A proof-theoretic characterization of the basic feasible functionals ⋮ Explicit mathematics: power types and overloading ⋮ Unnamed Item ⋮ Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms ⋮ On uniform weak König's lemma ⋮ TRUNCATION AND SEMI-DECIDABILITY NOTIONS IN APPLICATIVE THEORIES ⋮ Why Sets? ⋮ Operational set theory and small large cardinals ⋮ Feferman on Computability ⋮ Unfolding Schematic Systems ⋮ The Operational Penumbra: Some Ontological Aspects ⋮ Feferman’s Forays into the Foundations of Category Theory ⋮ Proof Theory of Constructive Systems: Inductive Types and Univalence ⋮ Unnamed Item ⋮ Elementary explicit types and polynomial time operations ⋮ Extended bar induction in applicative theories ⋮ A note on complexity measures for inductive classes in constructive type theory ⋮ Full operational set theory with unbounded existential quantification and power set ⋮ Fixed point theorems for precomplete numberings ⋮ Intensionality in mathematics ⋮ COMPUTABILITY IN PARTIAL COMBINATORY ALGEBRAS ⋮ Towards a computation system based on set theory ⋮ The non-constructive \(\mu\) operator, fixed point theories with ordinals, and the bar rule ⋮ Predicativity and constructive mathematics ⋮ Systems of explicit mathematics with non-constructive \(\mu\)-operator and join ⋮ Reflections on reflections in explicit mathematics ⋮ Replacement versus collection and related topics in constructive Zermelo-Fraenkel set theory ⋮ Well-ordering proofs for Martin-Löf type theory ⋮ Realizability and intuitionistic logic ⋮ A well-ordering proof for Feferman's theoryT 0 ⋮ On the Strength of the Uniform Fixed Point Principle in Intuitionistic Explicit Mathematics ⋮ Aspects of Categorical Recursion Theory ⋮ ORDINAL ANALYSIS OF PARTIAL COMBINATORY ALGEBRAS ⋮ A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\) ⋮ On the compatibility between the minimalist foundation and constructive set theory ⋮ Applicative theories for logarithmic complexity classes ⋮ Systems of explicit mathematics with non-constructive \(\mu\)-operator. I ⋮ Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe ⋮ Universes over Frege structures ⋮ Generalizing classical and effective model theory in theories of operations and classes
This page was built for publication:
