{"entities":{"Q1101100":{"pageid":1111852,"ns":120,"title":"Item:Q1101100","lastrevid":66135087,"modified":"2026-04-12T07:46:46Z","type":"item","id":"Q1101100","labels":{"en":{"language":"en","value":"Arithmetical axiomatization of first-order temporal logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4045719"}},"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":"Q1101100$11A2A46D-87D7-4E86-BEEA-FD41448DC68F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ff07b0f771c25661308f8e1033b17986a8e0c611","datavalue":{"value":{"text":"Arithmetical axiomatization of first-order temporal logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1101100$A72738D4-71BC-4AB9-AACD-234CB3BEC5C0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e431967ee139be153be9c7b2f87eff1f7e9fd9de","datavalue":{"value":"0642.03018","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1101100$05A72E74-9662-4580-8320-F9B3DA619339","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f31a0801e9239ca9f28225d165dcc84730638e90","datavalue":{"value":"10.1016/0020-0190(87)90047-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1101100$BA82583F-1441-4771-BA26-7073566267CE","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"52fa7d44b58d0511cb8993765bd916aef86052d8","datavalue":{"value":{"entity-type":"item","numeric-id":63092,"id":"Q63092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1101100$2974DA48-8974-4D92-A8AD-4F028407FEEF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5ae48c61eed19d1e1e1f33f9255d5b329362d064","datavalue":{"value":{"time":"+1987-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":"Q1101100$28226FD7-10F4-4FAC-9CEC-956D8BFF715D","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"4d0301879809b0e0b546358292d0a99506b8626c","datavalue":{"value":"The paper is devoted to a syntactic characterization of first-order temporal formulae valid in Kripke structures that contain arithmetics of natural numbers. It is impossible to provide a finitistic and complete axiomatization of first-order temporal logic with linear and discrete time. In another paper the author has presented a complete but infinitary proof system. In order to deal with finitistic proof rules, one can consider arithmetical proof systems. A new method of obtaining arithmetical axiomatizations of logics of programs is introduced.    A many sorted first-order language with equality, \\(at\\) oerator (A \\(at B\\) means that A holds in the next state that B holds), local and global variables, nexttime operator \\({\\mathcal O}\\) applied to local variables is considered.    Two proof systems are presented: the first one, PN, for logic \\(L_ 0\\) with the only temporal modality \\({\\mathcal O}\\). The second one, PA, for logic \\(L_{at}\\)- a full temporal logic contaning \\(at\\), too. It is shown that PN is sound and complete, and that inductive defnitions do not add to the logical contents of arithmetical temporal theories based on \\(L_ 0\\). The proof system PA is shown to be arithmetically sound and arithmetically complete.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1101100$27C0F151-C340-416C-82E8-3A34A8D0067D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1101100$B746908A-8D8F-4184-9588-9E1132587CB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1101100$284319E7-A97D-4F27-BBF6-9DC65398B5D3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"275e14a06f6d175daa4abc7b4384962396be90d7","datavalue":{"value":"4045719","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1101100$50E5AB10-BB2D-4C8A-9E5F-7F9DEBFA795F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4ff02888b791812ddffc3fccfc663496a3736af7","datavalue":{"value":"arithmetical completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1101100$112DF55D-0CF7-49EA-9A72-85660CE8CDDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ee3eabf068a032eacfb187bf2ca0f45abd025d2b","datavalue":{"value":"arithmetical soundness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1101100$7AF75A1F-E64A-4179-B38F-A4B7B80AC029","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"000d054838ba79f1c83227281d29722f07d85a76","datavalue":{"value":"Kripke structures","type":"string"},"datatype":"string"},"type":"statement","id":"Q1101100$C184CE5E-3581-4C1E-82FB-C32A5FA83004","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4a1a1b4de2f6601636779c475343b36943870036","datavalue":{"value":"first-order temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1101100$F8A2BBB9-6D12-43BE-9652-D281E19B9B02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9b26281765fd6f75f31ee2fcdb5343ed665b7ead","datavalue":{"value":"arithmetical proof systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1101100$348876BD-CE1D-4D59-A15E-76D99FF68333","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7e0cf683ce28aea4f7e4494b6461847d3e756038","datavalue":{"value":"arithmetical axiomatizations of logics of programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1101100$E27B369F-CBE9-4C33-AA75-1DCAC7F2BF50","rank":"normal"}],"P16":[{"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":"Q1101100$81322AC8-E650-4C88-9A06-76BF29239C9E","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"f16d300f1af622676dccb372accc3bc0c9d577af","datavalue":{"value":{"entity-type":"item","numeric-id":588374,"id":"Q588374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1101100$3D2AF11A-F7B4-4DC4-A82B-E10A690BEB4D","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":"Q1101100$CFEE0A01-9BF6-47E4-A94A-FEB7FF0A034D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8c1f1662fb8a8d8d47dd20ca4adca2b5260f4e83","datavalue":{"value":"https://doi.org/10.1016/0020-0190(87)90047-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q1101100$E900C108-D0B2-4468-8C6B-C93565276385","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ccb7599d35cb74f6dbead200a2e884056de45188","datavalue":{"value":"W2015571575","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1101100$70710677-7151-4806-92D6-372D1AE77751","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2c71c26bf7e075dc23cee40b3135f1af13e67a2","datavalue":{"value":{"entity-type":"item","numeric-id":4151703,"id":"Q4151703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1101100$35C65088-0FCD-4968-A6BF-6B2197119827","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5710cd0fb8b5907d40eeada6e14d4018e26669a5","datavalue":{"value":{"entity-type":"item","numeric-id":1255942,"id":"Q1255942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1101100$30150D7D-DC4E-459A-B180-0C06093FA6F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d0c0494e343ccadfed43fe5761af39dbee3392a9","datavalue":{"value":{"entity-type":"item","numeric-id":4160382,"id":"Q4160382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1101100$5DEE4D3A-8E87-42E8-9E8F-264A1E18DF53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1101100$3520895F-59D2-42C3-B92D-BE90B8675A27","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":"Q1101100$C4B59DC9-5392-4107-BF08-39B95E213975","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"45c73db8b3c2a0a30e7c3eaaca382d1ea005a940","datavalue":{"value":{"entity-type":"item","numeric-id":3677141,"id":"Q3677141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1101100$CC3FED7D-61C4-41AF-8FCA-2DE3F17CEC0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5b4c95f53b57f2eb31607a9241c4b370cdcd831","datavalue":{"value":{"entity-type":"item","numeric-id":3939208,"id":"Q3939208"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1101100$6F3332F6-964C-474A-81A0-375A1DD30F81","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":"Q1101100$0B1772FF-38C4-4BA8-86CA-8D0399F1FD30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c56abf17fe38c9d6f19bb07c76c7c037b3d964b6","datavalue":{"value":{"entity-type":"item","numeric-id":1102941,"id":"Q1102941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1101100$5E6B7AB8-C2F0-4965-80A3-5555216728E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d9456d9b3e59e143f5e55b694b92114428f6e73","datavalue":{"value":{"entity-type":"item","numeric-id":1123184,"id":"Q1123184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1101100$99C99123-F96E-4A7C-BADA-17DD08230EC9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"341fc183e534ecaf9bb2c42b864481a6c925c178","datavalue":{"value":{"entity-type":"item","numeric-id":1118578,"id":"Q1118578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0f68e65b3a422a79964c58878e4f0fa2317eec31","datavalue":{"value":{"amount":"+0.8572895526885986","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1101100$0BB7255E-EDE7-4801-8AEE-99C005DC45A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"081bd63286da1909b7245ea381f5077097f31ff7","datavalue":{"value":{"entity-type":"item","numeric-id":2913981,"id":"Q2913981"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"234ac2634b44562ae6d5924b98bacd653888a7c3","datavalue":{"value":{"amount":"+0.8570249676704407","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1101100$06C4C2BF-5EF6-4FE7-B0E3-2AE8F8CAFA1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"46a6d0aaee26eaaec2e49277d698939f014f41fc","datavalue":{"value":{"entity-type":"item","numeric-id":915718,"id":"Q915718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4fb1f07f5fb32ded43d9030db0e84f7c485a85a8","datavalue":{"value":{"amount":"+0.8487012982368469","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1101100$1C02334D-A5BF-4C24-9F53-81782E6893AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"faf473c9db566695247ab3f0587faa9d503c8c5d","datavalue":{"value":{"entity-type":"item","numeric-id":1102941,"id":"Q1102941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3bb704f5820681ea1def576a80b7e995f7f7c28d","datavalue":{"value":{"amount":"+0.8367118239402771","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1101100$3187E22F-FE20-4CCC-88C5-677DB03362A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"891ec74453572b7814cf8b5c6c0909e95aa17119","datavalue":{"value":{"entity-type":"item","numeric-id":4353629,"id":"Q4353629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3bb0ef86704465d0aa00ffeff52870847daa0f2b","datavalue":{"value":{"amount":"+0.8136100172996521","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1101100$ED600EAB-90A4-4746-9FC8-0E8E04E9DDFE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Arithmetical axiomatization of first-order temporal logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Arithmetical_axiomatization_of_first-order_temporal_logic"}}}}}