The Rule of Existential Generalisation, Its Derivability and Formal Semantics
| Authors | |
|---|---|
| Year of publication | 2021 |
| Type | Appeared in Conference without Proceedings |
| MU Faculty or unit | |
| Citation | |
| 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). |
| Related projects: |