scientific article

Publication date: 1979

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

survey independence consistency models realizability Bishop's constructive mathematics formalization equivalence in strength

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Metamathematics of constructive systems (03F50)

Related Items (71)

Interpretation of constructive multi-typed theory in the theory of arithmetical truth ⋮ Realizability interpretation of generalized inductive definitions ⋮ Metamathematical properties of a constructive multi-typed theory ⋮ The strength of some Martin-Löf type theories ⋮ Proof-relevance in Bishop-style constructive mathematics ⋮ Formalizing non-termination of recursive programs ⋮ Totality in applicative theories ⋮ A feasible theory of truth over combinatory algebra ⋮ Understanding uniformity in Feferman's explicit mathematics ⋮ On the proof-theoretic strength of monotone induction in explicit mathematics ⋮ Direct spectra of Bishop spaces and their limits ⋮ Monotone inductive definitions in a constructive theory of functions and classes ⋮ Systems of explicit mathematics with non-constructive \(\mu\)-operator. II ⋮ Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels ⋮ Monotone recursive definition of predicates and its realizability interpretation ⋮ A first order logic of effects ⋮ Unnamed Item ⋮ Arithmetical conservation results ⋮ A realizability interpretation of Church's simple theory of types ⋮ EXTENSIONAL REALIZABILITY AND CHOICE FOR DEPENDENT TYPES IN INTUITIONISTIC SET THEORY ⋮ Choice and independence of premise rules in intuitionistic set theory ⋮ 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 ⋮ Proofs and programs: A naïve approach to program extraction ⋮ Theories with self-application and computational complexity. ⋮ Intuitionistic fixed point logic ⋮ A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP ⋮ 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 ⋮ About Truth and Types ⋮ The Operational Perspective: Three Routes ⋮ Objectivity and Truth in Mathematics: A Sober Non-platonist Perspective ⋮ Extending constructive operational set theory by impredicative principles ⋮ Reflection principles for synthetic theories of smooth manifolds ⋮ A theory for program and data type specification ⋮ Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice ⋮ What is constructive 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 ⋮ TRUNCATION AND SEMI-DECIDABILITY NOTIONS IN APPLICATIVE THEORIES ⋮ Why Sets? ⋮ The Operational Penumbra: Some Ontological Aspects ⋮ Proof Theory of Constructive Systems: Inductive Types and Univalence ⋮ Elementary explicit types and polynomial time operations ⋮ Extended bar induction in applicative theories ⋮ A flexible type system for the small Veblen ordinal ⋮ Intensionality in mathematics ⋮ Towards a computation system based on set theory ⋮ The non-constructive \(\mu\) operator, fixed point theories with ordinals, and the bar rule ⋮ Truth and the philosophy of mathematics ⋮ Systems of explicit mathematics with non-constructive \(\mu\)-operator and join ⋮ Constructive mathematics: a foundation for computable analysis ⋮ Remarks on applicative theories ⋮ Reflections on reflections in explicit mathematics ⋮ Replacement versus collection and related topics in constructive Zermelo-Fraenkel set theory ⋮ Extracting Lisp programs from constructive proofs: A formal theory of constructive mathematics based on Lisp ⋮ Realizability and intuitionistic logic ⋮ Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions ⋮ A well-ordering proof for Feferman's theoryT 0 ⋮ On the collection of points of a formal space ⋮ Cut-Elimination for SBL ⋮ On the Strength of the Uniform Fixed Point Principle in Intuitionistic Explicit Mathematics ⋮ A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\) ⋮ 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: