Decidable Fragments of the Simple Theory of Types with Infinity and NF

作者：Dawar Anuj^*; Forster Thomas; McKenzie Zachiri

来源：Notre Dame Journal of Formal Logic, 2017, 58(3): 433-451.

DOI：10.1215/00294527-2017-0009

• simple theory of types
• Quine's NF
• universal-existential sentences

We identify complete fragments of the simple theory of types with infinity (TSTI) and Quine's new foundations (NF) set theory. We show that TSTI decides every sentence phi in the language of type theory that is in one of the following forms:
(A) phi = for all chi(r1)(1) ... for all chi(rk)(k) there exists y(1)(s1) ... there exists y(l)(sl) theta where the superscripts denote the types of the variables, s(1) > ... > s(l), and theta is quantifier-free,
(B) phi = for all chi(r1)(1) ... for all chi(rk)(k) there exists y(1)(s) ... there exists y(l)(s) theta where the superscripts denote the types of the variables and theta is quantifier-free.
This shows that NF decides every stratified sentence theta in the language of set theory that is in one of the following forms:
(A') phi = for all chi(1)...for all chi(k)there exists y(1)...there exists y(1) theta where theta is quantifier-free and phi admits a stratification that assigns distinct values to all of the variables y(1),...,y(l),
(B') phi = for all chi(1)...for all chi(k)there exists y(1)...there exists y(1) theta where theta is quantifier-free and phi admits a stratification that assigns distinct values to all of the variables y(1),...,y(l).

• 出版日期2017