{"entities":{"Q2566069":{"pageid":2576812,"ns":120,"title":"Item:Q2566069","lastrevid":74231238,"modified":"2026-04-14T19:04:59Z","type":"item","id":"Q2566069","labels":{"en":{"language":"en","value":"A simple proof of second-order strong normalization with permutative conversions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2207225"}},"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":"Q2566069$A0CAF2F3-CDE5-497F-BAA1-95466FC90B9C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e5a5f62380ee3edbdcbeb06c172a79006d101cdb","datavalue":{"value":{"text":"A simple proof of second-order strong normalization with permutative conversions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2566069$D4D66B92-22A8-46CF-8CAC-E825E1E8C334","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3c5305cbfae341130986d1788058825ea50b2c67","datavalue":{"value":"1095.03057","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2566069$52E204DA-FBF4-4FDA-91DC-6F355E44F940","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a26d759a8f15177451aa97ef2fc9836978dfb443","datavalue":{"value":{"entity-type":"item","numeric-id":278746,"id":"Q278746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2566069$D64FC64E-E247-4594-8A1F-D6B74A3EA67E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"739bb59f926e46bf270e3affee77bc2ef6969661","datavalue":{"value":{"entity-type":"item","numeric-id":454365,"id":"Q454365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2566069$07893927-CCB2-4635-84BB-C32142D23555","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":"Q2566069$E597355E-1D6F-41C8-9101-AA0851C52AC0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6ec9da92ba7b4e525d61f27d0c249399f1779b4c","datavalue":{"value":{"time":"+2005-09-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2566069$72C74F3C-41B8-4515-9A78-439C5A34F2B5","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"65ff4552c95e0d2ee4249111c1706fdca5d4a7fb","datavalue":{"value":"The authors present a proof of strong normalization for first- and second-order intuitionistic natural deduction including disjunction, first-order existence and permutative conversions. It follows the Tait-Girard approach using computability predicates and saturated sets. As main technical advantage compared with other strong normalization proofs in this area, the authors (re)establish a convenient modularity of the proof (p.~135f): ``Instead of natural deductions deriving a formula \\(A\\) one works (via Curry-Howard isomorphism) with corresponding \\(\\lambda\\)-terms of type \\(A\\). A useful device introduced in [\\textit{W. W. Tait}, ``A realizability interpretation of the theory of species'', Logic Colloq., Symp. Logic Boston 1972--73, Lect. Notes Math. 453, 240--251 (1975; Zbl 0328.02014)], [...] is to switch to untyped \\(\\lambda\\)-terms, some of which can belong to a set \\(\\bar{A}\\) of computable terms of type \\(A\\). [... A] simple induction on \\(A\\) proves that all terms in \\(\\bar{A}\\) are strongly normalizing. After this it turned out to be possible to prove that every typed term \\(t\\) of type \\(A\\) belongs to \\(\\bar{A}\\), hence strongly normalizes. The second proof is by induction on the term \\(t\\). [...] Most of the obvious attempts to define sets \\(\\overline{\\exists x A}\\) and \\(\\overline{A \\vee B}\\) of computable terms of type \\(\\exists x A\\) and \\(A \\vee B\\) stall because the complexity of the conclusion \\(C\\) of the \\(\\exists\\)- or \\(\\vee\\)-elimination rule [...] is not connected in any way with the complexity of \\(\\exists x A\\) or \\(A \\vee B\\). This difficulty is resolved in the present paper by additional conversions \\((\\exists)\\), \\((\\vee 1)\\), \\((\\vee 2)\\) [...], which allow us to define \\(\\overline{\\exists x A}\\) in terms of \\(\\bar{A}\\).'' The paper gives not only a simple and complete proof of strong normalization for various first- and second-order logics, but the proof is also ``suitable both for extensions to stronger systems and for teaching'' (p.~135).","type":"string"},"datatype":"string"},"type":"statement","id":"Q2566069$3F4BB53C-5731-4358-8793-C75EADC37DC6","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"698ef69cf2501558685cb66472f90d21aa909f07","datavalue":{"value":{"entity-type":"item","numeric-id":194998,"id":"Q194998"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2566069$C361556B-E54B-4265-8FFC-535FB81D4A5A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2566069$472F8C8B-221A-4AEC-BC33-80AAD993E59A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2566069$B8AF38F6-4F06-4FEC-982F-8DD960927349","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2566069$BB3B4A6E-E6DD-4774-9016-25C9B7ECB506","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"91a8f48501b104871db472fd7ed35836bfc9f1aa","datavalue":{"value":"2207225","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2566069$2E77A5F4-4F63-4D95-B905-A4EFEB086DD1","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"af462e56ed2ce88a42c8df0ec7f2dc6a55ded212","datavalue":{"value":"strong normalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q2566069$7A5ACB7F-D94F-4FE1-A6AA-0BFD890963D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"15796d431e57463b26d4f2da913a40ab41040b54","datavalue":{"value":"permutative conversions","type":"string"},"datatype":"string"},"type":"statement","id":"Q2566069$B7D4E8F5-9B80-4C91-ABDC-3380E01F4A8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2e5020beaaefb57c7061501010e4301087091a54","datavalue":{"value":"second-order natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2566069$8309C3A4-74C9-49A5-AB06-05912CD6A47F","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2566069$B62D8647-C9BB-4B08-8309-62A6A852F139","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":"Q2566069$AE4D19FC-6568-4BD1-BFD8-76EA0EFAFDDC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5f4c84024298d539426818626f1c869b4cec0291","datavalue":{"value":"https://doi.org/10.1016/j.apal.2005.05.009","type":"string"},"datatype":"url"},"type":"statement","id":"Q2566069$D53EFD9F-74D5-4EB9-9014-3FDE6D4CA492","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"91dca213f2a0739d5c76524d6627bbf15cc8ca9b","datavalue":{"value":"W2034989554","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2566069$F382EEE1-9548-410B-96E2-67C8489E757D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"27ceeb9d1d61c6f5a256858dc451469f1b7db716","datavalue":{"value":{"entity-type":"item","numeric-id":4650284,"id":"Q4650284"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2566069$9CD43012-A7D4-42CB-8851-8A6328DBE7E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84c43b5305804b9a8d81c8c472c25b8921246913","datavalue":{"value":{"entity-type":"item","numeric-id":1400711,"id":"Q1400711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2566069$1E2D8391-22D6-4B85-B251-0805575C6B23","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":"Q2566069$DF52941B-2865-4FD0-B286-0E7B80D0189B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99c6176bcb92cea3bde43c51d54f8875f446d09c","datavalue":{"value":{"entity-type":"item","numeric-id":3994895,"id":"Q3994895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2566069$8C70B3FC-5585-47B5-B4DD-221543CA0347","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe478b1c9e3755ecb4683bf76c070eb4413865c0","datavalue":{"value":{"entity-type":"item","numeric-id":1407578,"id":"Q1407578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2566069$1CE375C1-853C-4E5F-9AB2-A55E1D6508B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a9979469b08338cac6986677509579b97c8bd2d0","datavalue":{"value":{"entity-type":"item","numeric-id":4083402,"id":"Q4083402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2566069$E7FD5579-8A57-4B94-A63D-40CB6184B715","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bc3da221ef639195800fa999b5da3717f501950b","datavalue":{"value":{"entity-type":"item","numeric-id":5638282,"id":"Q5638282"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2566069$C7826D2E-054E-43EF-9164-D14B3DE59A51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bdd017d35f44f14a51ba00ad5bb8a601ffea5446","datavalue":{"value":{"entity-type":"item","numeric-id":1772778,"id":"Q1772778"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2566069$ECFC0281-A3B0-434E-B10B-E4729D428D1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"348178f282a0443f05b752d7893cd6cfb0db1cf7","datavalue":{"value":{"entity-type":"item","numeric-id":4376065,"id":"Q4376065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2566069$DA791D24-8001-499F-B419-F64F36F0E57E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8d95625ec9e5b7c46cee42d87256157d982706a","datavalue":{"value":{"entity-type":"item","numeric-id":5559220,"id":"Q5559220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2566069$B9CB4C35-052C-47C8-97C8-216F42D6F467","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ed6186f00d683b4c7cb7f70af7a03fd2b654c87","datavalue":{"value":{"entity-type":"item","numeric-id":5632554,"id":"Q5632554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2566069$E9FA2264-EF4C-45AE-B163-9A4E605A7612","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9bd4384e04df05a6d681d8752a6931ccfe2df646","datavalue":{"value":{"entity-type":"item","numeric-id":4093416,"id":"Q4093416"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2566069$B5D2D49C-6FA7-4EB1-B55C-E85C35980551","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2507a1c7e65ba41d8c11044b1c4d9b2d4fd57c93","datavalue":{"value":{"entity-type":"item","numeric-id":3160566,"id":"Q3160566"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2566069$1342423D-A66C-453A-A151-C420B7E68575","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"384c88ee747368e498e55b1ebc22017816448ffc","datavalue":{"value":{"entity-type":"item","numeric-id":2265415,"id":"Q2265415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2566069$C9B6B734-DA5A-4D47-A222-8F6808C3ED0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"56327724d8101cacc3d4e5b36700dc86a7feb472","datavalue":{"value":{"entity-type":"item","numeric-id":4499084,"id":"Q4499084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2566069$9671B6B8-2AEE-455D-ACE2-8D540B872AA4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6eb04f5c392d5367d17aa4c73807c620fc3f037f","datavalue":{"value":"10.1016/J.APAL.2005.05.009","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2566069$0838A8DA-EF18-403D-9F2E-41680BC7728D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"26a1e95e103b48b2ec9f98a8e4b8a2be4e2bde0b","datavalue":{"value":{"entity-type":"item","numeric-id":3599163,"id":"Q3599163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4bfb98435f014be89d0ba90ec42c2a72933476bd","datavalue":{"value":{"amount":"+0.8282250761985779","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":"Q2566069$5DF3CF7B-B1ED-4036-AEBC-8749CB5AFE65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"19095695d51e2717ea9a5b5b5543a588beae2a57","datavalue":{"value":{"entity-type":"item","numeric-id":1407578,"id":"Q1407578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"330406104ddc4415638237260db709e7525bb795","datavalue":{"value":{"amount":"+0.8234164714813232","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":"Q2566069$F7F065C0-3BB8-48A7-9C5B-A8D4E363FFA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"05d1cb7f50ff15314687d4e9e68913f9827f827e","datavalue":{"value":{"entity-type":"item","numeric-id":2482841,"id":"Q2482841"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2d9c9a9a53091522e0d33c955823f0cb9e69b5df","datavalue":{"value":{"amount":"+0.8201735019683838","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":"Q2566069$FD6728AF-95F5-4399-B032-49E71244C53E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1d97faa2ac5a7df01c3b864c90903470d7e32d38","datavalue":{"value":{"entity-type":"item","numeric-id":4382485,"id":"Q4382485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8377d0fa8ab5e4f2ba2082f67026b9841716f693","datavalue":{"value":{"amount":"+0.8087654709815979","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":"Q2566069$2FF1063A-63E7-4B2D-B549-6DBFB85BF4A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7ab8f2efce65f1bb0e13fc4caa073a89436edf6c","datavalue":{"value":{"entity-type":"item","numeric-id":1769440,"id":"Q1769440"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a7c633e94e16889b8245f635cf178d4c5b6c9fff","datavalue":{"value":{"amount":"+0.8020405173301697","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":"Q2566069$4887A528-345E-4418-8E23-E5604FB27D58","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A simple proof of second-order strong normalization with permutative conversions","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_simple_proof_of_second-order_strong_normalization_with_permutative_conversions"}}}}}