The placeholder view of assumptions and the Curry–Howard correspondence

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985955%3A_____%2F21%3A00546332" target="_blank" >RIV/67985955:_____/21:00546332 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/s11229-020-02706-z" target="_blank" >https://doi.org/10.1007/s11229-020-02706-z</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/s11229-020-02706-z" target="_blank" >10.1007/s11229-020-02706-z</a>

Jazyk výsledku

angličtina

Název v původním jazyce

The placeholder view of assumptions and the Curry–Howard correspondence

Popis výsledku v původním jazyce

Proofs from assumptions are amongst the most fundamental reasoning techniques. Yet the precise nature of assumptions is still an open topic. One of the most prominent conceptions is the placeholder view of assumptions generally associated with natural deduction for intuitionistic propositional logic. It views assumptions essentially as holes in proofs, either to be filled with closed proofs of the corresponding propositions via substitution or withdrawn as a side effect of some rule, thus in effect making them an auxiliary notion subservient to proper propositions. The Curry-Howard correspondence is typically viewed as a formal counterpart of this conception. I will argue against this position and show that even though the Curry-Howard correspondence typically accommodates the placeholder view of assumptions, it is rather a matter of choice, not a necessity, and that another more assumption-friendly view can be adopted.

Název v anglickém jazyce

The placeholder view of assumptions and the Curry–Howard correspondence

Popis výsledku anglicky

Proofs from assumptions are amongst the most fundamental reasoning techniques. Yet the precise nature of assumptions is still an open topic. One of the most prominent conceptions is the placeholder view of assumptions generally associated with natural deduction for intuitionistic propositional logic. It views assumptions essentially as holes in proofs, either to be filled with closed proofs of the corresponding propositions via substitution or withdrawn as a side effect of some rule, thus in effect making them an auxiliary notion subservient to proper propositions. The Curry-Howard correspondence is typically viewed as a formal counterpart of this conception. I will argue against this position and show that even though the Curry-Howard correspondence typically accommodates the placeholder view of assumptions, it is rather a matter of choice, not a necessity, and that another more assumption-friendly view can be adopted.

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í

2021

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

Synthese

ISSN

0039-7857

e-ISSN

1573-0964

Svazek periodika

198

Číslo periodika v rámci svazku

11

Stát vydavatele periodika

NL - Nizozemsko

Počet stran výsledku

17

Strana od-do

10109-10125

Kód UT WoS článku

000537329100001

EID výsledku v databázi Scopus

2-s2.0-85085971427