{"entities":{"Q6156642":{"pageid":13291191,"ns":120,"title":"Item:Q6156642","lastrevid":57126711,"modified":"2026-03-26T17:24:54Z","type":"item","id":"Q6156642","labels":{"en":{"language":"en","value":"Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7695716"}},"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":"Q6156642$6E4D96E2-8824-4320-8850-51B03672DDBA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0584bb0733caa5dd7e697dac635c43af1bb4ac3f","datavalue":{"value":{"text":"Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6156642$B265F4BE-AE55-444A-9BFF-1976DB804143","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2727ea0c536c8b8965c6e43987197ce28213d80a","datavalue":{"value":{"entity-type":"item","numeric-id":1687748,"id":"Q1687748"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$A3FADF88-4AB8-4D77-AB0A-1E0A603BD60A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7c67d5aa4a8a3849e4b03581dc7f5d817732be99","datavalue":{"value":{"entity-type":"item","numeric-id":6099612,"id":"Q6099612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$BF375AE8-0618-4193-ADC1-82049D34B0DE","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$62DD1A12-B0C3-4B7B-A5B0-F58277B581B7","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e078913baaf6e58e465be4601d94b7e1928c7c65","datavalue":{"value":{"time":"+2023-06-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6156642$2C24BB8D-3140-4609-B000-A77B44F8F7B5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156642$BED7E98B-90C7-42A8-BDC4-E73A92051D4C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f3712534cee29c7da452cda38eb0bb843e826f5e","datavalue":{"value":"7695716","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156642$71AEB1E3-DCBC-436B-8C8C-AFB891161EAB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a813fd0e4aef1fda5e8e7d4b77b02104337d96e6","datavalue":{"value":"undecidability","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156642$DAE3BAC1-257A-42B5-8F41-4DEACC95B91B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ede99d15840ea539cd09dd524f7bcf2a6351a209","datavalue":{"value":"synthetic computability","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156642$FDEEE6AF-D9B2-4BC6-8DC4-79E296AC6FFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e2e80a7123e4ea6d0418cb24d37b1837f13e3514","datavalue":{"value":"first-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156642$58C42D03-A13D-4DBB-9910-55CAAF25FCF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7861d405a9971345694c1f3f0657d2fb86fbb667","datavalue":{"value":"incompleteness","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156642$BB8C0E30-C44A-48C6-8441-277C80744D5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7090cb2b2cefa03cee6b50a67ca057c086ad0f00","datavalue":{"value":"Peano arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156642$EAFFE5C2-5E3E-436E-AE82-B7CCFD18F58D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"629db6856d0dc33e7f80e1fce45b626c027d7b52","datavalue":{"value":"ZF set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156642$280C311B-7A71-4401-ACAA-31BDF40FF76D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d6c658f92cfca10399e0b9df9aa408c3bc22cae6","datavalue":{"value":"constructive type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156642$761C386C-048F-484D-A7F1-F378AE8721C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q6156642$8D9F5148-3CAD-428A-A400-01CE3F3475AB","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":"Q6156642$F5F7EB09-58AD-4DD4-AF78-A9AEF6399466","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"67e43cd194146fff0fb8e4b0aacca2f4f32e42e3","datavalue":{"value":{"entity-type":"item","numeric-id":3937387,"id":"Q3937387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$766CEA88-E3EC-478B-8017-67C054D92D79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2edbd4db20ecbcbb1c315d5320a38ebf3acfa299","datavalue":{"value":{"entity-type":"item","numeric-id":3992552,"id":"Q3992552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$5F0F65BF-31CE-4807-AC5D-231226E6D5EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"739330a58a3c3aae77075c5fb847ca13d50160d0","datavalue":{"value":{"entity-type":"item","numeric-id":3075242,"id":"Q3075242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$DC62048A-D315-40DB-A718-3DB653826A95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0fb38957e731e5275c5deddcd104913f80c935fd","datavalue":{"value":{"entity-type":"item","numeric-id":2852343,"id":"Q2852343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$EF5E27D0-D98A-4C45-9E20-AA518795533A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"decc60dfbdecb52e4624e62a3849ec2745afa0d5","datavalue":{"value":{"entity-type":"item","numeric-id":5747648,"id":"Q5747648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$8C65B05D-ECC5-4F36-B50D-7468FF0AE465","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"821e3dd05d0443a56f3b6ab108f431e592ffad4d","datavalue":{"value":{"entity-type":"item","numeric-id":1373302,"id":"Q1373302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$263F30BD-9C6B-432B-BF6C-E39475E805FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5369245c683380663d43367502a396b591af1be3","datavalue":{"value":{"entity-type":"item","numeric-id":5763293,"id":"Q5763293"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$44F1492D-F959-40B1-93D7-1C25F099E361","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70d5dcacdf82491509f047ffa7adf630e71ade90","datavalue":{"value":{"entity-type":"item","numeric-id":5667469,"id":"Q5667469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$89DF56E1-9B31-4B1B-9B85-B46D2DA47BA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"843e3290ea281afff49033aac2cf70e2a4d8546f","datavalue":{"value":{"entity-type":"item","numeric-id":3791109,"id":"Q3791109"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$FD824FFD-D624-48C8-9F0F-04BA567D8883","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"44741cdb786a6bf061a764c2d5d278518b6bcecf","datavalue":{"value":{"entity-type":"item","numeric-id":1791165,"id":"Q1791165"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$FACF4A65-7E91-4367-B010-D2FC92727269","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"659834f1596059b45ef2192e187dd9ba3dcf6dd0","datavalue":{"value":{"entity-type":"item","numeric-id":5875425,"id":"Q5875425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$57362076-88F9-4D2D-8EB1-C8BE90EF11C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"53a419cc1148ddf55be6b5ee1a7219992f7c9285","datavalue":{"value":{"entity-type":"item","numeric-id":5028312,"id":"Q5028312"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$BD88FB85-7253-4DC7-924C-0F8DACA3DA43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"20078d69304e2df97ca3f40332c8d92086a6b541","datavalue":{"value":{"entity-type":"item","numeric-id":4179016,"id":"Q4179016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$0928AF48-CE16-4CBF-B5A7-0F72F85C2370","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0dd25b59545bf053240d7666399c86ee581fbbcd","datavalue":{"value":{"entity-type":"item","numeric-id":1049686,"id":"Q1049686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$E2290FFD-3CD3-430C-A3E7-4BAEE8EAE708","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42d1a22bab52e3efafefc530de3433317743df68","datavalue":{"value":{"entity-type":"item","numeric-id":5048993,"id":"Q5048993"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$48CFCE3E-5001-4735-A98F-18109A4335EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"82da2224f14e03ddf985d14a87269f3e0107f66c","datavalue":{"value":{"entity-type":"item","numeric-id":5597507,"id":"Q5597507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$3B788000-180D-4FDD-B16C-469059AF316D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7b3a2c82a66b9447278ab0b37c5a6dcff305b827","datavalue":{"value":{"entity-type":"item","numeric-id":5089029,"id":"Q5089029"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$478E86AB-4903-4C8B-9FF1-6CEC4FE183E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b485181b6485fecf4313a7a59389b80e233a0ad4","datavalue":{"value":{"entity-type":"item","numeric-id":2945640,"id":"Q2945640"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$00D4E0E6-3F2D-4D4A-85F6-FCD293525374","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3e13325bae56272b4ba305483ee09cc3ad5047e8","datavalue":{"value":{"entity-type":"item","numeric-id":3214891,"id":"Q3214891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$704C7EA2-1319-43FA-B8A7-C4E4D54C1D5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc4ddddb5840ee99760e1c2afc56ab700e598c2d","datavalue":{"value":{"entity-type":"item","numeric-id":5477659,"id":"Q5477659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$4D53FBF7-47B1-479B-9910-42D61F100901","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aab84f6aaf590fa756248847abc358b761eb7958","datavalue":{"value":{"entity-type":"item","numeric-id":286772,"id":"Q286772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$1AC27A4D-1B84-4EFC-8174-C2A21BFAC146","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6d5d760852b694b74735eed422ff0987947ff940","datavalue":{"value":{"entity-type":"item","numeric-id":2305432,"id":"Q2305432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$A6E7C43F-34D0-49E3-AD99-4BB60AE8CC5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d938e2cf16a516c25169e92ed68817a27d01f44d","datavalue":{"value":{"entity-type":"item","numeric-id":5845382,"id":"Q5845382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$895DDC86-2010-4DAA-AA8B-73E418026A5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b492d3887dfe91f103ef3e57c2ed830a645ba0a7","datavalue":{"value":{"entity-type":"item","numeric-id":3980089,"id":"Q3980089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$E746DF57-1E22-438E-A477-EAC65BAB9E9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c10090462c85cbbe7d5d33edaaeddcc1bdf0b3aa","datavalue":{"value":{"entity-type":"item","numeric-id":1110495,"id":"Q1110495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$7EE8B45A-E64E-4CD7-B39F-2D115183CB06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a83f0bb883ffac343e6299387c4e2613e1c540f","datavalue":{"value":{"entity-type":"item","numeric-id":3043140,"id":"Q3043140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$1E3B5543-3542-4324-8C34-85B1CF3CD63F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f5c224a3ccb2b12fb80f7fe1e482e6147509f051","datavalue":{"value":{"entity-type":"item","numeric-id":3654817,"id":"Q3654817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$E01A4AC4-AEDF-4981-851F-595F8BCB59A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3dd9957084ef43a62c06703b0d19c71b6dbb0524","datavalue":{"value":{"entity-type":"item","numeric-id":2829273,"id":"Q2829273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$D3FA9DA9-8EEE-49AD-AFB9-482E5E83AC11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c103bf2cb62768c300adccc9356dc2154001a007","datavalue":{"value":{"entity-type":"item","numeric-id":2209542,"id":"Q2209542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$A7D860E2-30C1-4C5D-B067-22C49EBD0C66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27c43b7e3610435da5759ec0170acf5a3e0de1df","datavalue":{"value":{"entity-type":"item","numeric-id":5797034,"id":"Q5797034"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$3F65948D-9CDE-4B89-A051-C41D410C5888","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"497b4c81f4eb1172c293c9383a73640c83e593d4","datavalue":{"value":{"entity-type":"item","numeric-id":4364399,"id":"Q4364399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$4B20F4B7-879B-4A0C-807B-96420528AEF7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"673349c894564e1ca88d9377614f88609a236969","datavalue":{"value":"10.1007/S10817-022-09647-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6156642$243FC43B-C6BC-445A-A362-5DDC4DD5BAD0","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6156642$4F4FE586-19FF-4CD6-A389-E2ACD6832322","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6156642","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6156642"}}}}}