Další formáty:
BibTeX
LaTeX
RIS
@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, s.~68-83. ISSN~2075-2180. Dostupné z: https://dx.doi.org/10.4204/EPTCS.358.6.
|
