Proof-relevance in Bishop-style constructive mathematics

DOI10.1017/S0960129522000159MaRDI QIDQ5055489zbMATH OpenOpenAlexWikidataFDO

Authors Iosif Petrakis

Publication date 9 December 2022

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1017/s0960129522000159

zbMATH Keywords

BHK-interpretationBishop setsconstructive mathematicsproof-relevance

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• Constructive Mathematics
• Church's thesis and Bishop's constructivism
• Constructive set theory with operations
• Constructive Mathematics in Theory and Programming Practice
• scientific article; zbMATH DE number 2233169

Cites work

• A constructive function-theoretic approach to topological compactness
• A course in constructive algebra
• Algebras of complemented subsets
• Bases of Pseudocompact Bishop Spaces
• Borel and Baire sets in Bishop spaces
• Closed subsets in Bishop topological groups
• Completely regular Bishop spaces
• Constructing categories and setoids of setoids in type theory
• Constructive measure theory
• Constructive topology of Bishop spaces
• Constructive uniformities of pseudometrics and Bishop topologies
• Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets
• Countable Choice as a Questionable Uniformity Principle
• Direct spectra of Bishop spaces and their limits
• Embeddings of Bishop spaces
• Functions of Baire class one over a Bishop topology
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 4002093 (Why is no real title available?)
• scientific article; zbMATH DE number 4070894 (Why is no real title available?)
• scientific article; zbMATH DE number 3687373 (Why is no real title available?)
• scientific article; zbMATH DE number 3726339 (Why is no real title available?)
• scientific article; zbMATH DE number 1217494 (Why is no real title available?)
• scientific article; zbMATH DE number 1302061 (Why is no real title available?)
• scientific article; zbMATH DE number 1795226 (Why is no real title available?)
• scientific article; zbMATH DE number 7561488 (Why is no real title available?)
• scientific article; zbMATH DE number 3291139 (Why is no real title available?)
• scientific article; zbMATH DE number 3325567 (Why is no real title available?)
• Intuitionism and proof theory. Proceedings of the summer conference at Buffalo N. Y. 1968
• Proof-relevance in Bishop-style constructive mathematics
• Proofs and computations
• Reuniting the antipodes---constructive and nonstandard views of the continuum. Symposium proceedings, San Servolo, Venice, Italy, May 16--22, 1999
• The Urysohn extension theorem for Bishop spaces

Cited in

(10)

• Closed subsets in Bishop topological groups
• Bishop-Style Constructive Reverse Mathematics
• Proof-relevance in Bishop-style constructive mathematics
• Sets completely separated by functions in Bishop set theory
• Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory
• Strong negation in the theory of computable functionals TCF
• On the Weihrauch degree of the additive Ramsey theorem
• Hilbert's tenth problem for term algebras with a substitution operator
• Complemented subsets and Boolean-valued, partial functions
• A predicative approach to the constructive integration theory of locally compact metric spaces

This page was built for publication: Proof-relevance in Bishop-style constructive mathematics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5055489)