{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:19:21Z","timestamp":1759637961648,"version":"3.40.5"},"reference-count":47,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2022,5,31]],"date-time":"2022-05-31T00:00:00Z","timestamp":1653955200000},"content-version":"unspecified","delay-in-days":150,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2022,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Bishop\u2019s presentation of his informal system of constructive mathematics BISH was on purpose closer to the proof-irrelevance of classical mathematics, although a form of proof-relevance was evident in the use of several notions of moduli (of convergence, of uniform continuity, of uniform differentiability, etc.). Focusing on membership and equality conditions for sets given by appropriate existential formulas, we define certain families of proof sets that provide a BHK-interpretation of formulas that correspond to the standard atomic formulas of a first-order theory, within Bishop set theory<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000159_inline1.png\"\/><jats:tex-math>$(\\mathrm{BST})$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, our minimal extension of Bishop\u2019s theory of sets. With the machinery of the general theory of families of sets, this BHK-interpretation within BST is extended to complex formulas. Consequently, we can associate to many formulas<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000159_inline2.png\"\/><jats:tex-math>$\\phi$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>of BISH a set<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000159_inline3.png\"\/><jats:tex-math>${\\texttt{Prf}}(\\phi)$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>of \u201cproofs\u201d or witnesses of<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000159_inline4.png\"\/><jats:tex-math>$\\phi$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. Abstracting from several examples of totalities in BISH, we define the notion of a set with a proof-relevant equality, and of a Martin-L\u00f6f set, a special case of the former, the equality of which corresponds to the identity type of a type in intensional Martin-L\u00f6f type theory<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000159_inline5.png\"\/><jats:tex-math>$(\\mathrm{MLTT})$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. Through the concepts and results of BST notions and facts of MLTT and its extensions (either with the axiom of function extensionality or with Vooevodsky\u2019s axiom of univalence) can be translated into BISH. While Bishop\u2019s theory of sets is standardly understood through its translation to MLTT, our development of BST offers a partial translation in the converse direction.<\/jats:p>","DOI":"10.1017\/s0960129522000159","type":"journal-article","created":{"date-parts":[[2022,5,31]],"date-time":"2022-05-31T12:37:16Z","timestamp":1654000636000},"page":"1-43","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":3,"title":["Proof-relevance in Bishop-style constructive mathematics"],"prefix":"10.1017","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4121-7455","authenticated-orcid":false,"given":"Iosif","family":"Petrakis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2022,5,31]]},"reference":[{"volume-title":"Intuitionism and Proof Theory","year":"1970","author":"Kino","key":"S0960129522000159_ref12"},{"key":"S0960129522000159_ref6","volume-title":"Grundlehren der Mathematischen Wissenschaften","volume":"279","author":"Bishop","year":"1985"},{"key":"S0960129522000159_ref15","unstructured":"Palmgren, E. (2005). Bishop\u2019s set theory, Slides from TYPES Summer School 2005, Gothenburg, in http:\/\/staff.math.su.se\/palmgren\/."},{"key":"S0960129522000159_ref18","unstructured":"Palmgren, E. (2013). Bishop-style constructive mathematics in type theory - A tutorial, Slides, in http:\/\/staff.math.su.se\/palmgren\/."},{"key":"S0960129522000159_ref19","unstructured":"Palmgren, E. (2014). Lecture Notes on Type Theory."},{"key":"S0960129522000159_ref27","first-page":"1","article-title":"Constructive uniformities of pseudometrics and Bishop topologies","volume":"11","author":"Petrakis","year":"2019","journal-title":"Journal of Logic and Analysis"},{"key":"S0960129522000159_ref31","unstructured":"Petrakis, I. (to appear). Bases of pseudocompact Bishop spaces. invited chapter in the \u201cHandbook of Constructive Mathematics\u201d, Bridges, D. S., Ishihara, H., Ratjen, M. and Schwichtenbrg, H. (eds.), Cambridge University Press."},{"key":"S0960129522000159_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70740-7"},{"key":"S0960129522000159_ref30","first-page":"1","article-title":"Direct spectra of Bishop spaces and their limits","volume":"17","author":"Petrakis","year":"2021","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129522000159_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-20028-6_31"},{"key":"S0960129522000159_ref33","unstructured":"Petrakis, I. (2019c). Dependent sums and dependent products in Bishop\u2019s set theory. In: Dybjer, P. et al. (eds.) TYPES 2018, LIPIcs, vol. 130, Article No. 3."},{"key":"S0960129522000159_ref36","unstructured":"Petrakis, I. (2022b). Positive negation in constructive mathematics, in preparation."},{"key":"S0960129522000159_ref10","unstructured":"Coquand, T. (2014). A remark on singleton types, manuscript, 2014. Available at http:\/\/www.cse.chalmers.se\/ $\\sim$ coquand\/singl.pdf."},{"key":"S0960129522000159_ref4","unstructured":"Bishop, E. (1968). A General Language, unpublished manuscript, (9)."},{"key":"S0960129522000159_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511565663"},{"key":"S0960129522000159_ref34","unstructured":"Petrakis, I. (2019d). A Yoneda lemma-formulation of the univalence axiom, unpublished manuscript. Available at http:\/\/www.mathematik.uni-muenchen.de\/ $\\sim$ petrakis\/content\/Preprints.php"},{"key":"S0960129522000159_ref1","unstructured":"Aczel, P. and Rathjen, M. (2010). Constructive Set Theory, book draft."},{"key":"S0960129522000159_ref29","doi-asserted-by":"crossref","unstructured":"Petrakis, I. (2020b). Functions of Baire class one over a Bishop topology. In: Anselmo, M. et al. (eds.) Beyond the Horizon of Computability, CiE 2020, LNCS, vol. 12098, 215\u2013227.","DOI":"10.1007\/978-3-030-51466-2_19"},{"key":"S0960129522000159_ref24","doi-asserted-by":"crossref","unstructured":"Petrakis, I. (2016a). The Urysohn extension theorem for bishop spaces. In: Artemov, S. and Nerode, A. (eds.) Symposium on Logical Foundations of Computer Science 2016, LNCS 9537, Springer, 299\u2013316.","DOI":"10.1007\/978-3-319-27683-0_21"},{"key":"S0960129522000159_ref39","doi-asserted-by":"crossref","unstructured":"Richman, F. (1981). Constructive Mathematics, LNM, vol. 873, Springer-Verlag.","DOI":"10.1007\/BFb0090721"},{"key":"S0960129522000159_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0090733"},{"key":"S0960129522000159_ref20","unstructured":"Palmgren, E. (2017). On Equality of Objects in Categories in Constructive Type Theory, TYPES 2017, Abel, A. et al. (eds.), Article No. 7, 7:1\u20137:7."},{"key":"S0960129522000159_ref9","unstructured":"Coquand, T. , Dybjer, P. , Palmgren, E. and Setzer, A. (2005). Type-theoretic Foundations of Constructive Mathematics, book-draft."},{"key":"S0960129522000159_ref13","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198501275.003.0010"},{"key":"S0960129522000159_ref35","unstructured":"Petrakis, I. (2020c). Families of Sets in Bishop Set Theory. Habilitation thesis, LMU. Available at https:\/\/www.mathematik.uni-muenchen.de\/ petrakis\/content\/Theses.php."},{"volume-title":"Foundations of Constructive Analysis","year":"1967","author":"Bishop","key":"S0960129522000159_ref3"},{"key":"S0960129522000159_ref7","article-title":"Constructive Measure Theory","volume":"116","author":"Bishop","year":"1972","journal-title":"Memoirs of the American Mathematical Society"},{"key":"S0960129522000159_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-011-0252-9"},{"key":"S0960129522000159_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71625-2"},{"key":"S0960129522000159_ref21","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(3:25)2014"},{"key":"S0960129522000159_ref28","unstructured":"Petrakis, I. (2020a). Embeddings of Bishop spaces. Journal of Logic and Computation exaa015, https:\/\/doi. org\/10.1093\/logcom\/exaa015."},{"key":"S0960129522000159_ref37","doi-asserted-by":"crossref","unstructured":"Petrakis, I. and Wessel, D. (to appear). Algebras of complemented subsets. In: CiE 2022.","DOI":"10.1007\/978-3-031-08740-0_21"},{"key":"S0960129522000159_ref26","doi-asserted-by":"crossref","unstructured":"Petrakis, I. (2019a). Borel and Baire sets in Bishop Spaces. In: Manea, F. et al. (eds.) Computing with Foresight and Industry, CiE 2019, LNCS, vol. 11558, Springer, 240\u2013252.","DOI":"10.1007\/978-3-030-22996-2_21"},{"key":"S0960129522000159_ref40","doi-asserted-by":"crossref","unstructured":"Richman, F. (2001). Constructive mathematics without choice. In: Reuniting the Antipodes Constructive and Nonstandard Views of the Continuum, Proceedings of 1999 Venice Symposium, Kluwer, Dordrecht, 199\u2013205.","DOI":"10.1007\/978-94-015-9757-9_17"},{"key":"S0960129522000159_ref42","doi-asserted-by":"crossref","unstructured":"Schuster, P. , Berger, U. and Osswald, H. (eds.) (2001). Reuniting the antipodes constructive and nonstandard views of the continuum. In: Proceedings of 1999 Venice Symposium, Kluwer, Dordrecht.","DOI":"10.1007\/978-94-015-9757-9"},{"key":"S0960129522000159_ref43","doi-asserted-by":"publisher","DOI":"10.1093\/philmat\/12.2.106"},{"key":"S0960129522000159_ref38","unstructured":"Petrakis, I. and Zeuner, M. (2022). Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory, submitted."},{"key":"S0960129522000159_ref32","doi-asserted-by":"crossref","unstructured":"Petrakis, I. (2022a). Closed subsets in Bishop topological groups, submitted.","DOI":"10.1016\/j.tcs.2022.09.004"},{"key":"S0960129522000159_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8640-5"},{"key":"S0960129522000159_ref47","unstructured":"Zeuner, M. (2019). Families of Sets in Constructive Measure Theory. Master\u2019s thesis, LMU."},{"key":"S0960129522000159_ref22","unstructured":"Petrakis, I. (2015a). Constructive Topology of Bishop Spaces. Phd thesis, Ludwig-Maximilians-Universit\u00e4t, M\u00fcnchen."},{"key":"S0960129522000159_ref41","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198501275.001.0001"},{"volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","year":"2013","key":"S0960129522000159_ref46"},{"volume-title":"Perspectives in Logic","year":"2012","author":"Schwichtenberg","key":"S0960129522000159_ref44"},{"key":"S0960129522000159_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2012.01.011"},{"key":"S0960129522000159_ref25","doi-asserted-by":"crossref","unstructured":"Petrakis, I. (2016b). A constructive function-theoretic approach to topological compactness. In: Proceedings of the 31st Annual ACM-IEEEE Symposium on Logic in Computer Science (LICS 2016), July 5\u20138, 2016, NYC, USA, 605\u2013614.","DOI":"10.1145\/2933575.2933582"},{"key":"S0960129522000159_ref45","unstructured":"Streicher, T. (2018). Realizability, Lecture Notes, TU Darmstadt."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129522000159","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,6]],"date-time":"2023-02-06T20:40:00Z","timestamp":1675716000000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129522000159\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1]]},"references-count":47,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,1]]}},"alternative-id":["S0960129522000159"],"URL":"https:\/\/doi.org\/10.1017\/s0960129522000159","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2022,1]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}