Puzzles of Existential Generalisation from Type-theoretic
Perspective

D 2022

Puzzles of Existential Generalisation from Type-theoretic Perspective

RACLAVSKÝ, Jiří

Basic information

Original name

Puzzles of Existential Generalisation from Type-theoretic Perspective

Authors

RACLAVSKÝ, Jiří (203 Czech Republic, guarantor, belonging to the institution)

Edition

SYDNEY, 00000, AUSTRALIA, Electronic Proceedings In Theoretical Computer Science (358), p. 68-83, 16 pp. 2022

Publisher

OPEN PUBL ASSOCOPEN PUBL ASSOC,

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

60301 Philosophy, History and Philosophy of science and technology

Country of publisher

United States of America

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

electronic version available online

References:

URL

RIV identification code

RIV/00216224:14210/22:00129199

Organization unit

Faculty of Arts

ISSN

DOI

http://dx.doi.org/10.4204/EPTCS.358.6

UT WoS

001045096000006

Keywords in English

existential generalisation; quantifying in; explicit substitution; partial type logic; natural deduction

Abstract

V originále

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.

Links

GA19-12420S, research and development project

Name: Hyperintenzionální význam, teorie typů a logická dedukce (Acronym: Hyperintensionality and Types)

Investor: Czech Science Foundation

Citovat

RACLAVSKÝ, Jiří. Puzzles of Existential Generalisation from Type-theoretic Perspective. Online. In Indrzejczak, Andrzej; Zawidski, Michal. Electronic Proceedings In Theoretical Computer Science (358). SYDNEY, 00000, AUSTRALIA: OPEN PUBL ASSOCOPEN PUBL ASSOC,, 2022, p. 68-83. ISSN 2075-2180. Available from: https://dx.doi.org/10.4204/EPTCS.358.6.

@inproceedings{2226260,
   author = {Raclavský, Jiří},
   address = {SYDNEY, 00000, AUSTRALIA},
   booktitle = {Electronic Proceedings In Theoretical Computer Science (358)},
   doi = {http://dx.doi.org/10.4204/EPTCS.358.6},
   editor = {Indrzejczak, Andrzej; Zawidski, Michal},
   keywords = {existential generalisation; quantifying in; explicit substitution; partial type logic; natural deduction},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {SYDNEY, 00000, AUSTRALIA},
   pages = {68-83},
   publisher = {OPEN PUBL ASSOCOPEN PUBL ASSOC,},
   title = {Puzzles of Existential Generalisation from Type-theoretic Perspective},
   url = {https://arxiv.org/pdf/2204.06726v1.pdf},
   year = {2022}
}

TY  - JOUR
ID  - 2226260
AU  - Raclavský, Jiří
PY  - 2022
TI  - Puzzles of Existential Generalisation from Type-theoretic Perspective
PB  - OPEN PUBL ASSOCOPEN PUBL ASSOC,
CY  - SYDNEY, 00000, AUSTRALIA
KW  - existential generalisation
KW  - quantifying in
KW  - explicit substitution
KW  - partial type logic
KW  - natural deduction
UR  - https://arxiv.org/pdf/2204.06726v1.pdf
N2  - 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.
ER  -

RACLAVSKÝ, Jiří. Puzzles of Existential Generalisation from Type-theoretic Perspective. Online. In Indrzejczak, Andrzej; Zawidski, Michal. \textit{Electronic Proceedings In Theoretical Computer Science (358)}. SYDNEY, 00000, AUSTRALIA: OPEN PUBL ASSOCOPEN PUBL ASSOC,, 2022, p.~68-83. ISSN~2075-2180. Available from: https://dx.doi.org/10.4204/EPTCS.358.6.

Detailed Information on Publication Record