Composition of Deductions within the Propositions-As-Types Paradigm

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985955%3A_____%2F20%3A00535279" target="_blank" >RIV/67985955:_____/20:00535279 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.1007/s11787-020-00260-3" target="_blank" >https://doi.org/10.1007/s11787-020-00260-3</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/s11787-020-00260-3" target="_blank" >10.1007/s11787-020-00260-3</a>

Result language
angličtina
Original language name
Composition of Deductions within the Propositions-As-Types Paradigm
Original language description
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.
Czech name
—
Czech description
—

Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
60301 - Philosophy, History and Philosophy of science and technology

Project
<a href="/en/project/GA19-12420S" target="_blank" >GA19-12420S: Hyperintensional Meaning, Type Theory and Logical Deduction</a><br>
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year
2020
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)