MENŠÍK, Marek, Jakub KERMASCHEK and Luděk CIENCIALA. Existential generalization in TIL. In International Multidisciplinary Scientific GeoConference Surveying Geology and Mining Ecology Management, SGEM. Volume 17. Sofia: International Multidisciplinary Scientific Geoconference, 2017, p. 311-318. ISBN 978-619-7408-01-0. Available from: https://dx.doi.org/10.5593/sgem2017/21/S07.040.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Existential generalization in TIL
Authors MENŠÍK, Marek (203 Czech Republic, guarantor, belonging to the institution), Jakub KERMASCHEK (203 Czech Republic) and Luděk CIENCIALA (203 Czech Republic, belonging to the institution).
Edition Volume 17. Sofia, International Multidisciplinary Scientific GeoConference Surveying Geology and Mining Ecology Management, SGEM, p. 311-318, 8 pp. 2017.
Publisher International Multidisciplinary Scientific Geoconference
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Bulgaria
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
RIV identification code RIV/47813059:19240/17:A0000111
Organization Filozoficko-přírodovědecká fakulta – Slezská univerzita v Opavě – Repository
ISBN 978-619-7408-01-0
ISSN 1314-2704
Doi http://dx.doi.org/10.5593/sgem2017/21/S07.040
Keywords in English Deduction; Existential Generalization; Extension; Hyperintension; Intension; Logic; TIL
Tags ÚI
Tags International impact, Reviewed
Changed by Changed by: Mgr. Kamil Matula, učo 1145. Changed: 28/3/2018 14:15.
Abstract
The paper deals with the fundamental rule of extensional logics, namely the rule of Existential Generalization. This rule can be applied in the situation when a function f is applied on its argument a to obtain the value of f at a. If the application does not fail, i.e., if the function f is defined at a, then we can existentially quantify, and derive that there is the value f(a). Our system is based on Transparent Intensional Logic (TIL). Since TIL is a hyperintensional, partial, typed lambda calculus, we examine the validity of the rule in TIL, or rather in its computational variant the TIL-Script language. The rule is context sensitive in the sense that depending on a context we should recognize the type of entity to be abstracted over. This is not to say that the rule can be invalid dependently on context; the rule is valid universally. Only that the type of the argument over which we quantity depends on the context. There are three kinds of contexts to be distinguished, namely extensional, intensional and hyperintensonal. We introduce the definition of these three kinds of context and an algorithm that recognizes in which context a particular construction occurs so that the Existential Generalization can be validly applied. The tool navigates users through the correct application of the deduction rules.
Print
Add to clipboard Displayed: 3/5/2024 09:34