{"entities":{"Q1099173":{"pageid":1109925,"ns":120,"title":"Item:Q1099173","lastrevid":69637299,"modified":"2026-04-13T08:22:08Z","type":"item","id":"Q1099173","labels":{"en":{"language":"en","value":"On the syntax of Martin-L\u00f6f's type theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4039894"}},"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":"Q1099173$4560AB56-CC61-42F6-A4DB-7AC472100E05","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0a3b553583bcbdf6ba0be288654a7d747234f1ab","datavalue":{"value":{"text":"On the syntax of Martin-L\u00f6f's type theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1099173$A29F4263-2CFC-4191-9D33-32966F6B8097","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"32732d31f8d357e52d1fdc1e1bcfaddcc5066984","datavalue":{"value":"0638.03056","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1099173$5568C6C4-34EB-4608-8C50-22C9152A6801","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"34b1e073a9a30d0a4aff4759a2bf4dd532119755","datavalue":{"value":"10.1016/0304-3975(87)90047-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1099173$60EB590D-8AB4-471B-B4AF-0F397493A101","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fd7bcd31c089eea43fd8677a5426b0c7b8e7e1a7","datavalue":{"value":{"entity-type":"item","numeric-id":792318,"id":"Q792318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099173$24D254BB-B7C1-4A51-B5F7-99323BB43E5D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099173$82121DEC-0A8D-4D35-9CA7-AB2EE16C17FD","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5ae48c61eed19d1e1e1f33f9255d5b329362d064","datavalue":{"value":{"time":"+1987-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1099173$52D2128C-4CFB-4782-90CF-E1ED9ACA00F0","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"6d1f13692ab78f236940d9e01037e9a91d5f4ebb","datavalue":{"value":"The paper gives a precise syntactical presentation of the arithmetical fragment (without universes and W-operator for the formation of well- founded trees) of Martin-L\u00f6f's type theories, both in an intensional and an extensional version. Some elementary proof-theoretic properties are established, such as normalization of terms, the equivalence between several versions, and the dropping of type-statement premises.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1099173$78E649CC-0136-4A6A-BB0B-E175B5268C3B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1099173$54419A07-E7C6-4B79-9148-9FD072C09B95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1099173$E3F3A6CE-7AED-4B09-A5F8-1CD9F92DF1F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1099173$2FD42F8E-D7A3-44BC-9FD8-0AE61E7FAE20","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b407880f1388391f91aeac0ecd9a6df3a0853511","datavalue":{"value":"4039894","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1099173$1B0B4D37-412F-49A7-B170-55B587A45973","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"289597ff22a7a4e6233f6186cb534e188c47190f","datavalue":{"value":"arithmetic fragment of Martin-L\u00f6f's type theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q1099173$6B50A291-9436-48D8-972A-3538401B7F54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"712e9aa867d72c292c7318cda071015aa51c0447","datavalue":{"value":"normalization of terms","type":"string"},"datatype":"string"},"type":"statement","id":"Q1099173$389B253F-4352-4329-9783-FDC91BBC430E","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":"Q1099173$E06824F5-7460-4CE9-BFE1-E0C4ED79DC8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099173$68528B88-0537-4EE2-B451-376473F25BFB","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":"Q1099173$182B5400-005D-4372-B4E1-8445300E1AEF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e058e22587c458fa072816308b071eac88623d30","datavalue":{"value":"https://doi.org/10.1016/0304-3975(87)90047-8","type":"string"},"datatype":"url"},"type":"statement","id":"Q1099173$A9273E76-EDD4-4EE6-A153-E6FC1ADCF3B1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c86f86a702c08f24a41e4fc49b87cc1accb2c3e0","datavalue":{"value":"W2068339813","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1099173$3CCF8969-6D8E-453D-BEB5-CAEC26F9D830","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9779d2f20504dba38f482f942c0abc04f8e04e14","datavalue":{"value":{"entity-type":"item","numeric-id":3310616,"id":"Q3310616"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099173$6E3406F2-A6A7-4361-B650-E97F9663E224","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"783487fbe7d5d00c916a5e1c362e506e08b899ca","datavalue":{"value":{"entity-type":"item","numeric-id":3678692,"id":"Q3678692"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099173$2CC0B303-0D62-4466-B660-F08BE80D9BE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b2e1ab8d6c4a6ea4362f203e5137d4541ef80eb","datavalue":{"value":{"entity-type":"item","numeric-id":3679172,"id":"Q3679172"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099173$32072DD9-4840-490C-B9DF-6E44F5C96CDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a0ad9da17a866aedbb1fcb0b1b80324ca70c7695","datavalue":{"value":{"entity-type":"item","numeric-id":5619069,"id":"Q5619069"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099173$D654F862-893A-49DD-A17F-B1D01970212A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae94f828af67e50fecbc9e4b645ed6964977b9db","datavalue":{"value":{"entity-type":"item","numeric-id":4099613,"id":"Q4099613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099173$F948613E-39D8-4169-AA5B-26EFD773AD46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86f69e4e3c6e6db6273645f322c23116e1ad1c80","datavalue":{"value":{"entity-type":"item","numeric-id":3343983,"id":"Q3343983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099173$CD6DBF9B-BF88-4017-9431-C3B94D96F14A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b0ec3118c55b6f3ab232f29debefc8c9d383a9","datavalue":{"value":{"entity-type":"item","numeric-id":3688389,"id":"Q3688389"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099173$50563C8A-1512-48B9-B6E3-282FA0F81C2E","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":"Q1099173$5A281958-FD8F-4832-90CD-E57B837F2AC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f6313bd92712173f409ee1f96aff08f4d96c5cbb","datavalue":{"value":{"entity-type":"item","numeric-id":3768897,"id":"Q3768897"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099173$6533F27C-EB7F-4B49-B395-9B24167A9096","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":"Q1099173$85C2ABE8-DB0D-490E-B191-EF26EC79501A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"385f9359a1dec0777500656b0fbfb3f247ade24a","datavalue":{"value":{"entity-type":"item","numeric-id":3313859,"id":"Q3313859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099173$AA9AB7B1-8F74-4D9B-B4AE-49E6243C5C92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1971f0a5aef4d2d81e705aaa7589e687d7ce05a3","datavalue":{"value":{"entity-type":"item","numeric-id":1092042,"id":"Q1092042"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099173$7FF07112-D490-4AB0-BA98-7E51619BD26C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a5928533f1a1251f0d11dc18c7b4ce473f48af9","datavalue":{"value":{"entity-type":"item","numeric-id":4187337,"id":"Q4187337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1099173$62B0A4ED-57A8-4EA1-8CFB-8E380D370C90","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":"Q1099173$4C64C0CE-D134-44D2-B01A-CD98F9454218","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f74c98b5a48e2ad52f2ae1ef2655d9c93c15c5d6","datavalue":{"value":{"entity-type":"item","numeric-id":3322097,"id":"Q3322097"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fef4867ffba80c520248f25ab5e2e2ec2616149f","datavalue":{"value":{"amount":"+0.8090963959693909","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":"Q1099173$5B16DC3D-5411-49AB-90AB-6A9C254737D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"69c627492fd500f9c724d36db9e0f420687d667a","datavalue":{"value":{"entity-type":"item","numeric-id":4247302,"id":"Q4247302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa01695122dd491026673895a6f88b2f84cd9ec4","datavalue":{"value":{"amount":"+0.7895460724830627","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":"Q1099173$7725E7DB-BB30-42D9-8DF1-2064577B1A2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e93f1a193eead903bffcd6270708864c38c07b90","datavalue":{"value":{"entity-type":"item","numeric-id":1344548,"id":"Q1344548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa01695122dd491026673895a6f88b2f84cd9ec4","datavalue":{"value":{"amount":"+0.7895460724830627","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":"Q1099173$207634CE-D628-42CE-8A41-6263654DD8D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"392c129b7f21c370b84fc2af79a657c412cde237","datavalue":{"value":{"entity-type":"item","numeric-id":4012883,"id":"Q4012883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4c7b7ff81f4bfc197d68ed5e8fd4343345a1efd6","datavalue":{"value":{"amount":"+0.7783395648002625","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":"Q1099173$EA238735-4BC7-4775-A099-126C69FC42D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"22c58fbceaca79f3a9c207feec1bc23bcd1a11b3","datavalue":{"value":{"entity-type":"item","numeric-id":4470492,"id":"Q4470492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0827d933f4f54f2522c4d161791b4875225276a4","datavalue":{"value":{"amount":"+0.7781835198402405","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":"Q1099173$7DC2B383-5481-401A-A040-6C48B32C44E4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On the syntax of Martin-L\u00f6f's type theories","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/On_the_syntax_of_Martin-L%C3%B6f%27s_type_theories"}}}}}