The Rule of Existential Generalisation, Its Derivability and Formal Semantics
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14210%2F21%3A00119214" target="_blank" >RIV/00216224:14210/21:00119214 - isvavai.cz</a>
Result on the web
<a href="https://iuc.hr/programme/1480" target="_blank" >https://iuc.hr/programme/1480</a>
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
The Rule of Existential Generalisation, Its Derivability and Formal Semantics
Original language description
My contribution addresses various issues concerning the rule of existential generalisation (EG). My solutions are framed within a higher-order partial type theory TT* that is equipped with a natural deduction system ND-TT*. I derive (EG) from its primitive rules, especially the rule of existential quantifier introduction (Exists-I). Similarly for another derived rule (Exists-I-eta). Substitution (t/x) of (EG) is fully and adequately specified inside the system and so (EG) is uniformly applicable within extensional, intensional and even hyperintensional contexts (we face no problems with quantifying in).
Czech name
—
Czech description
—
Classification
Type
O - Miscellaneous
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
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2021
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů