Composition of Deductions within the Propositions-As-Types Paradigm

0535279 - FLÚ 2021 RIV CH eng J - Journal Article
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
R&D Projects: GA ČR(CZ) GA19-12420S
Institutional support: RVO:67985955
Keywords : General proof theory * propositions as types * Curry–Howard isomorphism * constructive type theory * categorial proof theory * Cut rule * composition of deduction
OECD category: Philosophy, History and Philosophy of science and technology
Impact factor: 0.385, year: 2020
Method of publishing: Limited access
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.
Permanent Link: http://hdl.handle.net/11104/0313350