{"entities":{"Q4827615":{"pageid":6857195,"ns":120,"title":"Item:Q4827615","lastrevid":74923620,"modified":"2026-04-15T01:01:39Z","type":"item","id":"Q4827615","labels":{"en":{"language":"en","value":"The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle\u2044zf"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2116754"}},"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":"Q4827615$570ECA4E-4968-4FD4-9C2E-9BB6B7A22351","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fd097a0c1e550f9f582af5fd6c551c5e25d1083e","datavalue":{"value":{"text":"The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle\u2044zf","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4827615$21651D26-3515-497B-976D-A6AC0EC49B3C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"28fc37e66ba32f74163ea31d8587fc8fbccfd03f","datavalue":{"value":"1053.03009","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4827615$EB4C0E37-3413-4752-92D6-3D4186C55B4C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"723cc5e96bcaeeda7b32370d3cdf36fb5abbb658","datavalue":{"value":"10.1112/S1461157000000449","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4827615$EE3EAAA2-73E8-404E-899C-C6F3975316E6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"997f8e81aafe849f90a25017f3ed07a2b1feb16c","datavalue":{"value":{"entity-type":"item","numeric-id":2709391,"id":"Q2709391"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4827615$BD9293CA-F16C-48BB-A2A2-E6A35D0F4B32","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"037fcf95f864ae0e38f5b6894c4f594ea5ca568c","datavalue":{"value":{"time":"+2004-11-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4827615$1ACE178B-3F09-4664-885C-00FF2515BBA9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2f86b736d4e4af1afb250c6f9fa435475731a520","datavalue":{"value":"http://www.lms.ac.uk/jcm/6/lms2003-001/","type":"string"},"datatype":"url"},"type":"statement","id":"Q4827615$83AFD288-7D22-4299-8AF1-FCFFCF41228E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4827615$BBA78E4F-4F3A-44D7-8883-D73995E9EE34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"933c6ba8322680c85da12d59920a0a8822c2db22","datavalue":{"value":"03E35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4827615$A7C1F128-4B85-4E9F-BC6D-0015F0BFD3D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2f1459d5951e049c51abbc0d85c8bd47bc411fa9","datavalue":{"value":"03E25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4827615$9DF56FE8-AF70-4947-9584-A065D5C61C8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4827615$14B18F27-DF2F-4CA7-A2B6-F783C50A6A16","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8961c98427887f81de7a31f2d5178e1d6dc10880","datavalue":{"value":"2116754","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4827615$62F069DC-5B9C-4241-9E53-FDAF51341676","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb555ad50daa2f2442c3374413a67b79e38b5020","datavalue":{"value":"relative consistency","type":"string"},"datatype":"string"},"type":"statement","id":"Q4827615$151069AC-1C5C-424F-BA69-79A42BD575F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0836092e1fe2f2c9bcc68cbbaa259608b2f6de67","datavalue":{"value":"axiom of choice","type":"string"},"datatype":"string"},"type":"statement","id":"Q4827615$C0213AE5-77D6-4AA3-AB44-2BED2BDFA43D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"716c4b637014218c75203d204b1885f1646f0224","datavalue":{"value":"Isabelle/ZF","type":"string"},"datatype":"string"},"type":"statement","id":"Q4827615$CEC9C266-EA11-496C-965D-5A2FA30C2F8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4ed3d4d4d9a22bdf4e6fd0873d2198e6c20a0bac","datavalue":{"value":"mechanization","type":"string"},"datatype":"string"},"type":"statement","id":"Q4827615$279D6C86-89DB-4D7D-8B42-6DF5AB8A3BFA","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"e158afc6b13b401c5e68b0a05779fd4d160cd977","datavalue":{"value":"Q114008993","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4827615$4F5B4C0D-CE60-47F6-85EA-CCD1A47560E4","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":"Q4827615$D7593BCD-D1FD-4DFF-8315-727EF832E878","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":"Q4827615$C16C2544-155F-4FA4-ADAC-05C4B7F0A2BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"aca41f313ec935c6c7a90dad170b49859b6fac14","datavalue":{"value":{"entity-type":"item","numeric-id":17120,"id":"Q17120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4827615$D2258EBC-4B04-46C3-BFA3-F338EACF7A33","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":"Q4827615$0601C9D4-42AB-4826-BC50-3C281283CEBD","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e458e86c97f7ccf8f962d3236b3d8fde33bada17","datavalue":{"value":{"entity-type":"item","numeric-id":1613678,"id":"Q1613678"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4827615$6D3767E0-A59F-41D2-A5D0-72ECF2C1AD9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"52b946fb2f63c0dda27fa5ba25a5cecdec9a1c9a","datavalue":{"value":{"entity-type":"item","numeric-id":4229041,"id":"Q4229041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4827615$5404662A-A19C-4F45-82E9-76353CD9D583","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65c8c8ed706a86d97db05d5b778c49fb79be8a30","datavalue":{"value":{"entity-type":"item","numeric-id":1144013,"id":"Q1144013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4827615$570036D5-F9CB-4444-BA78-13E8405F429F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ddd70fb9307baa76a2064c43fce88ffa925876a","datavalue":{"value":{"entity-type":"item","numeric-id":5772630,"id":"Q5772630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4827615$EC39A0FF-3450-4BBA-9236-6A171F141321","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d4dd4faeed82b17a31b15b4f4a630199ca52442","datavalue":{"value":{"entity-type":"item","numeric-id":4692885,"id":"Q4692885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4827615$48B1B14E-1FF3-4B31-93EC-14074E08F59A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df566ef0248fe3e927a10046fdd99e599cbaa541","datavalue":{"value":{"entity-type":"item","numeric-id":5961491,"id":"Q5961491"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4827615$C2779DF6-8854-4A60-8F4C-B3B72215D072","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2097e358c778dbb154854453f32efc62a8e3614c","datavalue":{"value":{"entity-type":"item","numeric-id":1904402,"id":"Q1904402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4827615$A1908137-AAC1-4BA9-B251-ABC04A83722B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4827615$AB78E0F2-5D8D-4B37-A90F-A74F3AE048AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0136d3bc330af377385e6266bfd9e4c2d4c7a96c","datavalue":{"value":{"entity-type":"item","numeric-id":1319386,"id":"Q1319386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4827615$CBCA8CAA-8DA5-4D92-9F60-FB8A11D60E1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1404903fbb3450c69ae4b46e148487834232fe43","datavalue":{"value":{"entity-type":"item","numeric-id":1823013,"id":"Q1823013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4827615$F63F3CF3-DC5A-48B5-BCA2-7F33F1B67310","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ad81f402aa8faa0a03f0359bfe0281627918b2e2","datavalue":{"value":"W2017971007","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4827615$5B2ED02D-73A4-4CAB-B574-C90A892E1330","rank":"normal"}],"P1643":[{"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":"ce0ada207894afce8ea281a161d43b9000462e1c","datavalue":{"value":{"amount":"+0.8793987035751343","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":"Q4827615$9D14FA32-F5A7-4456-B7B9-CC6A261EB05A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f6946cd334a576097a16d5346c4ccb4db32e8d67","datavalue":{"value":{"entity-type":"item","numeric-id":5961491,"id":"Q5961491"},"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":"Q4827615$682BE570-3110-4D4F-B328-A7B8DACF5AD0","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":"fadf09c3d15d5f403cb909f10f7331a90b125a6a","datavalue":{"value":{"amount":"+0.7455518245697021","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":"Q4827615$C8556257-B32C-43EE-92E0-49A3D7AB19FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a0ea3a15d6367636d22543fb15a9c56e3bc93a57","datavalue":{"value":{"entity-type":"item","numeric-id":2333671,"id":"Q2333671"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a6f2884ef031a565342dff56c1f2aa2221eff777","datavalue":{"value":{"amount":"+0.7414522767066956","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":"Q4827615$76B4D746-29A0-4A55-8386-5FD87931A8F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d4d8bd861fad72b8d2a4ae0cc98add32adbe3f3","datavalue":{"value":{"entity-type":"item","numeric-id":1312157,"id":"Q1312157"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0c53f41d3edcaf6e5af94485e4e526af4c265013","datavalue":{"value":{"amount":"+0.7265117764472961","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":"Q4827615$5105E1C8-87A7-49B8-8D00-C662B0803FFD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle\u2044zf","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_Relative_Consistency_of_the_Axiom_of_Choice_Mechanized_Using_Isabelle%E2%81%84zf"}}}}}