{"entities":{"Q1625591":{"pageid":1636332,"ns":120,"title":"Item:Q1625591","lastrevid":72839895,"modified":"2026-04-14T08:10:48Z","type":"item","id":"Q1625591","labels":{"en":{"language":"en","value":"On arithmetical completeness of the logic of proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6986591"}},"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":"Q1625591$6912BAEA-A755-4749-AC4A-9EDB881BE0DC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d0198db6e6ace01aba9f8ff2a7a2c1ffabf3ea57","datavalue":{"value":{"text":"On arithmetical completeness of the logic of proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1625591$8D7D5A06-6AED-4BA3-A9E1-C311E45BDA82","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7d2d033c943d037cb0849372077e9d10bcecdc77","datavalue":{"value":"1412.03022","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1625591$68B75386-E46E-4113-A229-D557886E9A00","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7523585c785045bead275e6fbe25bcaa71b52517","datavalue":{"value":{"entity-type":"item","numeric-id":1625590,"id":"Q1625590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1625591$F8E9F2F1-0DD3-4091-9A86-AEFAED6A1007","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"128c2b12d65261607bd53a5a5505e34270780d7e","datavalue":{"value":{"entity-type":"item","numeric-id":312495,"id":"Q312495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1625591$C74F790B-B1AE-4B57-97BC-D5BCC2BFD44A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1625591$2236D0EB-3FD0-4CE6-BF1A-8D79EA9D0F78","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"90fc82896c37d679c242bb4883bc4b47e7985482","datavalue":{"value":{"time":"+2018-11-29T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1625591$D76E3D1C-A8BF-4421-BBA1-4EC066390C62","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b65692daf4216f124563ba0fdc7c6e790c5f4f28","datavalue":{"value":"\\textit{S. N. Artemov} introduced the logic of proofs \\(\\mathsf{LP}\\) [Bull. Symb. Log. 7, No. 1, 1--36 (2001; Zbl 0980.03059)]. The logic of proofs \\(\\mathsf{LP}\\) includes several modal-like operators that allow formulas of the form \\(t:X\\) (intuitively meaning that term \\(t\\) is a proof for formula \\(X\\)). The logic \\(\\mathsf{LP}\\) without the axiom necessitation rule is denoted by \\(\\mathsf{LP}_0.\\) Artemov [loc. cit.] proved the arithmetical completeness theorem of \\(\\mathsf{LP}_0\\).   A stronger version of Artemov's arithmetical completeness of the \\(\\mathsf{LP}_0\\) is proved in the paper under review. Moreover, the authors prove a version of the uniform arithmetical completeness theorem of \\(\\mathsf{LP}_0,\\) i.e.\\ there exist a \\(\\Sigma_1\\) proof predicate \\(\\mathsf{Prf}(x,y)\\) and an arithmetical interpretation \\(\\ast\\) based on \\(\\mathsf{Prf}\\) such that for any \\(\\mathsf{LP}\\)-formula \\(F\\), \\(\\mathsf{LP}_0\\vdash F\\) if and only if \\(PA\\vdash F^\\ast\\).","type":"string"},"datatype":"string"},"type":"statement","id":"Q1625591$1EAD5AF7-61E2-45FD-BD64-3E883A60ADDD","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"4f8e4d6d96d31b6da2906ce2893c15ec96871a66","datavalue":{"value":{"entity-type":"item","numeric-id":190353,"id":"Q190353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1625591$B0BA3CD9-AB36-498E-8A37-ECFBF5843905","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"b638c7935436ccffba7a737e2b57436cbbd2533c","datavalue":{"value":"03F45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1625591$275C7F15-6D43-4786-AD62-A2C4FF71492A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1625591$C27C23DF-F752-4742-A1EB-36F113428A4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1625591$69EC1CB2-7871-4E24-955B-232B4F087560","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c44e4550b60355cc572c6c4d7a5a72dc0832c1d0","datavalue":{"value":"03F40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1625591$4D1EBD2D-BF58-4D93-8B11-0A626328A41C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5465c04ca168b65400b448f5bfafaa24f1775547","datavalue":{"value":"6986591","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1625591$97BF35EA-01DA-4811-B0C0-DBA9E56AE8F6","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7e2e21a984526b8024b04acd04fd80cbaaf58f4b","datavalue":{"value":"logic of proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1625591$4237559C-D751-4BDD-BDC8-73338D6010E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4ff02888b791812ddffc3fccfc663496a3736af7","datavalue":{"value":"arithmetical completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1625591$3666AC89-FD67-4796-8319-A1037A7C048A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"370f3df2f45f377ce5764f58ee5e633266fb94f2","datavalue":{"value":"proof predicates","type":"string"},"datatype":"string"},"type":"statement","id":"Q1625591$8D79CD75-3CC9-4209-A412-0A62F2C3000A","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":"Q1625591$497B20F7-A7E1-4293-A56D-6D1FBD8B30A9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a67bd58b76f1f2177cdcfa12f689da05794481b7","datavalue":{"value":"https://doi.org/10.1016/j.apal.2018.09.004","type":"string"},"datatype":"url"},"type":"statement","id":"Q1625591$F1702DF8-5EDC-4C67-B89A-33E9DDC61A77","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"386913f8fce13bb6333bb9cdea5f4e20f7896b43","datavalue":{"value":"W2890211092","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1625591$95E4FC98-C4D4-4A64-946F-469576675175","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"e08931818cd4fb47767f4f8b58546a3178ced777","datavalue":{"value":"Q113880328","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1625591$6F193B32-A0A6-48A1-965D-811D21AD6992","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ceb7872ca8844112136937ea41bf92a162143dcd","datavalue":{"value":{"entity-type":"item","numeric-id":3752370,"id":"Q3752370"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1625591$A31F1D24-2281-4815-8156-4BF86DD0B1FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e1a6ebb360b6bfc3a111b832b5231ca5c9153b7","datavalue":{"value":{"entity-type":"item","numeric-id":2732527,"id":"Q2732527"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1625591$47BF82EE-02AB-454A-84AA-FFB74878548C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c77d029ca17e8cbeae5ff8bc11ecd94cb2895f59","datavalue":{"value":{"entity-type":"item","numeric-id":3714054,"id":"Q3714054"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1625591$D340DE65-58DD-43CC-AC47-5930AF51FA39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"41704d75503b555029d696b92528a73c9193d861","datavalue":{"value":{"entity-type":"item","numeric-id":3944575,"id":"Q3944575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1625591$F1855ED9-8140-4DAC-8CAE-F966BCC153AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dba3659de23929a44a1642cbbbc4ab273698ed56","datavalue":{"value":{"entity-type":"item","numeric-id":4437331,"id":"Q4437331"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1625591$ABD9BF36-ED64-41E0-9953-D6E6119EFBC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1dfbfd3fd8285c1b250d4a94e1be2061d1444016","datavalue":{"value":{"entity-type":"item","numeric-id":4376067,"id":"Q4376067"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1625591$C0142232-F65E-4317-92AF-0D8E75D482D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a575b135ab8c68ef066d427f8c2b91aeb49e6000","datavalue":{"value":{"entity-type":"item","numeric-id":3852250,"id":"Q3852250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1625591$6EDD2E49-70C2-472F-B5A3-2EF0A463EF24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65af634f8ea04e9717486b98f2f6b61acf5b154f","datavalue":{"value":{"entity-type":"item","numeric-id":1235695,"id":"Q1235695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1625591$65AE934F-1B1B-4196-A738-2725BEA8729D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b1dea56ea644446392244f914c11b5f353f5ad33","datavalue":{"value":"10.1016/J.APAL.2018.09.004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1625591$335CDC03-3D94-4467-A7E1-AD8B343A81EC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"044291259c567a861f70b4edb59a603305874c53","datavalue":{"value":{"entity-type":"item","numeric-id":3094147,"id":"Q3094147"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f31641b1f89d6393c776c4a1bdf86967e2a99560","datavalue":{"value":{"amount":"+0.8917515873908997","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":"Q1625591$B7AE2BB3-06FD-4887-A6C6-E890B04431BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"69f0206eee7ec92afebd05ca513872623e5a8e30","datavalue":{"value":{"entity-type":"item","numeric-id":703832,"id":"Q703832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cdef47589e8955a59f7be0b7faf9357054fe0e76","datavalue":{"value":{"amount":"+0.8740904331207275","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":"Q1625591$1167DAA3-D3A1-4EF5-A227-A0B0971B1CE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b90ab663875c7c8317669cbfa1f597cc59f7ffe8","datavalue":{"value":{"entity-type":"item","numeric-id":5294019,"id":"Q5294019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa71c0184757213f673bf69826bf6fd51a62cb74","datavalue":{"value":{"amount":"+0.8664036393165588","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":"Q1625591$71BB0478-80CA-4422-96BB-9E8BC95D136A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ddff6a2c9b0a71362c60ce75f039eff25b36331c","datavalue":{"value":{"entity-type":"item","numeric-id":2753697,"id":"Q2753697"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6cfe75c64c5c0d589d4143651caacb91ce4f9fef","datavalue":{"value":{"amount":"+0.8609668612480164","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":"Q1625591$34A9571F-41FB-44C5-9A15-135ED5E42E6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bfdfe9e8d4e40a77511aa05163b15c6ac721e36d","datavalue":{"value":{"entity-type":"item","numeric-id":4644547,"id":"Q4644547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6cfe75c64c5c0d589d4143651caacb91ce4f9fef","datavalue":{"value":{"amount":"+0.8609668612480164","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":"Q1625591$61E46D99-34F8-4CFC-9D79-911B7F882A22","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On arithmetical completeness of the logic of proofs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/On_arithmetical_completeness_of_the_logic_of_proofs"}}}}}