{"entities":{"Q2500813":{"pageid":2511556,"ns":120,"title":"Item:Q2500813","lastrevid":49898419,"modified":"2026-01-11T20:06:09Z","type":"item","id":"Q2500813","labels":{"en":{"language":"en","value":"Proof-theoretic semantics for classical mathematics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5047762"}},"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":"Q2500813$BCCABE94-98B7-4BE8-A614-B2F2F1B92133","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f94c7aabde1cc7effdaeb393a555b0330cbab0bf","datavalue":{"value":{"text":"Proof-theoretic semantics for classical mathematics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2500813$7F5DCE11-A8E6-4873-9156-D65CDDD8FD0F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"73de9e83a1a36388f63285998c5acdc484a1ea0d","datavalue":{"value":"1104.03059","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2500813$9D193BD3-A610-40A6-9BD4-7DFC4534C942","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"760745bbc6b5c9a1a5cd89c9feef2726e8d06aec","datavalue":{"value":{"entity-type":"item","numeric-id":2500812,"id":"Q2500812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2500813$2ACD0617-612C-4A77-9524-C09D070C36CF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"28921346d64a666ce2dd47540df2f388e07634f5","datavalue":{"value":{"entity-type":"item","numeric-id":162813,"id":"Q162813"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2500813$8FD5ED3F-ED74-4D16-8768-39231828C624","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2dbf0d064b7b30d698c2952a304e12fd601ac87c","datavalue":{"value":{"time":"+2006-08-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2500813$AFD2CC8C-E27F-485C-9277-63E3837CC854","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"923a47f1098e39a3be1617566f5fb2ebe3ecacac","datavalue":{"value":"This article originated from the 1999 conference on `proof-theoretic semantics', and in it the author extends Curry-Howard's `formulae-as-types' notion from constructive mathematics to classical, thus showing, according to the author, that it ``does not need to be founded on an inchoate picture of truth-functional semantics in the big-model-in-the-sky, a picture that can in any case never be coherently realized.'' In this paper, the author discusses only the elementary theory of types and objects, and does not touch upon numbers or arithmetic. After setting up formalism, including type-base and object-forming operations, the author shows how to get rid of variables from \\(\\lambda\\)-abstraction and quantification by means of combinators. He defines extensional equality for each type. Also, the principle of the excluded middle is shown to be not about truth values but about the introduction of ideal elements, and its connection to the comprehension principle is exhibited.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2500813$817FAD7C-88D5-4799-AD60-CB96907E1CAB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d971f250f4b60bd91da7e9350568180af141e6af","datavalue":{"value":"03F03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2500813$69F00D75-1A5C-4976-918C-7388C24AEB72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e671cb9a7cd5542f21890d12b2e8ee004a8c8889","datavalue":{"value":"03C99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2500813$54F8A74D-AB9B-4B23-9145-24A7A355500B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2500813$72E51AD2-F65B-47B7-A70A-16A108926CCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2500813$E8A0EAAB-3B08-4F76-A362-E26044229377","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"90fa7e2ff4cb78cc60642b164270faa9b3f395ed","datavalue":{"value":"5047762","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2500813$73020A21-6CDA-4E6B-A893-F3DABABFEC60","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c5ad769370a61737150762bbe31791625ec17b85","datavalue":{"value":"types and objects","type":"string"},"datatype":"string"},"type":"statement","id":"Q2500813$1D7FDC4B-F64F-4EF0-B66F-8D13FAD3922C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fda66cc14b4a2e488220a5793b9239d3f9f1f56f","datavalue":{"value":"variable-free","type":"string"},"datatype":"string"},"type":"statement","id":"Q2500813$7649E2E0-24B0-462F-AA83-C9F4C45D70DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"98afc8bf077732faa7b36e358825aad09c7afaa7","datavalue":{"value":"proof-theoretic semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q2500813$69E0508A-5D65-41EA-A4F1-8B426201D924","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":"Q2500813$D6F2C8BB-0569-45B2-8884-03932B3B2B7A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"840270c5c1cd63312f82704fdaee2368409b361e","datavalue":{"value":"https://doi.org/10.1007/s11229-004-6271-x","type":"string"},"datatype":"url"},"type":"statement","id":"Q2500813$961C79B6-480C-4C7D-8DA1-CE6E92B9AD34","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"54eb11fed9c66e2128617cc3b1bb5acade25063f","datavalue":{"value":"W2049638658","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2500813$E2854F92-51CA-484D-B723-800E061F363A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ee5ac48bc66d7918ce3d169b23c5947ccc95caf","datavalue":{"value":{"entity-type":"item","numeric-id":3257767,"id":"Q3257767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2500813$29FC02B4-4ED4-4F7D-9741-C3871A5B20F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ae542aa49195da2f0564220c3e6d6c6c5762344","datavalue":{"value":{"entity-type":"item","numeric-id":769601,"id":"Q769601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2500813$088DFB68-D037-49A7-AE4A-19475F64EA43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dfa03673a22904351b77dbc72cf01417c04eb97d","datavalue":{"value":{"entity-type":"item","numeric-id":2702592,"id":"Q2702592"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2500813$E1291EEE-7E88-46E2-8365-4BB358042DC3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9a646e55a18f10ee50f4a28b44b578bf49a2f45a","datavalue":{"value":"10.1007/S11229-004-6271-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2500813$A1E2C68B-8397-41DE-8F25-5A945B530811","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e9f59cf9210ab60a60c25cb7b5f4507dd705a1fd","datavalue":{"value":{"entity-type":"item","numeric-id":4340496,"id":"Q4340496"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"97532ff0a4a73f04b06dfaec8ae548d209618ee5","datavalue":{"value":{"amount":"+0.7563989758491516","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":"Q2500813$66EA9C71-5F86-4E43-8567-82F1A49565B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a6abce847cf695a1699d312233c2b4b9995b7529","datavalue":{"value":{"entity-type":"item","numeric-id":580341,"id":"Q580341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b646e5bafee772bbaa81f01ec64c32fd60a50f49","datavalue":{"value":{"amount":"+0.7304844260215759","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":"Q2500813$CAD35AE8-AFF3-499D-BFE4-4FB9BBCF1C95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8a40b525022ec1dccaba201ae6fd7476bf823c4c","datavalue":{"value":{"entity-type":"item","numeric-id":4856946,"id":"Q4856946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fcd52abfd6a485ff8bc519e0d59a947632c13332","datavalue":{"value":{"amount":"+0.7278064489364624","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":"Q2500813$DC432976-4D46-4F22-AF2F-262842BDCA2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fa4cc4e163d96ec665e22b90913b2f57598d1d5d","datavalue":{"value":{"entity-type":"item","numeric-id":5286647,"id":"Q5286647"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"432209ce1436dd8ea707dcf824d034ea66b8b2a7","datavalue":{"value":{"amount":"+0.7208877801895142","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":"Q2500813$EFA6FE15-60BE-4F20-AF38-BB12EE4E8AFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fcc2d6a22da579c1d4fbf32c42a0633df44845d9","datavalue":{"value":{"entity-type":"item","numeric-id":5957852,"id":"Q5957852"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6b1bfc3d835be4761144c6105d9fc141f15ec730","datavalue":{"value":{"amount":"+0.7206531763076782","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":"Q2500813$DF964658-0BE3-401B-869C-2D8600F3CAED","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2500813","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2500813"}}}}}