Completeness in Partial Type Theory

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14210%2F21%3A00119367" target="_blank" >RIV/00216224:14210/21:00119367 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Completeness in Partial Type Theory

Original language description

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).

Czech name

—

Czech description

—

Type

O - Miscellaneous

CEP classification

—

OECD FORD branch

60301 - Philosophy, History and Philosophy of science and technology

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)

Publication year

2021

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů