{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:05Z","timestamp":1753889765724,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2008,1,7]],"date-time":"2008-01-07T00:00:00Z","timestamp":1199664000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>For many a natural deduction style logic there is a Hilbert-style logic that\nis equivalent to it in that it has the same theorems (i.e. valid judgements\nwith empty contexts). For intuitionistic logic, the axioms of the equivalent\nHilbert-style logic can be propositions which are also known as the types of\nthe combinators I, K and S. Hilbert-style versions of illative combinatory\nlogic have formulations with axioms that are actual type statements for I, K\nand S. As pure type systems (PTSs)are, in a sense, equivalent to systems of\nillative combinatory logic, it might be thought that Hilbert-style PTSs (HPTSs)\ncould be based in a similar way. This paper shows that some PTSs have very\ntrivial equivalent HPTSs, with only the axioms as theorems and that for many\nPTSs no equivalent HPTS can exist. Most commonly used PTSs belong to these two\nclasses. For some PTSs however, including lambda* and the PTS at the basis of\nthe proof assistant Coq, there is a nontrivial equivalent HPTS, with axioms\nthat are type statements for I, K and S.<\/jats:p>","DOI":"10.2168\/lmcs-4(1:1)2008","type":"journal-article","created":{"date-parts":[[2008,6,3]],"date-time":"2008-06-03T13:25:30Z","timestamp":1212499530000},"source":"Crossref","is-referenced-by-count":0,"title":["Are there Hilbert-style Pure Type Systems?"],"prefix":"10.46298","volume":"Volume 4, Issue 1","author":[{"given":"M. W.","family":"Bunder","sequence":"first","affiliation":[]},{"given":"W. M. J.","family":"Dekkers","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2008,1,7]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/839\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/839\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:57:19Z","timestamp":1681243039000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/839"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,1,7]]},"references-count":0,"URL":"https:\/\/doi.org\/10.2168\/lmcs-4(1:1)2008","relation":{"is-same-as":[{"id-type":"arxiv","id":"0707.0890","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.0707.0890","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2008,1,7]]},"article-number":"839"}}