J 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 (203 Česká republika, domácí) a Jiří RACLAVSKÝ (203 Česká republika, garant, domácí)

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 v roce 2022

Organizační jednotka

Filozofická fakulta

DOI

UT WoS

000936329300001

Klíčová slova anglicky

partial type theory; completeness proof; partiality; natural deduction; higher-order logic; hyperintensionality

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 11. 3. 2024 12:35, RNDr. Daniel Jakubík

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