The placeholder view of assumptions and the Curry–Howard correspondence
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
The placeholder view of assumptions and the Curry–Howard correspondence
Original language description
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.
Czech name
—
Czech description
—
Classification
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
Result continuities
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
Others
Publication year
2021
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Synthese
ISSN
0039-7857
e-ISSN
1573-0964
Volume of the periodical
198
Issue of the periodical within the volume
11
Country of publishing house
NL - THE KINGDOM OF THE NETHERLANDS
Number of pages
17
Pages from-to
10109-10125
UT code for WoS article
000537329100001
EID of the result in the Scopus database
2-s2.0-85085971427