Completeness in Partial Type Theory

Logo poskytovatele
Autoři

RACLAVSKÝ Jiří KUCHYŇKA Petr

Rok publikování 2021
Druh Další prezentace na konferencích
Fakulta / Pracoviště MU

Filozofická fakulta

Citace
Popis 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).
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.