{"entities":{"Q7361870":{"pageid":31521149,"ns":120,"title":"Item:Q7361870","lastrevid":105369992,"modified":"2026-10-07T13:38:45Z","type":"item","id":"Q7361870","labels":{"en":{"language":"en","value":"Formalization of Forcing in Isabelle/ZF"}},"descriptions":{"en":{"language":"en","value":"AFP entry Forcing"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4f41c23d57e656fc3f3dadb94bdd67739eed1cd8","datavalue":{"value":"https://isa-afp.org/entries/Forcing.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361870$8BD84D7B-45C3-4293-855D-3245E6E975EC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"63b133e2f3cdb47e2584c85d3d40bfb2c7f5272d","datavalue":{"value":{"time":"+2020-05-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361870$DD45FF99-78E0-4564-A45E-443A0FA1A3E2","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"eaaf565f6272bb2d70747c8de188f73fd6ceb28e","datavalue":{"value":"Emmanuel Gunther","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361870$D0D6C55E-5A96-4F83-B087-BC69A167E716","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"4d4c94149d76b14d163b803839378e3d89689dd5","datavalue":{"value":"Miguel Pagano","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361870$1F448824-C884-45DA-A6CD-DC40ABDA790D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"8b79a12243cce5133b63a6dc0b6b79e3b6810f84","datavalue":{"value":"Pedro S\u00e1nchez Terraf","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361870$0E4A4D00-C4BF-4B25-AEF3-442956ED25DF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f680ffa51bc31657066a25aa6ea94af95000e6df","datavalue":{"value":{"text":"Formalization of Forcing in Isabelle/ZF","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361870$2CE122E5-9340-4195-B322-BEFA92EF8FF4","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"078e13e6fa8283a81fc5a2f10c66b0ab4dc827a5","datavalue":{"value":"We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct a proper generic extension and show that the latter also satisfies ZFC.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361870$E95D8FCB-BBA7-4AED-8565-FFD84DA4D014","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5bf133f24682eadb30cba47d623064046c8dc5c","datavalue":{"value":{"entity-type":"item","numeric-id":2333671,"id":"Q2333671"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361870$24E0DBBA-ED0B-464C-A2D8-8ED08005406B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f04632d5958d80f81462441db38ef00e84019e13","datavalue":{"value":{"entity-type":"item","numeric-id":5049004,"id":"Q5049004"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361870$D632EF44-0CFA-4BA9-AD55-CEB0BF03E63F","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":"Q7361870$5F1149FD-6898-48AA-9E52-BA15E6A0A3A7","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361870$C929CE06-755C-4467-93BD-93F86EF40B22","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"aae4e841d888433a47c995aa4de254ab1873976e","datavalue":{"value":{"entity-type":"item","numeric-id":7360819,"id":"Q7360819"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361870$1EBB0C86-A1D5-4D4E-BCA9-BCC60A440688","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361870$BCD0EAC1-56A1-426C-8FF0-F2000EE2C21E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalization of Forcing in Isabelle/ZF (AFP entry Forcing)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formalization_of_Forcing_in_Isabelle/ZF_(AFP_entry_Forcing)"}}}}}