{"entities":{"Q345704":{"pageid":347471,"ns":120,"title":"Item:Q345704","lastrevid":61131108,"modified":"2026-04-10T21:23:02Z","type":"item","id":"Q345704","labels":{"en":{"language":"en","value":"Realizability for Peano arithmetic with winning conditions in HON games"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6659111"}},"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":"Q345704$B582FBC5-2C3B-4705-A72E-9CE49DFE3EF9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6c61167debac38fd6f386c2a40a3f5693ae6d350","datavalue":{"value":{"text":"Realizability for Peano arithmetic with winning conditions in HON games","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q345704$E2861290-4D2B-41F4-B02C-7E434D80C9BD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"664e17a9a08b9e7bcba5ba5995b7d8259fccf739","datavalue":{"value":"1377.03020","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q345704$C356D260-0A5F-4A33-8129-40D09434ABB8","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e6a7c9fa9dc3fdeaa7fa6fbe2fe38f9449434b88","datavalue":{"value":{"entity-type":"item","numeric-id":345703,"id":"Q345703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$3BC52942-E8D4-4185-A891-582806865B00","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":"Q345704$06EE3B74-0448-4DEA-8CDE-0540A0A00590","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a54830ddddf8efde2ef9bbf0a00011143bf8f201","datavalue":{"value":{"time":"+2016-12-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q345704$D57FC94F-5A95-4EEA-9350-2B9EA789978E","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"bf05c748b19f894b0cb445a65a1da1ca24dbc809","datavalue":{"value":{"entity-type":"item","numeric-id":331053,"id":"Q331053"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$D156B611-F70B-427E-AEB2-4E7205A20D44","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q345704$58872983-D644-4F61-B26F-5B1233FACE50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q345704$CB00F058-D73F-4616-9311-B8C84A114B41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q345704$6EFB8CEA-F225-4991-B362-CF3BED5C4A9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"44bfe90f17a7ad0027a9dbba6d9564554d8f86b7","datavalue":{"value":"18D15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q345704$507ED91E-FE65-4842-9F54-46E7060B24E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d5c83f057600e5614b7fec59c8e4ac61cb41ba8d","datavalue":{"value":"91A80","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q345704$BF63FEDA-3718-4530-91B9-40C6776F6360","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c185a047e5e4660beb8188fe9300a2193b74ee45","datavalue":{"value":"6659111","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q345704$A99B5E72-69A1-459F-A946-C831541CC9AA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3329e5ddc19ec41605ea21e54e688588faa574a2","datavalue":{"value":"classical realizability","type":"string"},"datatype":"string"},"type":"statement","id":"Q345704$F500F61F-7EC7-4EB1-B78A-3F1F496BB79E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7090cb2b2cefa03cee6b50a67ca057c086ad0f00","datavalue":{"value":"Peano arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q345704$ED3951B8-5D38-48FF-BAA3-F8614D174631","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"10a7851ab6bb8feeb91b4fc2f18a3666f4b53097","datavalue":{"value":"Hyland-Ong game semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q345704$85114C73-8E05-4E16-97E8-08FD3F9C4ED4","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":"Q345704$77A684EA-5C2C-4AF9-B702-FDC45658E4CC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4b49e71b29b22268d7221d1e67790af43f4646e9","datavalue":{"value":"https://doi.org/10.1016/j.apal.2016.10.006","type":"string"},"datatype":"url"},"type":"statement","id":"Q345704$3983A0DB-553A-407A-9869-BD3EA6675292","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d7e22a27443f3cd2c7f92483fd502d6f09736623","datavalue":{"value":"W2536088897","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q345704$49CF056C-006F-41AD-BB74-536501BA4D1B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"2b6ebce8fe1caa0cc920eda8427c705be142a0fd","datavalue":{"value":{"entity-type":"item","numeric-id":4218919,"id":"Q4218919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$42086122-F5E0-4585-B5E3-46581EB8216E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bf1a90574c396a1ca159a0401d8596bb5f1e528d","datavalue":{"value":{"entity-type":"item","numeric-id":4212925,"id":"Q4212925"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$B9439513-3C0F-425A-AF8D-EE0DB2AF36EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"924615cc812e877b54f0924f817aedd2e5e64bd8","datavalue":{"value":{"entity-type":"item","numeric-id":5300895,"id":"Q5300895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$8AFDE98A-D964-4AE8-9376-42B96BEBE84B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8f0c5c319fbac55703dd54df44030fd4d305c3a1","datavalue":{"value":{"entity-type":"item","numeric-id":3637187,"id":"Q3637187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$9EBE8A9F-0001-4C59-BE64-47112F51893F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4bdc535713bd2a1bea0ebcab85559eb258068f92","datavalue":{"value":{"entity-type":"item","numeric-id":3617718,"id":"Q3617718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$81D067EB-0BAD-4D6B-ADC6-3B9EBCC14778","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"371d2399f50a6aebcc2fc70e10f9c3ee27554be0","datavalue":{"value":{"entity-type":"item","numeric-id":4836058,"id":"Q4836058"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$17D94002-6EE3-42D6-BD1B-B9532E94F6F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5128ea1fce41e0cabe1ccf3f99222f6d7ae49f43","datavalue":{"value":{"entity-type":"item","numeric-id":4225150,"id":"Q4225150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$F5B7B977-4804-4755-BDA9-22FF0D9CCD09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b44d5c81f7735368555911d4bd1908764544894","datavalue":{"value":{"entity-type":"item","numeric-id":1854393,"id":"Q1854393"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$0DE6971E-6244-4364-86A4-036B0D070403","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0b75dd3fb8b48431eb9ad5b02ce91286f91c46a4","datavalue":{"value":{"entity-type":"item","numeric-id":5945009,"id":"Q5945009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$8621F230-48EE-47A3-B604-80D8A592FCC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cbc492aae6606d7fc7e30022e1b80faa51ce6ed9","datavalue":{"value":{"entity-type":"item","numeric-id":1884884,"id":"Q1884884"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$8B1A41C1-F48B-4149-8FF9-72A95E157434","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0a6ae770783aa142e6dd68c83f480feb4b97dec8","datavalue":{"value":{"entity-type":"item","numeric-id":3075442,"id":"Q3075442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$CFAE6CBC-BE54-40F3-B6DC-11CCAF62A0A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"763baafdcc1d0af41a2e1d9bb74e4febdbc046a2","datavalue":{"value":{"entity-type":"item","numeric-id":2849884,"id":"Q2849884"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$E9A74C90-1665-4D61-9A99-6BC0CA32C730","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef5f9b53550980d4dcc97faaadee38a9f077def0","datavalue":{"value":{"entity-type":"item","numeric-id":2570134,"id":"Q2570134"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$CE1B91F5-1693-4DF2-A60F-0243E91BF22B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"473157de33e9daafb8a601b8d009c0cc6f89ba3a","datavalue":{"value":{"entity-type":"item","numeric-id":2503039,"id":"Q2503039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$8C4D1C91-16BB-44B5-8056-B06ACAE125A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d3f467bc7e738d5a5a1046302aa48cf4cb7d8fc8","datavalue":{"value":{"entity-type":"item","numeric-id":3003319,"id":"Q3003319"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$6527FF12-7617-439B-8A5F-271F00EE0B0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ed9b59a5650f74d0bf864ccb2b42bedecdab9a58","datavalue":{"value":{"entity-type":"item","numeric-id":4501156,"id":"Q4501156"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$94D5C25A-7E75-47CF-9687-1CAEC1EE1C51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6d25189cadcfb01bfb85424fb5e34c27a9558087","datavalue":{"value":{"entity-type":"item","numeric-id":2719799,"id":"Q2719799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$8060DE83-C568-4518-B520-833807901F17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e45693061e506ddfc304d90cb392dffdbb69b973","datavalue":{"value":{"entity-type":"item","numeric-id":4215635,"id":"Q4215635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q345704$5C799B5A-A1EF-49B3-81CC-6198AD08542C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7c21977626b1b3482f078a064665de976b2acf19","datavalue":{"value":"10.1016/J.APAL.2016.10.006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q345704$A5650D44-5F4F-460B-A79E-281F7B53CA02","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"534477ce7f639a0194f7d3f2879624eccf17ab63","datavalue":{"value":"Hyland-Ong-Nickau games are used to provide semantics for programming languages. In HON games, plays are interaction traces between a program (player \\(P\\)), and an environment (opponent \\(O\\)); a program is interpreted by a strategy for \\(P\\) which represents the interactions it can have with the environment.NEWLINENEWLINEIn the paper under review, the author presents a classical realizability semantics based on HON games, using winning conditions on desequentialized plays. The realizability relation builds on an interpretation of the \\(\\lambda\\mu\\)-calculus in a coproduct completion of the Cartesian-closed category of single-threaded strategies. It is shown that the realizability relation provides sound semantics for classical first-order logic and, further employing a relativization predicate, for Peano arithmetic.","type":"string"},"datatype":"string"},"type":"statement","id":"Q345704$7507F9F7-A0E7-4DAE-B803-9A33FEA7348E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"da2f69a68b77f3314fe1ffe66c45fa74ede0d992","datavalue":{"value":{"entity-type":"item","numeric-id":5300895,"id":"Q5300895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c2e97ab8599b64a5fc505f35c40fc327dd1e08be","datavalue":{"value":{"amount":"+0.9954347014427184","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":"Q345704$6F704EB5-5B45-4E03-95EA-249D94E9E54B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"910c9cce5b7e616f23f6714d9ffc588ab2ed830d","datavalue":{"value":{"entity-type":"item","numeric-id":5360216,"id":"Q5360216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b2836c8ec41c3c4833e7ace4e82a09512e7f3cfc","datavalue":{"value":{"amount":"+0.7432608008384705","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":"Q345704$C9980FF7-81E0-41BC-B4B2-5DD816F37CAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b97ed9fc3bacdb0b98adc91b8ad5a012c0dc0a7d","datavalue":{"value":{"entity-type":"item","numeric-id":1946669,"id":"Q1946669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"90727a9d4fafd9b1581dfde0bf1f40c411e79207","datavalue":{"value":{"amount":"+0.7371401786804199","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":"Q345704$7732FA45-6718-449A-983B-0BDBAA7C3F3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f65ea139cbd1b472cb8aaf49a16264799fe6325d","datavalue":{"value":{"entity-type":"item","numeric-id":4964695,"id":"Q4964695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a65c4d9a5289e4eebc6806e28308f4ff2929be01","datavalue":{"value":{"amount":"+0.730728805065155","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":"Q345704$70FE9686-C8B4-4065-A28D-2C3B5001A5A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ff9ddc6fe1a55941c90677f589ce0b4da36c7df","datavalue":{"value":{"entity-type":"item","numeric-id":4944901,"id":"Q4944901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d1d790b1ef9d7f53a47920d8f5546624c72a486f","datavalue":{"value":{"amount":"+0.7273780703544617","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":"Q345704$3F150870-BA35-4E5F-BB81-38B8231145DB","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":"Q345704$D83263CC-27AB-4DEA-A0EB-8E2C147201E9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Realizability for Peano arithmetic with winning conditions in HON games","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Realizability_for_Peano_arithmetic_with_winning_conditions_in_HON_games"}}}}}