{"entities":{"Q812102":{"pageid":813950,"ns":120,"title":"Item:Q812102","lastrevid":64554978,"modified":"2026-04-11T20:40:25Z","type":"item","id":"Q812102","labels":{"en":{"language":"en","value":"Types of I-free hereditary right maximal terms"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5000205"}},"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":"Q812102$5CF324D4-5A1D-4A53-9EE9-5DCB4BF48296","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0f271d88421999845c5a152272f74c7a8da6874b","datavalue":{"value":{"text":"Types of I-free hereditary right maximal terms","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q812102$3C6EA151-0EEF-4587-8F12-1F734F012026","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"70189dcc6f721f641d0ec88ee14bcbe1320dbbc9","datavalue":{"value":"1089.03011","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q812102$05D7CC4D-E8FB-44F4-B3CB-AA42947564CE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"66f84fbf84627872ee8e4f09b27f58a25c3028cd","datavalue":{"value":{"entity-type":"item","numeric-id":266640,"id":"Q266640"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q812102$B591E57A-404C-4F07-A1CA-6CE3A0C90DCD","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e692f569038e7bcb7d3e72ba14d8d8e224046270","datavalue":{"value":{"entity-type":"item","numeric-id":169434,"id":"Q169434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q812102$489FBC45-37AD-478E-AE45-3F4FB5D18718","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6610cb28786ccc6a9ecdb40c1345499030b519d5","datavalue":{"value":{"time":"+2006-01-23T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q812102$2B4B0F72-0B01-4823-BEAC-DC73948AAE8B","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"4df2ed4026962bc09674f7d6c3106c9b573c957e","datavalue":{"value":"By the formulas-as-types (or Curry-Howard) isomorphism, for every closed \\(\\lambda\\)-term there is a theorem of the implicational intuitionistic logic \\(H_\\to\\), which is its type. Also, every such theorem is the type of a \\(\\lambda\\)-term which represents a natural deduction style proof of the theorem. The theorems of weaker logics than \\(H_\\to\\) have subsets of the closed lambda terms as their sets of proofs/inhabitants. Such subsets of the closed lambda terms were identified by \\textit{P. Trigg, J. R. Hindley} and \\textit{M. W. Bunder} [``Combinatory abstraction using \\(B, B'\\) and friends'', Theor. Comput. Sci. 135, 405--422 (1994; Zbl 0838.03012)] for a large number of logics including the implicational fragment \\(T_\\to\\) of Ticket Entailment. Other work on this appears in the reviewer's chapter ``Combinators, proofs and implicational logics'' [in: D. M. Gabbay and F. Guenthner (eds.), Handbook of philosophical logic. Vol. 6. 2nd ed. Dordrecht: Kluwer, 229--286 (2002; Zbl 1065.03002)]. The current paper also identifies the class of \\(\\lambda\\)-terms representing the proofs of \\(T_\\to\\) and finds a Fitch-style formulation for \\(T_\\to\\).","type":"string"},"datatype":"string"},"type":"statement","id":"Q812102$8CBB7229-1C42-4CBC-B394-1EF52AB68B63","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q812102$F6A07642-00F7-4A7D-B685-0567D06368E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b363e494c684597e57f0cc15c7c0d8f9f3bcf9fc","datavalue":{"value":"03B47","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q812102$39BDA297-775B-41D0-9A0C-343BCBB73FDD","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5c74125679b139e5038682f8d34f55a5cd9422a6","datavalue":{"value":"5000205","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q812102$18EB40EA-F46B-4235-A76E-48416ACCB394","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"46702c6954cd4327c8ecee41c7fc6cb0048d3911","datavalue":{"value":"Combinatory logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q812102$B36D6013-0284-48D8-9F04-A3C329838C15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"48fe5da30f2000a910dd1a06f280ea2b3174328d","datavalue":{"value":"decidability","type":"string"},"datatype":"string"},"type":"statement","id":"Q812102$30F0B670-E368-4DB5-A1C9-433F8B975DDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b876698d821b50cd7ba02ddb5424ed80f1905d8","datavalue":{"value":"lambda calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q812102$BE822CFB-CC3F-4D17-ADCD-5C9178B8D309","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7245057d33d9a959e820bafe53b372c083536e6","datavalue":{"value":"natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q812102$3502BBEC-392C-4FE0-9F24-49F2DEFDCA22","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"376f136d3715d0668145bfef82b652dbeb24818d","datavalue":{"value":{"entity-type":"item","numeric-id":591019,"id":"Q591019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q812102$7D7ECBBA-F9B9-4C7A-B48D-23B1F57D35F7","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":"Q812102$CCED27C1-3760-4A37-A716-C30905A5F593","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"619c5a590796a5f620721e0d64a49d8c472ee136","datavalue":{"value":"https://doi.org/10.1007/s10992-005-2831-x","type":"string"},"datatype":"url"},"type":"statement","id":"Q812102$446715CE-8840-4DE1-A97E-0E96D1CE2D03","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5bf269edff34983104eaa8385be3938f81a2c236","datavalue":{"value":"W1969075264","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q812102$10930329-97E1-42A2-9DEB-68C939934CF5","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec09860f6f4856a0bfa1fcbed713df420a357696","datavalue":{"value":{"entity-type":"item","numeric-id":4085699,"id":"Q4085699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q812102$6E1525F8-0B46-4F7F-AD55-B90269D49C9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bcad1b51622bd87c59556af8c797422562d18a92","datavalue":{"value":{"entity-type":"item","numeric-id":4297115,"id":"Q4297115"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q812102$8223898E-9BD6-4956-A21E-D0D46CE064AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"15ffb46be9e49b237f6fde18c89e459513c877e1","datavalue":{"value":{"entity-type":"item","numeric-id":5547552,"id":"Q5547552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q812102$6323E7CE-64E5-4479-B469-4F1F197EFE64","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":"Q812102$DD1219ED-CA9C-47B8-B8E7-D2A19AB23562","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77f473aa08523f9a9a313b9aaded66a723dd75c9","datavalue":{"value":{"entity-type":"item","numeric-id":2553958,"id":"Q2553958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q812102$F617CEF8-AF44-4C46-8827-B7C3E29F6564","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1ebb81c5b91fbc05a090177adc4268ae243c00fe","datavalue":{"value":{"entity-type":"item","numeric-id":4342081,"id":"Q4342081"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q812102$3A5ED941-3BDA-4FB4-8989-3F9CD9BC5C95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5bbed57047570d97d4afd4eabda171670dfd2346","datavalue":{"value":{"entity-type":"item","numeric-id":2703808,"id":"Q2703808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q812102$8B261C72-D94A-44A8-98E2-14DB4C598DFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d18ca94c9b6fbb6087987abf23a68e215a4b57a","datavalue":{"value":{"entity-type":"item","numeric-id":1237066,"id":"Q1237066"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q812102$52C2611F-79A3-4407-8445-BB5FF3E8E036","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":"Q812102$2423302D-7754-4D39-9F3A-5867ED138D0D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c6837bd112ac58ca3bbce4b7b29cef4a46d73f70","datavalue":{"value":"10.1007/S10992-005-2831-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q812102$A0B0454A-2F35-4BB1-908D-18AD3EB694D8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b10a625021a0858b8f886bb18497e17fe079acec","datavalue":{"value":{"entity-type":"item","numeric-id":4916555,"id":"Q4916555"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1cc1cb1311998ede5d0e446f41ac6e7f4d86e0cb","datavalue":{"value":{"amount":"+0.7428849339485168","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":"Q812102$D2E363EE-39F0-4862-82E1-4F88D9E0C61D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"22b99fc825103aaeb693f5f9f8f03f9fea47d93d","datavalue":{"value":{"entity-type":"item","numeric-id":4925031,"id":"Q4925031"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"66651109a45de79284005fe5cafa69a765e361fe","datavalue":{"value":{"amount":"+0.7356717586517334","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":"Q812102$FC2E4CD1-207D-4A8C-A421-6E74A13062A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"523ceda9c46f837435b012e3131d159e916a802b","datavalue":{"value":{"entity-type":"item","numeric-id":1575928,"id":"Q1575928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8cbe5497c525db0d4e33a7a3d8455ba8e0278cca","datavalue":{"value":{"amount":"+0.7101632952690125","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":"Q812102$42C74E65-F164-46D6-B729-425DC2DE4B42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3762fc33dad403a22d56c5f18a16f5cfe7e3c744","datavalue":{"value":{"entity-type":"item","numeric-id":691126,"id":"Q691126"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e4627abbbc120d3f6d97e6f67da246824b0d9b9e","datavalue":{"value":{"amount":"+0.7101592421531677","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":"Q812102$E9FD2978-B663-4CFE-A948-EA1034B86E1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4d8c44a7ac909c85f8cda057466d5139f4dda388","datavalue":{"value":{"entity-type":"item","numeric-id":1694477,"id":"Q1694477"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"10deeaac8c07d7d8e9268f6aa8f6b1378543d779","datavalue":{"value":{"amount":"+0.7007039785385132","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":"Q812102$9EB47481-1883-4B5A-BDE6-27ABE613AAB2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Types of I-free hereditary right maximal terms","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Types_of_I-free_hereditary_right_maximal_terms"}}}}}