{"entities":{"Q1326769":{"pageid":1337519,"ns":120,"title":"Item:Q1326769","lastrevid":68472909,"modified":"2026-04-12T23:56:23Z","type":"item","id":"Q1326769","labels":{"en":{"language":"en","value":"Classical logic, storage operators and second-order lambda-calculus"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 584676"}},"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":"Q1326769$5D06B6ED-5886-44B7-B232-C548C98BA144","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7fb3e93e2091dcca4d7fd5691be1cd4aed75287c","datavalue":{"value":{"text":"Classical logic, storage operators and second-order lambda-calculus","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1326769$A58D5452-99ED-4E85-A956-6BDE6AF8C385","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5258a054e14d8eb28821ee16efcf35e0bbf1eae9","datavalue":{"value":"0814.03009","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1326769$FD73B12D-3710-4452-BDFD-2F42D3804DF7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b3811116a0d2a4e7c7d4d1803b51cfc29fba92f5","datavalue":{"value":"10.1016/0168-0072(94)90047-7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1326769$49EB2BB8-F9C3-4258-9D2E-C2FD8237051E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3c930bfaa88d0466feb9bef34cfbca5f6b60b9e3","datavalue":{"value":{"entity-type":"item","numeric-id":206560,"id":"Q206560"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1326769$F8F79180-2B34-457B-9C6E-E6D8CFDFDF59","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":"Q1326769$505A8B42-FAAD-42CA-B140-2BEF94FFB904","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b284e35c1970c32b54ea678933b5f17581b0b244","datavalue":{"value":{"time":"+1995-06-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1326769$490D70B8-4478-4CD2-B13A-B03854778EA8","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"5a5ddc8a6b264d6ac8e1628e829772a7ff4df442","datavalue":{"value":"Storage operators, introduced by the author [Arch. Math. Logic 30, 241- 267 (1990; Zbl 0712.03009)], are a device to simulate call-by-value in a lambda-calculus with head-reduction. In this paper this concept is used to characterize the lambda-terms encoding integers in classical logic. Let \\(\\text{Nat} [x]\\) be the formula expressing in second-order lambda- calculus (also with first-order variables and quantifiers) the data type of natural numbers. An important consequence of the normalization theorem is that if \\(\\vdash M: \\text{Nat} [x]\\), then \\(M\\) is beta-equivalent to \\(\\underline{n}\\), the Church numeral for \\(n\\). When one extends the calculus with axioms (i.e., when the typing context is extended with typed constants \\(c_ i: \\sigma_ i\\)), this in general is no longer true. The paper considers the especially relevant extension obtained with the axiom \\({\\mathbf c}\\): \\(\\forall X(\\neg\\neg X\\to X)\\). This system, in view of G\u00f6del's double-negation translation, axiomatizes classical logic. \\textit{M. Parigot} [Lect. Notes Comput Sci. 592, 361-380 (1991)] has shown that closed elements of type NAT in this extended system can be characterized in terms of storage operators: If \\({\\mathbf c} \\vdash M: \\text{Nat} [n]\\) and if \\(T\\) is a storage operator for integers, then, for any variable \\(f\\), \\(TfM\\) reduces by head reduction to \\(fN\\), with \\(N\\) beta- equivalent to \\(\\underline {n}\\), depending only on \\(n\\) (and not on \\(M\\)). The nontrivial proof uses a realizability argument. All the preliminaries, including those on storage operators and the proof of Parigot's result, are clearly explained in the first part (pp. 53-70) of the paper. The result, besides its direct technical interest, is of potential relevance also for the ongoing research on the extraction of programs from classical proofs.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1326769$AA853746-1B6C-4C52-B627-3B875E94CB52","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1326769$6E71C1F5-C216-49A4-BDB2-7086B340CD06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1326769$E8D45C8B-C3D3-49BF-A09B-EB2B91C75483","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2d9b0393dc84d97672017819be486c80791f1875","datavalue":{"value":"584676","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1326769$4ACE3F91-208C-4A00-810E-B1738089134E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e24821d94cc8c80abb5ca9331a432b22abfec884","datavalue":{"value":"continuations","type":"string"},"datatype":"string"},"type":"statement","id":"Q1326769$413C2C44-B679-4747-9119-9AF90049ABD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"33fd81627acd56a240fde0d4d7060d89e19d0782","datavalue":{"value":"System F","type":"string"},"datatype":"string"},"type":"statement","id":"Q1326769$A174F78E-7506-4466-B581-30B04794E2DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c94e0e5e9635edbab684bb87e21548292f90eade","datavalue":{"value":"second-order lambda-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1326769$0D95FF86-E630-434D-AA73-0651294F695A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"df4c05e8e858ce3e724a86a3f85b018eab12dbf2","datavalue":{"value":"data type of natural numbers","type":"string"},"datatype":"string"},"type":"statement","id":"Q1326769$B1862CF2-7405-4D95-A00B-3806B3255180","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9ffd3928aa1fd818bc1a8806528172e266ac8bcc","datavalue":{"value":"classical logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1326769$151CFC63-C19B-4D3E-9B25-13124FF0459B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8237243ac39caa3580f4136f84722538eb343898","datavalue":{"value":"storage operators","type":"string"},"datatype":"string"},"type":"statement","id":"Q1326769$F37F96F7-1E9A-4697-BCE0-AFD6AA863450","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e94b821003739a6c053dd26268b48fdf6756cf9c","datavalue":{"value":"head reduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1326769$B679F359-3AF1-4C75-ACD2-5268F1B44FC3","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"00ea4a5ed8879c1a6adc0802c8c4ce48d27b9055","datavalue":{"value":{"entity-type":"item","numeric-id":596036,"id":"Q596036"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1326769$AC11683D-ABF8-40A3-9B2E-52412637260C","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":"Q1326769$00F54EC6-E3DF-4680-8AD6-54CABB09764F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"72ff42d91f0f1e17e47dd77c2f3925a7a5dbf2c2","datavalue":{"value":"https://doi.org/10.1016/0168-0072(94)90047-7","type":"string"},"datatype":"url"},"type":"statement","id":"Q1326769$544733A0-B81A-4A4B-A8BE-6C71F00814F9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1c8581923ef83f74a7abb6f6771f667aee8a1675","datavalue":{"value":"W2007974484","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1326769$A8CC10E3-581E-4067-B445-C81A5B1EDC5F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"98f21a4a0099d31e158836c7dcfba6aa43c852ab","datavalue":{"value":{"entity-type":"item","numeric-id":3342534,"id":"Q3342534"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1326769$721802E5-4E03-4814-9433-420BFFA14C6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5cb3fb1f5163c51d21987992526ad7f1b03bc113","datavalue":{"value":{"entity-type":"item","numeric-id":5625124,"id":"Q5625124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1326769$543B148E-2C89-4DE0-B792-BFF581A06AB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d66518f09c99314187d256b3e54c7fdc6eb07ce","datavalue":{"value":{"entity-type":"item","numeric-id":4006233,"id":"Q4006233"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1326769$75CD71AC-E696-42F8-BDE4-EC4F2E568276","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14fba5e8ace22a05b3ebef9aa0392420cd4ad549","datavalue":{"value":{"entity-type":"item","numeric-id":685059,"id":"Q685059"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1326769$FD52E7B4-0BB4-4CEE-9E2F-18A523976FD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16de9a4f8e129e311d9ce09ae9e120dd4a226b8b","datavalue":{"value":{"entity-type":"item","numeric-id":3997016,"id":"Q3997016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1326769$28B3331A-F694-432E-BA8C-0FE0EA8E9E6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62728de11085b2637852fd5b2e4cd2194b3b9d02","datavalue":{"value":{"entity-type":"item","numeric-id":923069,"id":"Q923069"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1326769$64B13377-38AA-47D4-8AE6-09182ECE0162","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"36b355c034a15b6951cab8a2fb9dd01fb3be3dbf","datavalue":{"value":{"entity-type":"item","numeric-id":3477935,"id":"Q3477935"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1326769$93053BDB-1734-4AFE-AA95-32A945E5D984","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb9a53038a3e03bede13deef3624bad6ce441e04","datavalue":{"value":{"entity-type":"item","numeric-id":4264064,"id":"Q4264064"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1326769$850D4639-23EC-4ACE-9FA8-06A3B86DA0D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66257d76632b86525de5e8f5c47c6c6cf781ec1c","datavalue":{"value":{"entity-type":"item","numeric-id":4255509,"id":"Q4255509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1326769$384A7664-9EC2-4794-A36D-77914E74C4B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e27be5516997b567899ad0b0d96cb56d275522c","datavalue":{"value":{"entity-type":"item","numeric-id":1225449,"id":"Q1225449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1326769$DAF12209-2B23-4982-B2C5-4154A9AC3196","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e0c07f282afbe8a43758987596b036e7de351b8b","datavalue":{"value":{"entity-type":"item","numeric-id":923069,"id":"Q923069"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c8fd9122c54f68931dd5b092e9a54bf9fd0bf287","datavalue":{"value":{"amount":"+0.830154538154602","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":"Q1326769$74492F8C-CCB4-47D2-ABC9-3299DA67940D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"25ccbecfbc626beea6f239547add4cea8fa0c237","datavalue":{"value":{"entity-type":"item","numeric-id":3142911,"id":"Q3142911"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"38f3b094bc293c15b053dc914e409e2b806c3a61","datavalue":{"value":{"amount":"+0.8010852932929993","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":"Q1326769$65F7E0EF-6E75-4FF6-A6E1-67781671F658","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"01e0543f12dcc75b2e1908820bcde5d5ee0eb1eb","datavalue":{"value":{"entity-type":"item","numeric-id":1917084,"id":"Q1917084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"55321c133b10353625e64421b7b7e7144b177ca1","datavalue":{"value":{"amount":"+0.8010851144790649","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":"Q1326769$52431E4F-627F-4BF8-9E04-BEA7A41D886F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4db78fd63e4377c07a547e19509873ac907360e8","datavalue":{"value":{"entity-type":"item","numeric-id":1329740,"id":"Q1329740"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"de10d891e7e078a6eca0f617fb01ed37ed914e5a","datavalue":{"value":{"amount":"+0.8000075817108154","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":"Q1326769$9019D27B-F0B2-4A97-BD50-ACBE5034A769","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"344ec4df97e3b2b5cd7773baa442fe478afe76b6","datavalue":{"value":{"entity-type":"item","numeric-id":4862127,"id":"Q4862127"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a8127d7a315d76820fb4145c0ae18aa55a13df34","datavalue":{"value":{"amount":"+0.7973722815513611","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":"Q1326769$0201377D-F561-4456-BD24-F1A27D66A2B5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Classical logic, storage operators and second-order lambda-calculus","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Classical_logic,_storage_operators_and_second-order_lambda-calculus"}}}}}