{"entities":{"Q40276":{"pageid":40332,"ns":120,"title":"Item:Q40276","lastrevid":105428003,"modified":"2026-10-09T10:08:52Z","type":"item","id":"Q40276","labels":{"en":{"language":"en","value":"Completeness theorem"}},"descriptions":{"en":{"language":"en","value":"AFP entry Completeness"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"7cdcd689a4f94a9769add597ea7b6f478a532856","datavalue":{"value":"28562","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40276$42303AD9-599A-499F-A993-A9D3B867985A","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":"Q40276$D23687F6-2114-4F96-9D0D-0EFBBAA4F74C","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"01fe5436d4b9d6df5aac9a43424345a6906fb19c","datavalue":{"value":"https://www.isa-afp.org/entries/Completeness.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40276$65B3FDD2-55C4-4F1D-A981-4DB1E935A3D1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40276$AB5E6F28-5AFB-4669-A018-358685852897","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40276$C594F6C9-7C31-40A5-B4B0-5DDF47C50746","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40276$9F34C1EC-23D9-41CE-9C7C-859A77695873","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40276$2C70A28B-B9CB-41FC-AD9A-8C97453BAD61","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40276$2056E821-A948-4B21-84CD-B60D85BB55AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40276$740A0413-4F3B-40AC-B1AF-9B6D9C4C62D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a0a329d132b963c571723538ca5cd1b467b324fe","datavalue":{"value":{"entity-type":"item","numeric-id":40325,"id":"Q40325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40276$42385DAB-A58D-4606-A655-5F4F3FF31586","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8bf2731143fd82a1f95f40f13b2fce56fbb7345a","datavalue":{"value":{"entity-type":"item","numeric-id":40299,"id":"Q40299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40276$F9F6145F-3C53-43B3-B093-377BADE1FAA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40276$46AB618E-E685-42E2-96EC-407B94EE5944","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8533330b9fa0c1f7979d4af1d0e8bdba3ffc811c","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40276$9633AC8A-31F4-4D73-B116-CEB2BCE2E333","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"485b63894219b8c81472ad502491b9d2d5703cae","datavalue":{"value":{"entity-type":"item","numeric-id":31023,"id":"Q31023"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40276$89245E78-A416-4E65-8E07-D9DA1A74E3C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"331995fe532c23e24d72d01a1bd6245fafcd9671","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40276$AC8A08E6-F880-4E29-ACA6-1943D46FB04C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40276$F3277F4C-E975-4207-B04C-1C614FFA1FC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7ef1082544496cdbd626aabd0ffce07a1cf4d46a","datavalue":{"value":{"entity-type":"item","numeric-id":40285,"id":"Q40285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40276$DDB03DA0-6AA0-475E-99FE-BCC65F99B107","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8dde418bf28e22fefe1976bd953eb7c8ec5b548d","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40276$285C95BA-2F5B-44E5-89C0-C34D931D2AB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"28fc316ccc1f38bd6830fcffe3187b6d32168084","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40276$11A65101-D2F9-41B2-83E5-9F6EBA517C84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"493c5144a9d14f0b980d45769fb4b197b51b453c","datavalue":{"value":{"entity-type":"item","numeric-id":40555,"id":"Q40555"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40276$4E0BFE80-AA93-491A-ABEA-FA6E9C17396E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"0204f081facf570c6ab1a272475183b48ae5e4f2","datavalue":{"value":{"entity-type":"item","numeric-id":40286,"id":"Q40286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40276$0CC47CA7-A818-4D8B-8CBF-66E6C5BBCD45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b3df43f02eb541c419b766c9dd663037c99c0a0e","datavalue":{"value":{"entity-type":"item","numeric-id":40545,"id":"Q40545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40276$C8EB4BA1-89A8-4582-9E85-ED17539D52D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ed15eb8701a335444fde1bcc3327d1067ce64751","datavalue":{"value":{"entity-type":"item","numeric-id":24376,"id":"Q24376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40276$D439E333-EA93-49B4-93AF-E8774441E0B2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5742e2dc72ec7ac19ad036ee6b585c18a7be8152","datavalue":{"value":"https://isa-afp.org/entries/Completeness.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40276$645BEF1F-E100-4EC6-ABE1-3B693A5E7C48","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"75f34c5b91bd61dc3e319c8f12dc24bfe0527ead","datavalue":{"value":"James Margetson","type":"string"},"datatype":"string"},"type":"statement","id":"Q40276$59B978F0-ACD8-452C-840D-552E4B288033","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"cdcc065143ef05b577fcf1932e0ad33c387a57fd","datavalue":{"value":"Tom Ridge","type":"string"},"datatype":"string"},"type":"statement","id":"Q40276$66E42133-5D12-4BBB-BB51-1DFD3751BD75","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"5e1a918253620c2df3b4b0b3acc214302ff98d95","datavalue":{"value":"The completeness of first-order logic is proved, following the first five pages of Wainer and Wallen's chapter of the book Proof Theory by Aczel et al., CUP, 1992. Their presentation of formulas allows the proofs to use symmetry arguments. Margetson formalized this theorem by early 2000. The Isar conversion is thanks to Tom Ridge. A paper describing the formalization is available [pdf] .","type":"string"},"datatype":"string"},"type":"statement","id":"Q40276$E10FC55A-59B3-440B-98D7-F27305D1AA0B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"88ae69fb442504d60096a5bf02c2a2797fbe9f64","datavalue":{"value":{"time":"+2004-09-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40276$2A4EF586-AA46-4AAF-8167-0332B92DDEE9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b5454eada34f07c517908152c87c5a19bd0e8cc8","datavalue":{"value":{"text":"Completeness theorem","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40276$B11606A8-BA9D-41BB-9A4E-06C7A18478FF","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":"Q40276$E8BBA53C-53BB-4694-8523-C2F560AB90BA","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"0010e22d998484f218097f7f79d7fc22bc7427c6","datavalue":{"value":{"entity-type":"item","numeric-id":7360817,"id":"Q7360817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40276$2BEEEACD-CE47-4D47-9344-30D0381EDA18","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Completeness theorem","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Completeness_theorem"}}}}}