{"entities":{"Q7361320":{"pageid":31519499,"ns":120,"title":"Item:Q7361320","lastrevid":105364916,"modified":"2026-10-07T13:35:31Z","type":"item","id":"Q7361320","labels":{"en":{"language":"en","value":"Metatheory of Q0"}},"descriptions":{"en":{"language":"en","value":"AFP entry Q0_Metatheory"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b429d7cce169f8d829053bbbd5aa8bcf7c9c8717","datavalue":{"value":"https://isa-afp.org/entries/Q0_Metatheory.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361320$2733CF6C-2819-4BB0-9926-8553E8A11580","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ccf1f48ca40d51ac614ece0aaf2795c63e546686","datavalue":{"value":{"time":"+2023-11-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361320$CC72E2DD-C607-44A7-BAD3-E156902AA890","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"85f2c26a9869ad8fc1011885f090f0c55ab8d3a3","datavalue":{"value":"Javier D\u00edaz","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361320$A6CFD595-81B6-424E-93F8-BFB0B094E323","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3d000f80b51d418e74033046adf23eaa7b76ff0c","datavalue":{"value":{"text":"Metatheory of Q0","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361320$59B89A9B-6864-4839-8A51-BADD8D94A1FA","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"bea49db5ae8d9b8412ec3272f15923e9bd54ef95","datavalue":{"value":"This entry is a formalization of the metatheory of \\(\\mathcal{Q}_0\\) in Isabelle/HOL. \\(\\mathcal{Q}_0\\) is a classical higher-order logic equivalent to Church's Simple Theory of Types. In this entry we formalize Chapter 5 of \"An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof\" (Andrews, 2002), up to and including the proofs of soundness and consistency of \\(\\mathcal{Q}_0\\). These proof are, to the best of our knowledge, the first to be formalized in a proof assistant.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361320$CB18A83F-1162-4681-9323-6DD3DF30578D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5cb9e3a6772849ff9a629cad139288838375d09c","datavalue":{"value":{"entity-type":"item","numeric-id":2395467,"id":"Q2395467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361320$BBBA2432-4954-4AEC-9F85-F1A4518E4741","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b11646dfc2677d6614fa16128dbbd7844776606d","datavalue":{"value":{"entity-type":"item","numeric-id":1847766,"id":"Q1847766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361320$C4306300-4BA8-40D4-BD88-A078EA0100A6","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":"Q7361320$F158E77A-6CD8-41C5-9838-9CBA5D78615C","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"126b93a92266dc6b3b4fa8c76701a0e966604230","datavalue":{"value":{"entity-type":"item","numeric-id":7361366,"id":"Q7361366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361320$55893417-1074-4D0C-A2F4-1ADA96A93437","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"8722426ba1b47fd823a92204d9c28b25a42000cd","datavalue":{"value":{"entity-type":"item","numeric-id":7361533,"id":"Q7361533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361320$47E5F924-E34F-457C-89A2-D5088DBCA900","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"61ce00bd57c38f4b0878e61948aa744910b408d4","datavalue":{"value":{"entity-type":"item","numeric-id":7360807,"id":"Q7360807"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361320$215E5EEE-39A3-480B-9010-99F5E8A79A70","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":"Q7361320$6D6C0EE2-82AA-42A9-91C3-92E7C44DF4D4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Metatheory of Q0","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Metatheory_of_Q0"}}}}}