2024
Completeness in partial type theory
KUCHYŇKA, Petr a Jiří RACLAVSKÝZákladní údaje
Originální název
Completeness in partial type theory
Autoři
KUCHYŇKA, Petr a Jiří RACLAVSKÝ
Vydání
Journal of Logic and Computation, Oxford, UK, Oxford University Press, 2024, 0955-792X
Další údaje
Jazyk
angličtina
Typ výsledku
Článek v odborném periodiku
Obor
60301 Philosophy, History and Philosophy of science and technology
Stát vydavatele
Velká Británie a Severní Irsko
Utajení
není předmětem státního či obchodního tajemství
Odkazy
Impakt faktor
Impact factor: 0.700
Kód RIV
RIV/00216224:14210/24:00139346
Organizační jednotka
Filozofická fakulta
UT WoS
000936329300001
EID Scopus
2-s2.0-85182900627
Klíčová slova anglicky
partial type theory; completeness proof; partiality; natural deduction; higher-order logic; hyperintensionality
Štítky
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 20. 1. 2025 15:02, Mgr. et Mgr. Stanislav Hasil, Ph.D.
Anotace
V originále
The present paper provides a completeness proof for a system of higher-order logic framed within partial type theory. The framework is a modification of Tichý’s extension of Church’s simple type theory, equipped with his innovative natural deduction system in sequent style. The system deals with both total and partial (multiargument) functions-as-mappings and also accommodates algorithmic computations arriving at various objects of the framework. The partiality of a function or a failure of a computation is not represented by a postulated null object such as the third truth value. The logical operators of the system are classical. Another welcome feature of this expressive system is that its consequence relation is monotonic.
Návaznosti
| GA19-12420S, projekt VaV |
|