{"entities":{"Q7361073":{"pageid":31518758,"ns":120,"title":"Item:Q7361073","lastrevid":105362582,"modified":"2026-10-07T13:34:22Z","type":"item","id":"Q7361073","labels":{"en":{"language":"en","value":"Compactness Theorem for First-Order Logic"}},"descriptions":{"en":{"language":"en","value":"AFP entry FOL_Compactness"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"324e37cad49253a593949471045b0ac6b8728fdf","datavalue":{"value":"https://isa-afp.org/entries/FOL_Compactness.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361073$CBCD948A-2132-4B3A-A82B-2E6635D5388B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"862fba593555eff8cb7020791426db46cbd244d9","datavalue":{"value":{"time":"+2025-02-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361073$6D12F32D-06FF-49D7-9904-C4B44346931A","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"8166375b6e885d78d9cc04a5e84d03f5f37dead4","datavalue":{"value":"Sophie Tourret","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361073$85C0AB67-B740-45C8-9DE5-3D13F5FE9FDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"7479166f83b44c07c9a493479bd3c0ed2c72ef23","datavalue":{"value":"Lawrence C. Paulson","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361073$FC89DA04-46C8-4664-A049-473B58D4C516","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d53e3c14eefe3804049ca0a0ead1e3b51562d5aa","datavalue":{"value":{"text":"Compactness Theorem for First-Order Logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361073$23992131-6D87-461D-8449-DBC845E69251","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b7c76da5eda12ce009696940b5a153ea4977d2bc","datavalue":{"value":"This is a translation of a HOL Light formalization covering foundational results in first-order model theory, including the compactness of first-order logic. The original work is described in the following paper : Formalizing Basic First Order Model Theory John Harrison Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'98, Springer LNCS 1497, pp. 153-170. The corresponding HOL Light theories can be found on GitHub .","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361073$465B606F-1769-4E2F-AC19-B8D8FECBCA17","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"205fc50b5519f69b83835852ede0d50684c7d19b","datavalue":{"value":{"entity-type":"item","numeric-id":4247076,"id":"Q4247076"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361073$95E39935-64A0-402A-BEBE-B79384810B54","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":"Q7361073$24724C29-538A-4D1B-A0A3-207BC4F46BF9","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"6d228da4bce2fba997fec5a975b2ba853633b29e","datavalue":{"value":{"entity-type":"item","numeric-id":7361840,"id":"Q7361840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361073$E750665D-80B8-464D-AD3D-32B35BB1A256","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"6603b2a587424388be085eadb1b94d7144f1c3de","datavalue":{"value":{"entity-type":"item","numeric-id":7361652,"id":"Q7361652"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361073$97B7E93F-D03A-46B1-9450-6DB6E6308030","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"04648103e40c59982614f3813f352c9cf3f67ce8","datavalue":{"value":{"entity-type":"item","numeric-id":7360808,"id":"Q7360808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361073$A53B6B6A-DB22-45A3-8616-2C8618791D34","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":"Q7361073$AC8E03C2-EB55-4081-B5D0-BCBB344A7525","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Compactness Theorem for First-Order Logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Compactness_Theorem_for_First-Order_Logic"}}}}}