Composition of Deductions within the Propositions-As-Types Paradigm

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Composition of Deductions within the Propositions-As-Types Paradigm

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Composition of Deductions within the Propositions-As-Types Paradigm

Popis výsledku anglicky

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.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

60301 - Philosophy, History and Philosophy of science and technology

Projekt

<a href="/cs/project/GA19-12420S" target="_blank" >GA19-12420S: Hyperintenzionální význam, teorie typů a logická dedukce</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2020

Kód důvěrnosti údajů

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

Název periodika

Logica Universalis

ISSN

1661-8297

e-ISSN

—

Svazek periodika

14

Číslo periodika v rámci svazku

4

Stát vydavatele periodika

CH - Švýcarská konfederace

Počet stran výsledku

13

Strana od-do

481-493

Kód UT WoS článku

000565490700001

EID výsledku v databázi Scopus

2-s2.0-85090186027