{"entities":{"Q1891931":{"pageid":1902673,"ns":120,"title":"Item:Q1891931","lastrevid":73715457,"modified":"2026-04-14T17:01:05Z","type":"item","id":"Q1891931","labels":{"en":{"language":"en","value":"A note on the proof theory of the \\(\\lambda \\Pi\\)-calculus"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 761091"}},"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":"Q1891931$9D60A512-3561-4BBC-8034-BFA109CC3CD4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ccaa71742acb3927557507f1ed0839f42989c267","datavalue":{"value":{"text":"A note on the proof theory of the \\(\\lambda \\Pi\\)-calculus","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1891931$95A3398F-C365-45E0-AF5D-F5F2588A6D5D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1d1359b994cb09efc3471ac35c1c43996e68df9c","datavalue":{"value":"0831.03030","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1891931$55C350AB-DB00-467A-9BDE-2C5094525B98","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"10e2d31e65c737b3517d4f19440f4321445d6dc8","datavalue":{"value":"10.1007/BF01063152","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1891931$E509C705-CA48-4F18-A6C8-A7F54D207F86","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9f49fd2ae3d1da3d59eca25d7c6331cf7590a3c6","datavalue":{"value":{"entity-type":"item","numeric-id":1826633,"id":"Q1826633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$88B71B1E-2180-4957-9801-758A94BDBF83","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e34236ca73b92c6ee0bc17431d03c3537a7f0792","datavalue":{"value":{"entity-type":"item","numeric-id":195358,"id":"Q195358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$FA9AFEDB-A151-4402-8F1C-44332E755F79","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5eaeb2c9097fea69c487fbd2ea3e5d8c5e6a6b7a","datavalue":{"value":{"time":"+1996-02-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1891931$4C8F218F-3E79-41E0-901D-FC6E0F3E344A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b7641a90741378f1cc3a64dabcf4fdeddeb8c02e","datavalue":{"value":"The \\(\\lambda \\Pi\\)-calculus is a theory of first-order dependent function types, and so is a member of and/or related to the Edinburgh Logical Framework. Logics for computer science have been developed with an eye to checking formal proofs, etc. In this paper, the author turns the table around and proves the cut-elimination theorem (which was formulated and proved for a formal calculus by Gentzen six decades ago) in this \\(\\lambda \\Pi\\)-calculus. He formulates \\(\\lambda \\Pi\\) in two formats; one as natural deduction, N, and the other as the sequent calculus, \\(G\\). Then he shows the equivalence of G, N, and G-cut, establishing the eliminability of the rule, cut. Here, this rule is formulated as: from \\(\\Gamma \\vdash_\\Sigma M\\):\\(A\\) and \\(\\Gamma, x\\):\\(A, \\Delta \\vdash_\\Sigma X\\), \\(\\text{infer} \\Gamma, \\Delta [M/x] \\vdash_\\Sigma X[M/x]\\). In the second half of the paper, the author formulates and mentions a number of meta-calculi for proof search in \\(\\lambda \\Pi\\), utilizing ideas of unification and of resolution. Here is an example: first, he presents the calculus, NR, with a resolution rule, and shows its equivalence with N. Then he formulates a meta-calculus LNR, and shows: \\(\\Phi\\) is an LNR proof of \\(\\Gamma \\Rightarrow_\\Sigma A\\) if and only if NR proves \\(\\Gamma \\vdash_\\Sigma M\\):\\(A\\) where \\(M\\) is the extract-object of \\(\\Phi\\).","type":"string"},"datatype":"string"},"type":"statement","id":"Q1891931$B3AB6DB9-607F-4500-B139-DADCA06092B1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1891931$4F2334C0-23D9-4A45-ADD8-55DFD9174CBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1891931$7414E243-50B5-4D5B-95D8-0F6B1CE140B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1891931$B1CC85BC-BDCB-4DD4-B47C-3874030F7F8D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4be701cb7ec83b8ae20747a6af481900f2f57256","datavalue":{"value":"761091","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1891931$27B7E803-6A1E-4949-919B-C2E8EED64414","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b4ea14a753c4c46db3704ceac154670a93e59db5","datavalue":{"value":"Logical Framework","type":"string"},"datatype":"string"},"type":"statement","id":"Q1891931$A7DF093E-5607-4F45-9E2C-6C9E994C3EC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ee0a69ba46a5f23ccf6ad83fcf01b7501a19fa4e","datavalue":{"value":"cut-elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q1891931$FB35E5F2-33E8-46C8-AD13-AF981C49E606","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7245057d33d9a959e820bafe53b372c083536e6","datavalue":{"value":"natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1891931$7E8377FF-B820-4F30-A85D-636E9644A3B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c7d4aa0d3cf1745112ae7d594a2a5578f4e767f","datavalue":{"value":"sequent calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1891931$7B879380-FFD4-4E9B-A532-73F18D73DF30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4879e8c35d56fd297a402f7c1eba53238e04d57b","datavalue":{"value":"proof search","type":"string"},"datatype":"string"},"type":"statement","id":"Q1891931$A882AB68-6F3C-4E99-BB67-C222D0370039","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"666b9a47dc68ef552d799234146196fb61f3c743","datavalue":{"value":{"entity-type":"item","numeric-id":33169,"id":"Q33169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$D959282D-4084-44EC-A77F-12DEA6E81441","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":"Q1891931$C91CC676-F00C-4C52-8379-0AD4BFC6018B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c43d802f7fd6c267e5d32c3cf557b56e8f197773","datavalue":{"value":{"entity-type":"item","numeric-id":923083,"id":"Q923083"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$7C5C478C-D484-4F2A-ABB0-3F1BEAD0F25D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f7c99e107348aa82bd1ed9ca721c57c6ffc4f86","datavalue":{"value":{"entity-type":"item","numeric-id":688571,"id":"Q688571"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$EBF12D81-4503-4BA3-8DBF-4494F611C7EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d63e1d2c1097bf56f38b3464089e43c611b33ec4","datavalue":{"value":{"entity-type":"item","numeric-id":4939697,"id":"Q4939697"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$7496C791-FC55-4DDC-8BBD-D3BE4F6F69F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5adae15f6654acfbcf7621f32cd882969fbf6d8f","datavalue":{"value":{"entity-type":"item","numeric-id":1096716,"id":"Q1096716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$2B821CC5-0BEF-4D62-9B96-3A13B213BC5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70200912b15e3f6d8f97f26c605e4ed0a53464e8","datavalue":{"value":{"entity-type":"item","numeric-id":3919057,"id":"Q3919057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$860A13F8-340B-4139-9075-2D2E1CAB49BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27e31b151b8d22be2aa79bf2dfac73aa834ed045","datavalue":{"value":{"entity-type":"item","numeric-id":4012882,"id":"Q4012882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$16DA59B1-9FAF-4B1F-A024-DC91C0AED08C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84ad42be65af5dfa9e512f666229d02ed5041b60","datavalue":{"value":{"entity-type":"item","numeric-id":3856127,"id":"Q3856127"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$D20023DA-4F0D-4A22-A67D-9F662777231D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e74a7a357b1b46dc042b2194329594218f6b370","datavalue":{"value":{"entity-type":"item","numeric-id":1840142,"id":"Q1840142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$7B3D07A0-E7E9-45F6-80E5-1E01C3882D1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"021e6e2184fd3d7f831680d56b426b95217eac7a","datavalue":{"value":{"entity-type":"item","numeric-id":4033837,"id":"Q4033837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$13211AE0-63B0-4A32-A739-3C81413875AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f23417d0146cdc8808662ea4f0b0496e878f3547","datavalue":{"value":{"entity-type":"item","numeric-id":4722037,"id":"Q4722037"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$AC616536-8986-41DB-B135-5A7343A9A10B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"04bd6fdad25e36998ceb580f40c70d0e0fd67a3b","datavalue":{"value":{"entity-type":"item","numeric-id":3722468,"id":"Q3722468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$D2786A98-D0D3-4F28-957A-D27DA37EE975","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e7e43f784716a014f37546d3a4d6870aa0b11fe","datavalue":{"value":{"entity-type":"item","numeric-id":4744243,"id":"Q4744243"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$38773D8C-ADF5-45AF-9942-EA31A7E57FAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aebd32d099ee8c91552756addce4fb86715ed2d8","datavalue":{"value":{"entity-type":"item","numeric-id":2640596,"id":"Q2640596"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$04066554-F2EF-48D9-9156-4F7DD71597EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5333f404cb1c5a483ee97a9aa8db2143fb09170b","datavalue":{"value":{"entity-type":"item","numeric-id":4012879,"id":"Q4012879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$17E6190D-7F41-4992-93FC-2C942C5E400F","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":"Q1891931$06122AEA-3833-4ADB-9F93-AC20A8E105C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47a53c9ec1ed01dcb444298314487a4908d29766","datavalue":{"value":{"entity-type":"item","numeric-id":5286030,"id":"Q5286030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$26A05066-DC98-4A5B-94BA-F6F87C03F3F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"996546e15b6fbeb64dd43e0ea4bb4b45c952f698","datavalue":{"value":{"entity-type":"item","numeric-id":4012884,"id":"Q4012884"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$62042D55-6304-4C6E-9C24-FA1A17D60667","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$501EAC0F-3325-4285-AF23-EF29840F51FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"02e642d35b27f6202fe5a95f273070d49f953ce5","datavalue":{"value":{"entity-type":"item","numeric-id":3691668,"id":"Q3691668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$37A88BD8-C1BE-4112-8D0A-0C62CAEAA7CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bacb5aa102ce6c71274c34a5360472cea903ae3a","datavalue":{"value":{"entity-type":"item","numeric-id":2641297,"id":"Q2641297"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$D758445F-BB85-4AD4-A588-01FCD6AE14E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c90b2e0ced1298041d18e0c665831758c400276e","datavalue":{"value":{"entity-type":"item","numeric-id":4052084,"id":"Q4052084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1891931$DA518221-8887-4F52-B6D6-D63E3BD17242","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"452b25f8262b4dc37f73326ee7da67099a47a43d","datavalue":{"value":{"entity-type":"item","numeric-id":4012884,"id":"Q4012884"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1540f8c2e2d32921890a35ba53ba7f547485266c","datavalue":{"value":{"amount":"+0.8408960103988647","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":"Q1891931$496461BC-1059-4C8C-A167-FE2510EE1EC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec2f0bb38b56f759cbb69a7dc3cbce032e16f8c6","datavalue":{"value":{"entity-type":"item","numeric-id":5055716,"id":"Q5055716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1540f8c2e2d32921890a35ba53ba7f547485266c","datavalue":{"value":{"amount":"+0.8408960103988647","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":"Q1891931$C763A1CD-4EC9-4161-B957-86A248C7F01F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8293d39b4e139795d4cbfc0c1170fc2b9210bed3","datavalue":{"value":{"entity-type":"item","numeric-id":6488534,"id":"Q6488534"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"095d1546197b2eedfae670da49fa91352b87c7cd","datavalue":{"value":{"amount":"+0.8129501938819885","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":"Q1891931$D0E45DAE-4371-47D3-A2A9-C49D5CF25527","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aaae8b02556144ce3ed7738674e0ec95ed9ff1f9","datavalue":{"value":{"entity-type":"item","numeric-id":4223032,"id":"Q4223032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3eed4293ba6b231670d35f512471695613bdc444","datavalue":{"value":{"amount":"+0.7889596223831177","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":"Q1891931$CD28FF81-1551-4D20-B119-69ACF7BB1F8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0588fa81d050cdfd9c6444384081d8916c34387d","datavalue":{"value":{"entity-type":"item","numeric-id":3011126,"id":"Q3011126"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c2d27e0d1ab1fb836c132ddc876c4a27ad55e2ee","datavalue":{"value":{"amount":"+0.7824719548225403","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":"Q1891931$6B125A78-4E81-4AD9-95DB-9F7D9E66B9FD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A note on the proof theory of the \\(\\lambda \\Pi\\)-calculus","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_note_on_the_proof_theory_of_the_%5C(%5Clambda_%5CPi%5C)-calculus"}}}}}