k 2021

Completeness in Partial Type Theory

RACLAVSKÝ, Jiří a Petr KUCHYŇKA

Základní údaje

Originální název

Completeness in Partial Type Theory

Autoři

RACLAVSKÝ, Jiří (203 Česká republika, garant, domácí) a Petr KUCHYŇKA (203 Česká republika)

Vydání

Non-Classical Modal and Predicate Logics (NCMPL2021), Bochum, November 23-26, 2021, 2021

Další údaje

Jazyk

angličtina

Typ výsledku

Prezentace na konferencích

Obor

60301 Philosophy, History and Philosophy of science and technology

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Odkazy

Kód RIV

RIV/00216224:14210/21:00119367

Organizační jednotka

Filozofická fakulta

Klíčová slova anglicky

completeness; partial type theory; natural deduction

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 21. 3. 2022 12:38, Mgr. et Mgr. Lucie Racyn

Anotace

V originále

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

Návaznosti

GA19-12420S, projekt VaV
Název: Hyperintenzionální význam, teorie typů a logická dedukce (Akronym: Hyperintensionality and Types)
Investor: Grantová agentura ČR, Hyperintensional meaning, type theory and logical deduction