Composition of Deductions within the Propositions-As-Types Paradigm

0535279 - FLÚ 2021 RIV CH eng J - Článek v odborném periodiku
Pezlar, Ivo
Composition of Deductions within the Propositions-As-Types Paradigm.
Logica Universalis. Roč. 14, č. 4 (2020), s. 481-493. ISSN 1661-8297. E-ISSN 1661-8300
Grant CEP: GA ČR(CZ) GA19-12420S
Institucionální podpora: RVO:67985955
Klíčová slova: General proof theory * propositions as types * Curry–Howard isomorphism * constructive type theory * categorial proof theory * Cut rule * composition of deduction
Obor OECD: Philosophy, History and Philosophy of science and technology
Impakt faktor: 0.385, rok: 2020
Způsob publikování: Omezený přístup
https://doi.org/10.1007/s11787-020-00260-3

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.
Trvalý link: http://hdl.handle.net/11104/0313350