{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T23:04:52Z","timestamp":1776553492021,"version":"3.51.2"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030232498","type":"print"},{"value":"9783030232504","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-23250-4_4","type":"book-chapter","created":{"date-parts":[[2019,7,2]],"date-time":"2019-07-02T03:01:17Z","timestamp":1562036477000},"page":"44-60","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["A Tale of Two Set Theories"],"prefix":"10.1007","author":[{"given":"Chad E.","family":"Brown","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7099-1669","authenticated-orcid":false,"given":"Karol","family":"P\u0105k","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,7,3]]},"reference":[{"issue":"3","key":"4_CR1","first-page":"563","volume":"1","author":"G Bancerek","year":"1990","unstructured":"Bancerek, G.: Tarski\u2019s classes and ranks. Formalized Math. 1(3), 563\u2013567 (1990)","journal-title":"Formalized Math."},{"issue":"2","key":"4_CR2","first-page":"265","volume":"1","author":"G Bancerek","year":"1990","unstructured":"Bancerek, G.: Zermelo theorem and axiom of choice. Formalized Math. 1(2), 265\u2013267 (1990)","journal-title":"Formalized Math."},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-319-20615-8_17","volume-title":"Intelligent Computer Mathematics","author":"G Bancerek","year":"2015","unstructured":"Bancerek, G., et al.: Mizar: state-of-the-art and beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 261\u2013279. Springer, Cham (2015). \n                    https:\/\/doi.org\/10.1007\/978-3-319-20615-8_17"},{"issue":"1\u20134","key":"4_CR4","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s10817-017-9440-6","volume":"61","author":"G Bancerek","year":"2018","unstructured":"Bancerek, G., et al.: The role of the Mizar Mathematical Library for interactive proof development in Mizar. J. Autom. Reason. 61(1\u20134), 9\u201332 (2018). \n                    https:\/\/doi.org\/10.1007\/s10817-017-9440-6","journal-title":"J. Autom. Reason."},{"key":"4_CR5","doi-asserted-by":"publisher","first-page":"2351","DOI":"10.1098\/rsta.2005.1650","volume":"363","author":"H Barendregt","year":"2005","unstructured":"Barendregt, H., Wiedijk, F.: The challenge of computer mathematics. R. Soc. Lond. Trans. Ser. A 363, 2351\u20132375 (2005)","journal-title":"R. Soc. Lond. Trans. Ser. A"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-540-71067-7_3","volume-title":"Theorem Proving in Higher Order Logics","author":"Y Bertot","year":"2008","unstructured":"Bertot, Y.: A short presentation of Coq. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 12\u201316. Springer, Heidelberg (2008). \n                    https:\/\/doi.org\/10.1007\/978-3-540-71067-7_3"},{"key":"4_CR7","unstructured":"Brown, C.E.: The Egal manual, September 2014"},{"issue":"3","key":"4_CR8","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/s10817-015-9340-6","volume":"55","author":"CE Brown","year":"2015","unstructured":"Brown, C.E.: Reconsidering pairs and functions as sets. J. Autom. Reason. 55(3), 199\u2013210 (2015). \n                    https:\/\/doi.org\/10.1007\/s10817-015-9340-6","journal-title":"J. Autom. Reason."},{"key":"4_CR9","unstructured":"Brown, C.E., P\u0105k, K.: A tale of two set theories (2019). \n                    http:\/\/alioth.uwb.edu.pl\/~pakkarol\/publications.html"},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5, 56\u201368 (1940)","journal-title":"J. Symb. Log."},{"key":"4_CR11","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1090\/S0002-9939-1975-0373893-X","volume":"51","author":"R Diaconescu","year":"1975","unstructured":"Diaconescu, R.: Axiom of choice and complementation. Proc. Am. Math. Soc. 51, 176\u2013178 (1975)","journal-title":"Proc. Am. Math. Soc."},{"issue":"1","key":"4_CR12","doi-asserted-by":"publisher","first-page":"43","DOI":"10.4064\/fm-71-1-43-62","volume":"71","author":"U Felgner","year":"1971","unstructured":"Felgner, U.: Comparison of the axioms of local and universal choice. Fundamenta Mathematicae 71(1), 43\u201362 (1971)","journal-title":"Fundamenta Mathematicae"},{"key":"4_CR13","unstructured":"Fraenkel, A.A., Bar-Hillel, Y., L\u00e9vy, A.: Foundations of Set Theory. North-Holland Pub. Co. (1973)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BFb0105405","volume-title":"Theorem Proving in Higher Order Logics","author":"M Gordon","year":"1996","unstructured":"Gordon, M.: Set theory, higher order logic or both? In: Goos, G., Hartmanis, J., van Leeuwen, J., von Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 191\u2013201. Springer, Heidelberg (1996). \n                    https:\/\/doi.org\/10.1007\/BFb0105405"},{"issue":"2","key":"4_CR15","first-page":"153","volume":"3","author":"A Grabowski","year":"2010","unstructured":"Grabowski, A., Korni\u0142owicz, A., Naumowicz, A.: Mizar in a Nutshell. J. Formalized Reason. 3(2), 153\u2013245 (2010)","journal-title":"J. Formalized Reason."},{"issue":"3","key":"4_CR16","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10817-015-9345-1","volume":"55","author":"A Grabowski","year":"2015","unstructured":"Grabowski, A., Korni\u0142owicz, A., Naumowicz, A.: Four decades of Mizar. J. Autom. Reason. 55(3), 191\u2013198 (2015). \n                    https:\/\/doi.org\/10.1007\/s10817-015-9345-1","journal-title":"J. Autom. Reason."},{"key":"4_CR17","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0081551","volume-title":"Th\u00e9orie des Topos et Cohomologie Etale des Sch\u00e9mas","author":"A Grothendieck","year":"1972","unstructured":"Grothendieck, A., Verdier, J.L.: Th\u00e9orie des Topos et Cohomologie Etale des Sch\u00e9mas. LNM, vol. 269, 1st edn. Springer, Heidelberg (1972). \n                    https:\/\/doi.org\/10.1007\/BFb0081551","edition":"1"},{"key":"4_CR18","unstructured":"Ja\u015bkowski, S.: On the rules of suppositions. Studia Logica 1, 32 p. (1934)"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-319-62075-6_14","volume-title":"Intelligent Computer Mathematics","author":"C Kaliszyk","year":"2017","unstructured":"Kaliszyk, C., P\u0105k, K.: Presentation and manipulation of Mizar properties in an Isabelle object logic. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 193\u2013207. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-62075-6_14"},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Kaliszyk, C., P\u0105k, K.: Semantics of Mizar as an Isabelle object logic. J. Autom. Reason. (2018). \n                    https:\/\/doi.org\/10.1007\/s10817-018-9479-z","DOI":"10.1007\/s10817-018-9479-z"},{"key":"4_CR21","doi-asserted-by":"publisher","unstructured":"Kirst, D., Smolka, G.: Categoricity results and large model constructions for second-order ZF in dependent type theory. J. Autom. Reason. (2018). \n                    https:\/\/doi.org\/10.1007\/s10817-018-9480-6\n                    \n                  . Accessed 11 Oct 2018","DOI":"10.1007\/s10817-018-9480-6"},{"issue":"3","key":"4_CR22","first-page":"595","volume":"1","author":"B Nowak","year":"1990","unstructured":"Nowak, B., Bancerek, G.: Universal classes. Formalized Math. 1(3), 595\u2013600 (1990)","journal-title":"Formalized Math."},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/11921240_19","volume-title":"Theoretical Aspects of Computing - ICTAC 2006","author":"S Obua","year":"2006","unstructured":"Obua, S.: Partizan games in Isabelle\/HOLZF. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 272\u2013286. Springer, Heidelberg (2006). \n                    https:\/\/doi.org\/10.1007\/11921240_19"},{"key":"4_CR24","doi-asserted-by":"publisher","first-page":"68","DOI":"10.4064\/fm-30-1-68-89","volume":"30","author":"A Tarski","year":"1938","unstructured":"Tarski, A.: \u00dcber Unerreichbare Kardinalzahlen. Fundamenta Mathematicae 30, 68\u201389 (1938)","journal-title":"Fundamenta Mathematicae"},{"key":"4_CR25","unstructured":"Trybulec, A.: Tarski Grothendieck set theory. J. Formalized Math. Axiomatics (2002). Released 1989"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-23250-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,2]],"date-time":"2019-07-02T03:03:48Z","timestamp":1562036628000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-23250-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030232498","9783030232504"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-23250-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"3 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2019\/cicm.php?event=&menu=general","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}