Dawar, Anuj; Forster, Thomas; McKenzie, Zachiri Decidable fragments of the simple theory of types with infinity and NF. (English) Zbl 1417.03271 Notre Dame J. Formal Logic 58, No. 3, 433-451 (2017). Summary: 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=\forall x_{1}^{r_{1}}\dots \forall x_{k}^{r_{k}}\exists y_{1}^{s_{1}}\dots \exists y_{l}^{s_{l}}\theta\) where the superscripts denote the types of the variables, \(s_{1}> \dots > s_{l}\), and \(\theta\) is quantifier-free, (B) \(\phi=\forall x_{1}^{r_{1}}\dots \forall x_{k}^{r_{k}}\exists y_{1}^{s}\dots \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 \(\phi\) in the language of set theory that is in one of the following forms: (A\('\)) \(\phi=\forall x_{1}\dots \forall x_{k}\exists y_{1}\dots \exists y_{l}\theta\) where \(\theta\) is quantifier-free and \(\phi\) admits a stratification that assigns distinct values to all of the variables \(y_{1},\dots,y_{l}\), (B\('\)) \(\phi=\forall x_{1}\dots \forall x_{k}\exists y_{1}\dots \exists y_{l}\theta\) where \(\theta\) is quantifier-free and \(\phi\) admits a stratification that assigns the same value to all of the variables \(y_{1},\dots,y_{l}\). Cited in 1 Document MSC: 03E70 Nonclassical and second-order set theories 03B25 Decidability of theories and sets of sentences 03B15 Higher-order logic; type theory (MSC2010) Keywords:simple theory of types; Quine’s NF; universal-existential sentences PDFBibTeX XMLCite \textit{A. Dawar} et al., Notre Dame J. Formal Logic 58, No. 3, 433--451 (2017; Zbl 1417.03271) Full Text: DOI arXiv Euclid