Natural Deduction for Partial Type Theory with 'Evaluation Terms'

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 The talk proposes an expressive natural deduction system in sequent style $\mathsf{ND_{TT^*}}$ for a higher-order partial type theory $\mathsf{TT^*}$. $\mathsf{TT^*}$ treats both total and partial functions-as-graphs and also acyclic algorithmic computations, called constructions (of certain objects of $\mathsf{TT^*}$). The system is usable e.g. for the analysis of fine-grained hyperintensionality (see e.g. Tich\'{y} 1988) and meta-logical notions. The basic part is adjusted from Tich\'{y}'s 1982 convenient natural deduction system for his partial type theory (for other approaches, see e.g. Farmer 1990, Muskens 1995, Moschovakis 2005). $\mathsf{TT^*}$ mainly extends his system by admission of `evaluation terms' (cf. e.g. Tich\'{y} 1988, Farmer 2016, Raclavsk\'y 2020). Our $\mathsf{ND_{TT^*}}$ provides all basic rules governing those special constructions. Finally, we sketch a Henkin-style completeness proof for $\mathsf{ND_{TT^*}}$.
Související projekty:

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