RACLAVSKÝ, Jiří and Petr KUCHYŇKA. Completeness in Partial Type Theory. In Non-Classical Modal and Predicate Logics (NCMPL2021), Bochum, November 23-26, 2021. 2021.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Completeness in Partial Type Theory
Authors RACLAVSKÝ, Jiří (203 Czech Republic, guarantor, belonging to the institution) and Petr KUCHYŇKA (203 Czech Republic).
Edition Non-Classical Modal and Predicate Logics (NCMPL2021), Bochum, November 23-26, 2021, 2021.
Other information
Original language English
Type of outcome Presentations at conferences
Field of Study 60301 Philosophy, History and Philosophy of science and technology
Country of publisher Germany
Confidentiality degree is not subject to a state or trade secret
WWW URL
RIV identification code RIV/00216224:14210/21:00119367
Organization unit Faculty of Arts
Keywords in English completeness; partial type theory; natural deduction
Tags rivok
Tags International impact, Reviewed
Changed by Changed by: Mgr. et Mgr. Lucie Racyn, učo 445546. Changed: 21/3/2022 12:38.
Abstract
Higher-order logic (HOL), especially simple type theory (STT), are expressive systems of quantification over numerous domains. The expressive power causes incompleteness in standard models, but Henkin proved the completeness of STT w.r.t. to general models. We adjust his procedure and provide a completeness proof for natural deduction system for partial TT called TT*, which is systematically equipped with both total and partial functions, and even with special `evaluation terms' (the system thus treats even a hierarchy of functions-as-computations).
Links
GA19-12420S, research and development projectName: Hyperintenzionální význam, teorie typů a logická dedukce (Acronym: Hyperintensionality and Types)
Investor: Czech Science Foundation
PrintDisplayed: 29/7/2024 03:24