{"entities":{"Q1123184":{"pageid":1133933,"ns":120,"title":"Item:Q1123184","lastrevid":70116816,"modified":"2026-04-13T12:33:22Z","type":"item","id":"Q1123184","labels":{"en":{"language":"en","value":"Incompleteness of first-order temporal logic with until"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4108728"}},"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":"Q1123184$BD126B65-0D85-4C08-B1F9-36594876CC10","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bf50003e4787c3c3d82bfe572e4df88d46ae7610","datavalue":{"value":{"text":"Incompleteness of first-order temporal logic with until","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1123184$18751366-E359-40F2-B64B-B93066ED8083","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"787f75b05c1702a62de0e63b372fe0db45521f58","datavalue":{"value":"0677.03013","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1123184$97BF68FD-48CF-4CB4-873D-6561044F3D6A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"280fc9593c29342a4fe1c5d60e8a14e9c107c358","datavalue":{"value":"10.1016/0304-3975(88)90045-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1123184$BEB5D0D2-8974-4983-8346-F79C4E730565","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6a0b7caa867576126152d465e12b8f30421d1e09","datavalue":{"value":{"entity-type":"item","numeric-id":1111369,"id":"Q1111369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1123184$1AC1BCD3-DC85-4C64-B3CE-2F3D308010FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ca60e4abfd0c45cace511a7d7434a08b65f8249c","datavalue":{"value":{"entity-type":"item","numeric-id":763332,"id":"Q763332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1123184$E2BCBE42-14DC-4FED-93FC-0DE5C74BE3C9","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1123184$1AFEA3AD-34A6-4EF4-A470-F852E79418BD","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"31a1937240ca4a323604b4728c31d242b5596d7c","datavalue":{"value":{"time":"+1988-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1123184$763EE307-53D1-42C8-8DE2-9319ED78A0B9","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"674aa39e62f543dc6643b004e2f703fd27bd4168","datavalue":{"value":"The version of first-order temporal logic (with equality) chosen in this paper is essentially that introduced by \\textit{Z. Manna} and \\textit{A. Pnueli} [Verification of concurrent programs: the temporal framework, in: The correctness problem in computer science (\\textit{R. S. Boyer} and \\textit{J S. Moore} (eds.)), 215-273 (1981; Zbl 0476.68009)]; it uses the temporal modalities ``always'', ``sometimes'', ``next time'', ``until'' and ``at next''. It is shown that this logic is weakly incomplete (the set of tautologies over an arbitrary signature is not r.e.) and strongly incomplete (the set of tautologies is r.e. for no signature). Although the first claim is a consequence of the second, they are separately presented. The proof of the first theorem is analogous to the proof of incompleteness of second-order prediate logic. It is based on Trakhtenbrot's theorem and the fact that finite structures are characterizable in temporal logic (this result is interesting by its own). For the second theorem, the technique consists in reducing the complement of the halting problem for Turing machines to the problem whether a temporal formula (only with \\(``='')\\) is a tautology.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1123184$9E701AB0-0205-47A0-9F1A-BB4E7894231B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1123184$2F8E6EFD-8FB8-4E5B-B4E3-97E7EC6A2CC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1123184$7C7477FD-A816-4E3E-9DA5-342B6F14C2F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1123184$C9EDE0A0-A7C0-47B4-85E1-F5B08F74AE2F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b554a4f4c3996ace7d42a684c289b020cabe2794","datavalue":{"value":"4108728","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1123184$3854A5EF-8981-4608-9383-6924A0F0FCDE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7861d405a9971345694c1f3f0657d2fb86fbb667","datavalue":{"value":"incompleteness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1123184$97596B8D-2739-44C7-A403-9A1607FB5BF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4a1a1b4de2f6601636779c475343b36943870036","datavalue":{"value":"first-order temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1123184$DDD81C98-1ACD-46BC-B238-DEA34B37E777","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0067e55f13e9ea855671ec6de62f60b0986d7f5c","datavalue":{"value":"temporal modalities","type":"string"},"datatype":"string"},"type":"statement","id":"Q1123184$5371DFC8-2B65-4767-AC17-4ED29ACB44E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c9b38447a3ea959cbe95310edeeb21e7ef6903f8","datavalue":{"value":"halting problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1123184$172A6E89-914B-4E63-BF97-7B3B71B521C2","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"6536f759dee9ce142c834adc5cc137400d919eb8","datavalue":{"value":{"entity-type":"item","numeric-id":1037240,"id":"Q1037240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1123184$40D4AC77-B06F-4994-BEFA-E270F437E6D4","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":"Q1123184$5EBD2489-7CD9-4F7A-BCFB-3064FC007AB2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7b41ed073aa8154ef82f4568e281d9fa0e323670","datavalue":{"value":{"entity-type":"item","numeric-id":3220545,"id":"Q3220545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1123184$0058D981-F18C-4F8C-861B-10A8B9E6F5D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"161c81188dcd2fd1b18f956df590ef058f86413a","datavalue":{"value":{"entity-type":"item","numeric-id":800722,"id":"Q800722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1123184$A28B780F-F8E2-4BA6-BCE8-11C224A25332","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1aaa7c2a801938246bc5b9c35ae533855c08aea3","datavalue":{"value":{"entity-type":"item","numeric-id":1090673,"id":"Q1090673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1123184$6A8A0EE5-42D3-4C82-AB26-CE5D9B2A2A1E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"09978449857762c53fbc3674ed03aacf0e8c2138","datavalue":{"value":"https://doi.org/10.1016/0304-3975(88)90045-x","type":"string"},"datatype":"url"},"type":"statement","id":"Q1123184$F23CCE14-A55B-428C-B38C-324FDD8ECCDB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"091504873673e8a7f677f43d5dd465a5fa4ec7c6","datavalue":{"value":"W2092497338","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1123184$3AF39C4F-5AA2-4D5D-9D28-3BF20D657F50","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"70d74d9c8e0e524ff6a1666b660235e14a06b097","datavalue":{"value":{"entity-type":"item","numeric-id":3735688,"id":"Q3735688"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"00f79027c29e47b458ea5541947ee56117e09896","datavalue":{"value":{"amount":"+0.87104183","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1123184$2F3F3D5D-D649-4FB6-853A-8B0B9ADC7153","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3a6aca9a5039fba5f216bd8e6614355e9eea4c82","datavalue":{"value":{"entity-type":"item","numeric-id":4275689,"id":"Q4275689"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"42d43ae44be859e7d2f7d09026ec39350b7eb2bd","datavalue":{"value":{"amount":"+0.8493797","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1123184$AB263CB3-15E8-408F-B46D-E72A142115AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a63f27caaf271dd92d70879df13c0bf092e7b55","datavalue":{"value":{"entity-type":"item","numeric-id":809066,"id":"Q809066"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9a173495a72f6b95e6063d312b23ade940334501","datavalue":{"value":{"amount":"+0.84838027","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1123184$EA203B72-A9F8-4044-B15F-EF0D636EE6EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"daf6b8f91fb16ea93d824f7d61c49aa5a596c386","datavalue":{"value":{"entity-type":"item","numeric-id":1186428,"id":"Q1186428"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"154cecac0b82c99f19ccdbb89399339ae0f55bf9","datavalue":{"value":{"amount":"+0.84508586","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1123184$F562C641-34F4-4A0E-8BCB-F98D96635C08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"21dd37c41e1b798ce42fe7cd6ee278bf06601416","datavalue":{"value":{"entity-type":"item","numeric-id":3739112,"id":"Q3739112"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4ca78bbc415b6ee008eff532c644fa04467b432e","datavalue":{"value":{"amount":"+0.83038044","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1123184$50285EF4-A304-4CE3-8A9E-87CCF21CFC38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c05aa3dcda7621c0f67f1f397a8e1414dd729e7a","datavalue":{"value":{"entity-type":"item","numeric-id":2757840,"id":"Q2757840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7f18f19d6c11701a9c946a0c6a42cf8e43083e2f","datavalue":{"value":{"amount":"+0.8290525","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1123184$CB6DA9D7-9CB4-4174-860F-623D34BC1DD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8c4749c931588c31648c97654758bf0cdfb3dc96","datavalue":{"value":{"entity-type":"item","numeric-id":1591203,"id":"Q1591203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b1c5693593eba32a57bf101d7d7cbb1f176f8f9c","datavalue":{"value":{"amount":"+0.82788","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1123184$241DF414-5986-4E56-BF68-1041467FED33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d4f69ff61384e34b6f1c9fffb5e2c65fe257f29a","datavalue":{"value":{"entity-type":"item","numeric-id":3789533,"id":"Q3789533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b40c33edc4e1e36a65b6e728d24a253ad3178828","datavalue":{"value":{"amount":"+0.82752955","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1123184$33BEC631-85C1-4346-B52D-3F629962ABFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b4adf198757e8cb84c79e718d1bc35c4b3583a29","datavalue":{"value":{"entity-type":"item","numeric-id":1090673,"id":"Q1090673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"811eac08cf6cee0ffa13da8aaa89325d885c74e6","datavalue":{"value":{"amount":"+0.8259852","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1123184$9056E586-C976-4DF5-B444-4EFB99FCC118","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b2a268163365589a0d288d821dc138c43e323937","datavalue":{"value":{"entity-type":"item","numeric-id":2563451,"id":"Q2563451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7eea75c9830e098fd4d6fb89d6115ca2b8f13fdb","datavalue":{"value":{"amount":"+0.82196784","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1123184$BBF7783F-183E-462A-9E0A-F32CEA402AC8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Incompleteness of first-order temporal logic with until","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Incompleteness_of_first-order_temporal_logic_with_until"}}}}}