Number of the records: 1
Composition of Deductions within the Propositions-As-Types Paradigm
- 1.
SYSNO ASEP 0535279 Document Type J - Journal Article R&D Document Type Journal Article Subsidiary J Článek ve WOS Title Composition of Deductions within the Propositions-As-Types Paradigm Author(s) Pezlar, Ivo (FLU-F) ORCID, RID, SAI Source Title Logica Universalis. - : Springer - ISSN 1661-8297
Roč. 14, č. 4 (2020), s. 481-493Number of pages 13 s. Publication form Print - P Language eng - English Country CH - Switzerland Keywords General proof theory ; propositions as types ; Curry–Howard isomorphism ; constructive type theory ; categorial proof theory ; Cut rule ; composition of deduction Subject RIV AA - Philosophy ; Religion OECD category Philosophy, History and Philosophy of science and technology R&D Projects GA19-12420S GA ČR - Czech Science Foundation (CSF) Method of publishing Limited access Institutional support FLU-F - RVO:67985955 UT WOS 000565490700001 EID SCOPUS 85090186027 DOI 10.1007/s11787-020-00260-3 Annotation Kosta Došen argued in his papers Inferential Semantics (in Wansing, H. (ed.) Dag Prawitz on Proofs and Meaning, pp. 147–162. Springer, Berlin 2015) and On the Paths of Categories (in Piecha, T., Schroeder-Heister, P. (eds.) Advances in Proof-Theoretic Semantics, pp. 65–77. Springer, Cham 2016) that the propositions-as-types paradigm is less suited for general proof theory because-unlike proof theory based on category theory-it emphasizes categorical proofs over hypothetical inferences. One specific instance of this, Došen points out, is that the Curry-Howard isomorphism makes the associativity of deduction composition invisible. We will show that this is not necessarily the case. Workplace Institute of Philosophy Contact Chlumská Simona, chlumska@flu.cas.cz ; Tichá Zuzana, asep@flu.cas.cz Tel: 221 183 360 Year of Publishing 2021 Electronic address https://doi.org/10.1007/s11787-020-00260-3
Number of the records: 1