{"entities":{"Q5961491":{"pageid":8138293,"ns":120,"title":"Item:Q5961491","lastrevid":46469223,"modified":"2025-12-24T20:47:23Z","type":"item","id":"Q5961491","labels":{"en":{"language":"en","value":"Mechanizing set theory. Cardinal arithmetic and the axiom of choice"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 980899"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5961491$C834AC0C-AE6B-4782-8F3A-ADF26129D5DC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c899c11ca57d650e92f3d1be454964af8f87f5d6","datavalue":{"value":{"text":"Mechanizing set theory. Cardinal arithmetic and the axiom of choice","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5961491$CCCD7036-7096-47D0-B82D-E50D8FE8FF55","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1d84adc6aac611eac6c6463e4b54c10dea39150a","datavalue":{"value":"0868.03005","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5961491$A641A6C2-8CE5-4138-8E0B-A44BC6E3BD31","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3eacc8f1e2d6d6d3d4fe3caaa0c4d73c7332566b","datavalue":{"value":"10.1007/BF00283132","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5961491$6D6FFD95-22E0-4257-8A49-F9A02BE4AAE7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb5dfbdfa6d8a2070a67ff948fb8abd387eda36e","datavalue":{"value":{"entity-type":"item","numeric-id":352969,"id":"Q352969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5961491$A623F802-1659-42E5-9EE8-21FC3DE1B3E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1905c170d615eb4821e09def4f75002197234199","datavalue":{"value":{"entity-type":"item","numeric-id":242599,"id":"Q242599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5961491$42972A7F-7DF4-48A3-97F3-D5255F17F778","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5961491$E1F9133C-05E2-4D63-B622-BE7C788B3592","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b34f93578f34bf813eb265da2a0d58fb3d8dd5ea","datavalue":{"value":{"time":"+1997-08-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5961491$2E59FC6E-A695-46F9-8ABB-7A13ABEA6C59","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"c055e7e148d98dbbcb28c110a0ce6739458ec061","datavalue":{"value":"The authors use a proof assistant, the Isabelle Logical Framework, to establish some fairly deep results of Zermelo-Fraenkel set theory. The results, which are formally proven, concern cardinal arithmetic and the axiom of choice. The proofs require results from theories of orders, order-isomorphisms, order types, ordinal arithmetic, cardinals, etc., which covers most of the first chapter of Kunen's set theory book. Overall, the paper is a valuable contribution to the growing corpus of machine checked mathematics.","type":"string"},"datatype":"string"},"type":"statement","id":"Q5961491$922DF3A4-7F6F-49E6-AD3E-6F5A2D0981AC","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"ba8472b3da3fbe356de4dc8ca93e3dfd034c762e","datavalue":{"value":{"entity-type":"item","numeric-id":1332774,"id":"Q1332774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5961491$6CCE5D89-324E-4814-8F89-8DDE7CE7DB64","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5961491$025A2368-A8B2-40B6-AA34-5F2264BB82B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2f1459d5951e049c51abbc0d85c8bd47bc411fa9","datavalue":{"value":"03E25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5961491$A36DEC34-0022-4A78-A08D-D151CCCAA696","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5961491$493155D6-5D0A-4A63-9DC0-43F695B836BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7ae77b7014ae74d050ddd08c7570cbea14e17b7f","datavalue":{"value":"03E10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5961491$5E8676B8-99FA-400D-83C3-E83A6F7B4957","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bc4de30e2c472342a89b604ef1d4e8ae9d0625eb","datavalue":{"value":"980899","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5961491$2D4660BE-70AD-409C-8857-F2EDB6F86575","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6a78675f0dcb3af511ac1d4dfa61901e828bcb8","datavalue":{"value":"proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q5961491$0B67520A-F3BB-4116-B84D-7A717308B196","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d81d74d8354b37ff2fd815e873630a6617608b9a","datavalue":{"value":"Isabelle Logical Framework","type":"string"},"datatype":"string"},"type":"statement","id":"Q5961491$29B6F446-517F-40A6-BCE7-7932F0256462","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c222d2154c724462abd633657d9386ca4ec975ff","datavalue":{"value":"Zermelo-Fraenkel set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5961491$B383C6F3-07D4-43E1-959B-CF60B9BE9FEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e3e6e77720570f8376c2f9838e981d7a822b83e7","datavalue":{"value":"cardinal arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5961491$B557F640-3739-46D9-8072-CCF8957313A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0836092e1fe2f2c9bcc68cbbaa259608b2f6de67","datavalue":{"value":"axiom of choice","type":"string"},"datatype":"string"},"type":"statement","id":"Q5961491$51240155-5CA0-4597-9028-FB4266418EDA","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5961491$EA86FBCA-DF40-4C4E-A001-6AA602F4F0C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5961491$70ACC345-AFAA-4AAD-9F69-9A49E9557CAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b799da0cc0efb29a46dd283874e64386ca0e87dd","datavalue":{"value":{"entity-type":"item","numeric-id":21136,"id":"Q21136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5961491$91755523-2E7E-468B-BD42-D4087104464E","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5961491$62C1F7F0-F75F-4B8E-BBBF-64929C0EFCB1","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"3c49511756acebe1df100b6b6a13bcf27ebd7a93","datavalue":{"value":"Q114018501","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5961491$3CFB47E5-EF27-48A8-A1B3-EB52EE0E2069","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8d9658b61396421bb4c8b1ad3e8d2f7a4797f594","datavalue":{"value":"https://doi.org/10.1007/bf00283132","type":"string"},"datatype":"url"},"type":"statement","id":"Q5961491$DD100691-62C9-46AF-9E15-985A695B38FD","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"137fd0e48ff8a7660cbabeabd100244c3fb8e716","datavalue":{"value":"W2073127449","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5961491$5B969D60-2475-4CE3-B16A-DD85DE880A51","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cbce8cd1cb95caa98f839893cfea5c1f671543e8","datavalue":{"value":{"entity-type":"item","numeric-id":4827615,"id":"Q4827615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"db8913364e6106f73b25bd9280125f11b238cf51","datavalue":{"value":{"amount":"+0.8359882831573486","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5961491$FC80312A-5EE2-4A01-9D6E-E39390931B6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5174dcfa550a4cdf29f68698fbaebfd9edb66bc6","datavalue":{"value":{"entity-type":"item","numeric-id":3507465,"id":"Q3507465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"58df11ed649d78b0aa62e6e20aaf088334822f4b","datavalue":{"value":{"amount":"+0.7964447140693665","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5961491$A7535DF9-F8C3-4D15-BF21-FB6942B6615E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"de72a55ad8714891c24ede823c98f307f17fcba8","datavalue":{"value":{"entity-type":"item","numeric-id":1319386,"id":"Q1319386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"331c3197b20d88af990f82b41d9d9b64466fe65d","datavalue":{"value":{"amount":"+0.7909063696861267","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5961491$2CE07377-7547-45F5-891D-D39AFD9D2A36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e3f607eb892ede6a0a74f65718bef071331d5de7","datavalue":{"value":{"entity-type":"item","numeric-id":5313076,"id":"Q5313076"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cadd3f91a710c0162712d2c0566590f030eb6e58","datavalue":{"value":{"amount":"+0.7810214757919312","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5961491$F5B86B1C-38CB-45B3-AF71-9E18A7138EAF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5961491","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5961491"}}}}}