scientific article; zbMATH DE number 3687373
From MaRDI portal
Publication:3882452
zbMATH Open0441.03022MaRDI QIDQ3882452FDOQ3882452
Publication date: 1979
Title of this publication is not available (Why is that?)
surveyconsistencyindependencemodelsrealizabilityBishop's constructive mathematicsformalizationequivalence in strength
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Metamathematics of constructive systems (03F50)
Cited In (73)
- What is constructive mathematics?
- A flexible type system for the small Veblen ordinal
- Interpretation of constructive multi-typed theory in the theory of arithmetical truth
- Universes over Frege structures
- Reflections on reflections in explicit mathematics
- A first order logic of effects
- The strength of some Martin-Löf type theories
- Extending constructive operational set theory by impredicative principles
- A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\)
- Explicit mathematics: power types and overloading
- Cut-Elimination for SBL
- Monotone inductive definitions in a constructive theory of functions and classes
- Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels
- The Operational Perspective: Three Routes
- The non-constructive \(\mu\) operator, fixed point theories with ordinals, and the bar rule
- Monotone recursive definition of predicates and its realizability interpretation
- Constructive mathematics: a foundation for computable analysis
- Elementary explicit types and polynomial time operations
- Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice
- Systems of explicit mathematics with non-constructive \(\mu\)-operator. I
- Totality in applicative theories
- On the proof-theoretic strength of monotone induction in explicit mathematics
- Direct spectra of Bishop spaces and their limits
- A well-ordering proof for Feferman's theoryT 0
- A theory for program and data type specification
- Proof-relevance in Bishop-style constructive mathematics
- Remarks on applicative theories
- Systems of explicit mathematics with non-constructive \(\mu\)-operator. II
- Title not available (Why is that?)
- Extended bar induction in applicative theories
- TRUNCATION AND SEMI-DECIDABILITY NOTIONS IN APPLICATIVE THEORIES
- Towards a computation system based on set theory
- A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP
- Intensionality in mathematics
- Systems of explicit mathematics with non-constructive \(\mu\)-operator and join
- A proof-theoretic characterization of the basic feasible functionals
- 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
- Realizability interpretation of generalized inductive definitions
- Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms
- About Truth and Types
- Replacement versus collection and related topics in constructive Zermelo-Fraenkel set theory
- On the Strength of the Uniform Fixed Point Principle in Intuitionistic Explicit Mathematics
- Proof-theoretical analysis: Weak systems of functions and classes
- Extracting Lisp programs from constructive proofs: A formal theory of constructive mathematics based on Lisp
- On the collection of points of a formal space
- Arithmetical conservation results
- Formalizing non-termination of recursive programs
- Proofs and programs: A naïve approach to program extraction
- Theories with self-application and computational complexity.
- Realizability and intuitionistic logic
- Truth and the philosophy of mathematics
- Intuitionistic fixed point logic
- Title not available (Why is that?)
- Proof Theory of Constructive Systems: Inductive Types and Univalence
- Why Sets?
- Generalizing classical and effective model theory in theories of operations and classes
- Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe
- Primitive recursive selection functions for existential assertions over abstract algebras
- Understanding uniformity in Feferman's explicit mathematics
- Choice and independence of premise rules in intuitionistic set theory
- Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
- A realizability interpretation of Church's simple theory of types
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)
- Sets completely separated by functions in Bishop set theory
- A feasible theory of truth over combinatory algebra
- Metamathematical properties of a constructive multi-typed theory
- Reflection principles for synthetic theories of smooth manifolds
- Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory
- EXTENSIONAL REALIZABILITY AND CHOICE FOR DEPENDENT TYPES IN INTUITIONISTIC SET THEORY
- Objectivity and Truth in Mathematics: A Sober Non-platonist Perspective
- The Operational Penumbra: Some Ontological Aspects
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3882452)
