Puzzles of Existential Generalisation from Type-theoretic Perspective

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14210%2F22%3A00129199" target="_blank" >RIV/00216224:14210/22:00129199 - isvavai.cz</a>

Výsledek na webu

<a href="https://arxiv.org/abs/2204.06726v1" target="_blank" >https://arxiv.org/abs/2204.06726v1</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.4204/EPTCS.358.6" target="_blank" >10.4204/EPTCS.358.6</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Puzzles of Existential Generalisation from Type-theoretic Perspective

Popis výsledku v původním jazyce

The present paper addresses several puzzles related to the Rule of Existential Generalization, (EG). In solution to these puzzles from the viewpoint of simple type theory, I distinguish (EG) from a modified Rule of Existential Quantifier Introduction which is derivable from (EG). Both these rules are often confused and both are considered as primitive but I show that (EG) itself is derivable from the proper Rule of Existential Quantifier Introduction. Moreover, the latter rule must be primitive in logical systems that treat both total and partial functions, for the universal and the existential quantifiers are not interdefinable in them. An appropriate natural deduction for such a system is deployed. The present logical system is simpler than the system recently proposed and applied by the present author. It utilises an adequate definition of substitution which is capable of handling not only a higher-order quantification, but also (hyper)intensional contexts.

Název v anglickém jazyce

Puzzles of Existential Generalisation from Type-theoretic Perspective

Popis výsledku anglicky

The present paper addresses several puzzles related to the Rule of Existential Generalization, (EG). In solution to these puzzles from the viewpoint of simple type theory, I distinguish (EG) from a modified Rule of Existential Quantifier Introduction which is derivable from (EG). Both these rules are often confused and both are considered as primitive but I show that (EG) itself is derivable from the proper Rule of Existential Quantifier Introduction. Moreover, the latter rule must be primitive in logical systems that treat both total and partial functions, for the universal and the existential quantifiers are not interdefinable in them. An appropriate natural deduction for such a system is deployed. The present logical system is simpler than the system recently proposed and applied by the present author. It utilises an adequate definition of substitution which is capable of handling not only a higher-order quantification, but also (hyper)intensional contexts.

Druh

D - Stať ve sborníku

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

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2022

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 statě ve sborníku

10th International Conference on Non-Classical Logics. Theory and Applications (NCL 2022) Electronic Proceedings in Theoretical Computer Science (EPTCS) 358

ISBN

—

ISSN

2075-2180

e-ISSN

—

Počet stran výsledku

16

Strana od-do

68-83

Název nakladatele

Logic in Computer Science

Místo vydání

Cornell Univeristy (USA), UNSW Austrálie

Místo konání akce

Lodz (PL)

Datum konání akce

14. 3. 2022

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—